Tradeo Issues in Local Search Guidance for SAT 2001

Abstract:  Introduction Satisfiability (SAT) problems are capable of representing important real-world problems, like e.g. planning, scheduling and robotic movement, and e#cient encodings exist for many of these. E#cient solvers for these problems are thus of critical significance. SAT has thus received substantial attention in recent years, and e#cient SAT solvers exist. What sets SAT apart from other combinatorial optimization problems is that SAT is basically a feasibility problem. Once a variable assignment is found that satisfies all the clauses (see Section 2), the problem is solved. There is thus no guidance from the objective function. Guidance is customarily instead based on the amount of infeasibility, usually by counting the number of unsatisfied clauses for a given solution vector. There are many approaches to solving the SAT problem. Constructive methods range from complete tree-search (DPL - Davis-Putnam-Lovelan d [2]), to constructive heuristics like GRASP [8] and surrogate const