Skip navigation
Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributorGupta, Aarti-
dc.contributor.advisorMalik, Sharad-
dc.contributor.authorYing, Victor-
dc.description.abstractBoolean satisfiability (SAT) solvers have achieved impressive performance in practical settings. They are now heavily relied upon in formal verification and other industry applications. However, their degree of success not well understood, and it is not known how much room there is for improvement in performance through continued improvements in decision heuristics, whose development has been responsible for orders of magnitude of performance improvements in the past. In this report, we define a notion of dependency relations between events in solver execution that allows us to identify what portions of the work done by the solver on any given instance is required or could be avoided by changing the decision heuristic. We carry out experiments with practical application-focused benchmarks and find that most branches chosen by the decision heuristic are required, and a minority of work done by the solver is wasteful. This suggests limited improvements are still possible by improving decision heuristics alone if other aspects of SAT solvers are not improved.en_US
dc.format.extent65 pagesen_US
dc.titleAnalyzing Decision Heuristic Effectiveness in Boolean Satisfiability Solversen_US
dc.typePrinceton University Senior Theses-
pu.departmentElectrical Engineeringen_US
Appears in Collections:Electrical and Computer Engineering, 1932-2022

Files in This Item:
File SizeFormat 
Ying_Victor_thesis.pdf523.19 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.