学位论文详细信息
An Analysis of the Effect of Community Structure on SAT Solver Performance
community;survival;SAT;solver;boolean satisfiability;linear regression;Electrical and Computer Engineering
Newsham, Zackary
University of Waterloo
关键词: community;    survival;    SAT;    solver;    boolean satisfiability;    linear regression;    Electrical and Computer Engineering;   
Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/9110/1/Newsham_Zack.pdf
瑞士|英语
来源: UWSPACE Waterloo Institutional Repository
PDF
【 摘 要 】

Despite enormous improvements in Boolean SATisfiability solver performanceover the last decade, it is still unclear why specific input formula are slowto solve, when other similarly specified formula execute more quickly. Thiswork explores the relationship between the community structure of a SATformula and its execution time on several state-of-the-art solvers. We explorethe analysis of this data from a number of directions; first, we explore therelationship between the well known clause-variable ratio result, and com-munity structure in randomly generated instances. Second, we perform astandard linear regression on data obtained from the 2013 SAT competition.Third, we present a visualisation tool and data repository for viewing thestructure of a SAT formula. Fourth, we explore the effect of hardware con-straints on the solution time of instances across various machines. Finally,we explore survival analysis, a technique that is new to the field of BooleanSATisfiability. By collating the results from each of these experiments, wehave determined that the community structure is critical in determining thesolution time of a SAT formula, more important than the clause-variableratio of the formula. While this work is not a complete explanation of thevarying solution time of SAT formulae, it has provided us with significantinsight for further research to answer the question: why different similarlyspecified formula have such different solution times?

【 预 览 】
附件列表
Files Size Format View
An Analysis of the Effect of Community Structure on SAT Solver Performance 4366KB PDF download
  文献评价指标  
  下载次数:20次 浏览次数:38次