Solving Non-Boolean Satisfiability Problems with Stochastic Local Search

Much excitement has been generated by the success of stochastic local search procedures at finding solutions to large, very 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. The comparison first examines the search spaces confronted by the four methods then tests their ability to solve random formulas, the round-robin sports scheduling problem and the quasigroup completion problem. The experiments show that the re...

• Type: Conference
• Year: 2001
• Where: IJCAI
• Authors: Alan M. Frisch, Timothy J. Peugniez
• Keywords: Domain Size, IJCAI 2001, IJCAI 2007, Non-boolean Problems, Satisfiability Problems