Whose side are you on? Finding solutions in a biased search-tree

We introduce a new jump strategy for look-ahead based satisfiability (Sat) solvers that aims to boost their performance on satisfiable formulae, while maintaining their behavior on unsatisfiable instances. Direction heuristics select which Boolean value to assign to a decision variable. They are used in various state-of-the-art Sat solvers and may bias the distribution of solutions in the search-tree. This bias can clearly be observed on hard random k-Sat formulae. While alternative jump / restart strategies are based on exploring a random new part of the search-tree, the proposed one examines a part that is more likely to contain a solution based on these observations. Experiments with - so-called distribution jumping - in the march ks Sat solver, show that this new technique boosts the number of satisfiable formulae it can solve. Moreover, it proved essential for winning the satisfiable crafted category during the Sat 2007 competition.

• Type: Journal
• Year: 2008
• Where: JSAT
• Authors: Marijn Heule, Hans van Maaren
• Keywords: JSAT 2008, Random K-Sat Formulae, Satisfiable Formulae, State-of-the-art Sat Solvers