Solving Non-Boolean Satisfiability Problems
Project Summary
Much excitement has been generated by the recent success
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 project has been concerned with developing, analyzing and comparing
a variety of direct and transformation methods for solving
non-Boolean satisfiability problems with stochastic local search
[Frisch, Peugniez, Doggett and Nightingale, 2005; Frisch and Peugniez, 2001; Slack, 2000] and systematic search [Stock,2000].
Participants
Software Available
Download
a tar file that contains five
programs, described briefly below. Further discussion of
the first four of these programs can be found in
[Frisch and Peugniez, 2001].
The NB-Walksat search procedure
NB-Walksat is a stochastic local search procedure that can find
satisfying assignments to non-Boolean clauses in conjuctive normal
form (CNF). It directly generalises Walksat
[Selman, Kautz and Cohen, 1994], a highly-successful stochastic
local search procedure
for Boolean satisfiability problems. When handling a Boolean formula
the two procedures perform the same search, and, in spite of its
increased generality, NB-Walksat is almost as fast as Walksat.
The most recent version of NB-Walksat is version 4, which was
implemented by replacing the code of the core search procedure of
Walksat version 19 with code for the generalised search procedure.
Obtaining this generality required a complete reworking of the data
structures that maintain formulas and assignments.
The NB-to-B formula translator
This program transforms non-Boolean CNF formulas
to Boolean CNF formulas.
Three kinds of transformations are used, which we have
called "unary/unary", "unary/binary" and binary.
The unary/unary transformation has been previously used
by many researchers, and the binary transformation has
beeen previously used by only a few researchers. The unary/binary
transformation is newly-developed in this project.
The most recent version is Version 1.
The NB-to-B program allows the user to control a number of features of
the translation. The most important is whether the resulting Boolean
formulas should contain clauses that express the at-least-one and the
at-most-one constraints.
The most recent version is Version 1.
The NB-rand random formula generator
This program generates random, positive (that is, no negation symbols)
CNF non-Boolean formulas using a model
similar to the constant length model for Boolean clauses advocated by
Selman, Mitchell and Levesque [1996].
Frisch and Peugniez [2001] present a method for using this program
to generate random formulas that vary in domain size but are similar
in other respects. This has proved to be valuable to test the
effect of domain size on problem solving performance.
The program allows the user to set five
parameters: N, D, C, V and L.
Each generated formula consists of exactly C clauses.
Using a fixed set of N variables each with a domain size of
D, each clause is generated by randomly chosing V
distinct variables and then, for each, randomly choosing L
values from its domain.
Each of the chosen variables is coupled with each of its L
chosen values to form L x V positive literals, which are
disjoined together to form a clause.
The most recent version of this program is version 3.
The Col-to-NB colouring problem translator
This program tranlates graph coloring problems to non-Boolean CNF
formulas. The format of the graphs input to this program is that
which is used in the DIMACS archive. By passing the NB-formulas
produced by this translator through NB-to-B, one can produce Boolean
formulas to represent graph colouring problems.
The B-to-NB formula translator
This program transforms a Boolean formula to a non-Boolean formula
in which every variable has a domain of size 2. We have used
this to compare the performance of Walksat to that of NB-Walksat
by running Walsksat on a Boolean formula, say F,
and NB-Walksat on the formula that results from running F
through this translator.
The most recent version is Version 1.
References to Our Papers and Related Papers
- Alan M. Frisch, Timothy J. Peugniez,
Anthony J. Doggett and Peter W.Nightingale.
Solving Non-Boolean Satisfiability Problems with
Stochastic Local Search: A Comparison of Encodings,
Journal of Automated Reasoning,
to appear, 2005.
- Alan M. Frisch and Timothy J. Peugniez.
Solving
Non-Boolean Satisfiability Problems with Stochastic Local Search.
In
Proc. of the 17th International Joint Conf. on Artificial
Intelligence,
2001.
- Bart Selman, David Mitchell and Hector J. Levesque.
Generating Hard Satisfiability Problems.
Artificial Intelligence, Volume 81(1-2),
March 1996, pages 17-29.
- Timothy J. Peugniez.
Solving
Non-Boolean Satisfiability Problems with Local Search.
BSc Dissertation, Department of Computer Science, University of
York, March, 1998.
- Bart Selman, Henry A. Kautz and Bram Cohen.
Noise Strategies for Improving Local Search.
In
Proc. of AAAI-94, pages 337-343,
Menlo Park, CA, USA, 1994. AAAI Press.
- Matthew J. Slack.
Solving
Planning as Satisfiability: Boolean Versus Non-Boolean Encodings.
BSc Dissertation, Department of Computer Science, University of
York, March, 2000.
[
body of paper]
[
tables of results]
- Peter G. Stock.
Solving
Non-Boolean Satisfiability Problems with the Davis-Putnam Method.
BSc Dissertation, Department of Computer Science, University of
York, March, 2000.
Artificial Intelligence Group
Department of Computer Science
University of York
York YO10 5DD,
U.K.
Tel: +44 1904 432745, Fax: +44 1904 432767
Email: frisch@cs.york.ac.uk
WWW: http://www.cs.york.ac.uk/aig