Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability
Vladimir Pisanov · UWSpace (University of Waterloo) · 2012
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. \tWe 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. \tThe 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. \tThe second approach determines polarities by minimizing an objective function corresponding to the number of clauses conflicting with each assignment. \tThe third approach determines preferred polarities by performing stochastic gradient descent on objective functions sampled from a family of continuous potentials.\t \tThe 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.