Boolean Satisfiability (SAT) is a fundamental NP-complete problem of determining whether there exists an assignment of variables whichmakes 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 possiblevariable assignments.We show that the order in which variable polarities are assignedcan 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 clausesconflicting with each assignment.The third approach determines preferred polarities by performing stochasticgradient 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.
【 预 览 】
附件列表
Files
Size
Format
View
Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability
PDF
download
878987797
028-85220240
