Abstract
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, and then tests their ability to solve random formulas, the round-robin sports scheduling problem, and the quasigroup completion problem. The experiments show that the relative performance of the methods depends on the domain size of the problem and that the direct method scales better as domain size increases.
Along the route to performing these comparisons we make three other contributions. First, we generalize Walksat, a highly successful stochastic local search procedure for Boolean satisfiability problems, to work on problems with domains of any finite size. Second, we introduce a new method for transforming non-Boolean problems to Boolean problems and improve on an existing transformation. Third, we identify sufficient conditions for omitting at-least-one and at-most-one clauses from a transformed formula. Fourth, for use in our experiments we propose a model for generating random formulas that vary in domain size but are similar in other respects.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Achlioptas, D., Gomes, C. P., Kautz, H. A. and Selman, B. (2000) Generating satisfiable problem instances, in Proc. of the Seventeenth National Conf. on Artificial Intelligence, pp. 256–261.
Béjar, R. (2000) Systematic and Regular Search Algorithms for Regular-SAT. Ph.D. thesis, Universitat Autonòma de Barcelona.
Béjar, R. and Manyà, F. (1999a) A comparison of systematic and local search algorithms for regular CNF formulas, in A. Hunter and S. Parsons (eds.), Proc. Fifth European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty, ECSQARU’99, London, UK, Vol. 1638 of Lecture Notes in Artificial Intelligence, pp. 22–31.
Béjar, R. and Manyà, F. (1999b) Solving combinatorial problems with regular local search algorithm, in H. Ganzinger and D. McAllester (eds.), Proc. 6th Int. Conference on Logic for Programming and Automated Reasoning, LPAR, Tbilisi, Georgia, Vol. 1705 of Lecture Notes in Artificial Intelligence, pp. 33–43.
Béjar, R. and Manyà, F. (2000) Solving the round robin problem using propositional logic, in Proc. of the Seventeenth National Conf. on Artificial Intelligence, pp. 261–266.
Béjar, R., Cabicol, A., Fernàndez, C., Manyá, F. and Gomes, C. P. (2001) Capturing structure with satisfiability, in T. Walsh (ed.), Principles and Practice of Constraint Programming – CP 2001, pp. 135–149.
Brafman, R. I. and Hoos, H. H. (1999) To encode or not to encode – I: linear planning, in Proc. of the Sixteenth Int. Joint Conf. on Artificial Intelligence, pp. 988–993.
Colbourn, C. J. (1983) Embedding partial steiner triple systems is NP-complete, J. Comb. Theory 35.
Davis, M., Logemann, G. and Loveland, D. (1962) A machine program for theorem proving, Commun. ACM 5(7).
Ernst, M. D., Millstein, T. D. and Weld, D. S. (1997) Automatic SAT-compilation of planning problems, in Proc. of the Fifteenth Int. Joint Conf. on Artificial Intelligence, pp. 1169–1176.
Frisch, A. M. and Peugniez, T. J. (1998) Solving non-Boolean satisfiability problems with local search, in Fifth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, St. Andrews, Scotland.
Frisch, A. M. and Peugniez, T. J. (2001) Solving non-Boolean satisfiability problems with stochastic local search, in Proc. of the Seventeenth Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, pp. 282–288.
Gent, I. P. (2002) Arc consistency in SAT, in Proc. of the Fifteenth European Conf. on Artificial Intelligence, pp. 121–125.
Gent, I. P. and Walsh, T. (eds.), CSPLib: A Problem Library for Constraints. http://www.csplib.org.
Gomes, C. P. and Selman, B. (1997) Problem structure in the presence of perturbations, in Proc. of the Fourteenth National Conf. on Artificial Intelligence, pp. 221–226.
Gomes, C. P., Kautz, H. A. and Ruan, Y. (2001) lsencode: A Generator of Quasigroup with Holes and Quasigroup Completion Problems.
Hoos, H. H. (1998) Stochastic Local Search–Methods, Models, Applications. Ph.D. thesis, Technical University of Darmstadt.
Hoos, H. H. (1999) SAT-encodings, search space structure, and local search performance, in Proc. of the Sixteenth Int. Joint Conf. on Artificial Intelligence, pp. 296–302.
Jonsson, A. K. and Ginsberg, M. L. (1993) Experimenting with new systematic and nonsystematic search techniques, in Working Notes of the 1993 AAAI Spring Symposium on AI and NP-Hard Problems, Stanford University in Palo Alto, California.
Kautz, H. A. and Selman, B. (1992) Planning as satisfiability, in B. Neumann (ed.), Proc. of the Tenth European Conf. on Artificial Intelligence, Vienna, Austria, pp. 359–363.
Kautz, H. A. and Selman, B. (1996) Pushing the envelope: planning, propositional logic, and stochastic search, in Proc. of the Thirteenth National Conf. on Artificial Intelligence, Portland, Oregon, USA, pp. 1202–1207.
Kautz, H. A., McAllester, D. and Selman, B. (1996) Encoding plans in propositional logic, in L. C. Aiello, J. Doyle, and S. Shapiro (eds.), Principles of Knowledge Representation and Reasoning: Proc. of the Fifth Int. Conf. San Francisco, pp. 374–385.
Kautz, H. A., McAllester, D. and Selman, B. (1997) Exploiting variable dependency in local search (Abstract), in Poster Session Abstracts of IJCAI-97, p. 57.
Kautz, H. A., Ruan, Y., Achiloptas, D., Gomes, C., Selman, B. and Stickel, M. (2001) Balance and filtering in structured satisfiable problems, in Proc. of the Seventeenth Int. Joint Conf. on Artificial Intelligence, Seattle, Washington, pp. 351–358.
Li, C. M. and Anbulagan (1997) Heuristics based on unit propagation for satisfiability problems, in Proc. of the Fifteenth Int. Joint Conf. on Artificial Intelligence, pp. 366–371.
Mitchell, D., Selman, B. and Levesque, H. J. (1992) Hard and easy distributions of SAT problems, in Proc. of the Tenth National Conf. on Artificial Intelligence, San Jose, CA, pp. 459–465.
Peugniez, T. J. (1998) Solving Non-Boolean Satisfiability Problems with Local Search. BSc dissertation, Department of Computer Science, University of York.
Prestwich, S. (2004) Local search on SAT-encoded colouring problems, in Theory and Applications of Satisfiability Testing: 6th Int. Conf., pp. 105–119.
Sebastiani, R. (1994) Applying GSAT to non-clausal formulas, J. Artif. Intell. Res. 1, 309–314.
Selman, B., Levesque, H. J. and Mitchell, D. (1992) A new method for solving hard satisfiability problems in Proc. of the Tenth National Conf. on Artificial Intelligence, pp. 440–446.
Selman, B., Kautz, H. A. and Cohen, B. (1994) Noise strategies for improving local search, in Proc. of the Twelfth National Conf. on Artificial Intelligence, Menlo Park, CA, USA, pp. 337–343.
Shaw, P. (1998) Using constraint programming and local search methods to solve vehicle routing problems, in Principles and Practice of Constraint Programming – CP 1998, pp. 417–431.
Shaw, P., Stergiou, K. and Walsh, T. (1998) Arc consistency and quasigroup completion, in Proceedings of ECAI98 Workshop on Non-binary Constraints.
Stamm-Wilbrandt, H. (1993) Programming in Propositional Logic, or Reductions: Back to the Roots (Satisfiability), Technical report, Institut für Informatik III, Universität Bonn.
Stock, P. G. (2000) Solving Non-Boolean Satisfiability with the Davis-Putnam Method, BSc dissertation, Dept. of Computer Science, Univ. of York.
Van Hentenryck, P. and Michel, L. (2003) Control abstractions for local search, in Principles and Practice of Constraint Programming – CP 2003, pp. 65–80.
Walser, J. P. (1997) Solving linear pseudo-boolean constraint problems with local search, in Proc. of the Fourteenth National Conf. on Artificial Intelligence, pp. 269–274.
Walser, J. P. (1999) Integer Optimization by Local Search: A Domain-Independent Approach, Springer, Berlin Heidelberg New York.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Frisch, A.M., Peugniez, T.J., Doggett, A.J. et al. Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings. J Autom Reasoning 35, 143–179 (2005). https://doi.org/10.1007/s10817-005-9011-0
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-005-9011-0