As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Research on incomplete algorithms for satisfiability testing lead to some of the first scalable SAT solvers in the early 1990's. Unlike systematic solvers often based on an exhaustive branching and backtracking search, incomplete methods are generally based on stochastic local search. On problems from a variety of domains, such incomplete methods for SAT can significantly outperform DPLL-based methods. While the early greedy algorithms already showed promise, especially on random instances, the introduction of randomization and so-called uphill moves during the search significantly extended the reach of incomplete algorithms for SAT. This chapter discusses such algorithms, along with a few key techniques that helped boost their performance such as focusing on variables appearing in currently unsatisfied clauses, devising methods to efficiently pull the search out of local minima through clause re-weighting, and adaptive noise mechanisms. The chapter also briefly discusses a formal foundation for some of the techniques based on the discrete Lagrangian method.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.