Solving Non-Boolean Satisfiability Problems with Stochastic Local Search

Abstract

Abstract. Much excitement has been generated by the recent success of stochastic local search procedures at finding solutions to large, vary hard satisfiability problems. Many of the problems on which these procedures have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. Approaches to solving non-Boolean satisfiability problems fall into two categories. In the direct approach, the problem is tackled by an algorithm for non-Boolean problems. In the transformation approach, the non-Boolean problem is reformulated as an equivalent Boolean problem and then a Boolean solver is used. This paper compares four methods for solving non-Boolean problems: one direct and three transformational. 1 Introduction Much excitement has been generated by the recent success of stochastic local search (SLS) procedures at finding satisfying assignments to large formulas. These procedures stochasticly search a space of all assignments for one that satisfies the given formula. Many of the problems on which these methods have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. Approaches to solving non-Boolean satisfiability problems fall into two categories. In the direct approach, the problem is tackled by an algorithm for non-Boolean problems. In the transformation approach, a Boolean solver is used by first reformulating the non-Boolean problem as an equivalent Boolean problem in which multiple Boolean variables are used in place of each non-Boolean variable. This paper compares four methods for solving non-Boolean problems: one direct and three transformational. The comparison first examines the search spaces confronted by the four methods then tests their ability to solve large graph colouring problems and large random formulas.