You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

Whose side are you on?1


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.