Boolean Satisfiability (SAT) is a fundamental NP-complete problem of determining whether there exists an assignment of variables which
makes a Boolean formula evaluate to True. SAT is a convenient representation for many naturally occurring optimization and decisions problems
such as planning and circuit verification. SAT is most commonly solved by a form of backtracking search which systematically explores the space of possible
variable assignments.
We show that the order in which variable polarities are assigned
can have a significant impact on the performance of backtracking algorithms.
We present several ways of transforming SAT instances into non-linear objective functions and describe three value-ordering methods based on iterative optimization techniques. We implement and test these heuristics in the widely-recognized MiniSAT framework.
The first approach determines polarities by applying Newton's Method to a sparse system of non-linear objective functions whose roots correspond to the satisfying assignments of the propositional formula.
The second approach determines polarities by minimizing an objective function corresponding to the number of clauses
conflicting with each assignment.
The third approach determines preferred polarities by performing stochastic
gradient descent on objective functions sampled from a family of continuous potentials.
The heuristics are evaluated on a set of standard benchmarks including random, crafted and industrial problems. We compare our results to five existing heuristics, and show that MiniSAT equipped with our heuristics often outperforms state-of-the-art SAT solvers.
| Identifer | oai:union.ndltd.org:WATERLOO/oai:uwspace.uwaterloo.ca:10012/6941 |
| Date | January 2012 |
| Creators | Pisanov, Vladimir |
| Source Sets | University of Waterloo Electronic Theses Repository |
| Language | English |
| Detected Language | English |
| Type | Thesis or Dissertation |
Page generated in 0.0021 seconds