Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp018g84mp694
Title: Analyzing Decision Heuristic Effectiveness in Boolean Satisfiability Solvers
Authors: Ying, Victor
Advisors: Malik, Sharad
Contributors: Gupta, Aarti
Department: Electrical Engineering
Class Year: 2016
Abstract: Boolean 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.
Extent: 65 pages
URI: http://arks.princeton.edu/ark:/88435/dsp018g84mp694
Type of Material: Princeton University Senior Theses
Language: en_US
Appears in Collections:Electrical Engineering, 1932-2016

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.