Artificial Intelligence Group
Alan Frisch's Teaching Pages:
Projects: SAT, NB-SAT, CSP and local search
Application of Resolution and Backtracking to the Solution of Constraint
Satisfaction Problems
Edmund Dumbill
BEng Computer Science, March 1995
Abstract: Both resolution and constraint satisfaction problems (CSPs)
are well researched areas in Artificial Intelligence today. However,
little connection has ever been made between the two. This project
investigates the use of resolution as a method for solving constraint
satisfaction problems in combination with backtracking. The aim is to
discover a balance between the number of resolutions performed and the
amount of backtracking done, so as to achieve as efficient an
algorithm as possible. The ECLIPSE & CHR system for programming
constraint solvers is described and used to implement experiments. A
limited version of resolution, ordered resolution, is introduced, and
its behaviour compared to that of the Davis-Putnam method on Boolean
CSPs. Finally, further investigations and algorithms are suggested,
including extending methods to cover more than 2-valued constraint
satisfaction problems.
Resources
Experiments with Solving Graph Colouring by Reduction to Satisfiability
Gareth Jenkins
BSc Information Engineering, March 1996
Abstract: This project is concerned with the experimental
investigation of the solvability of NP-complete problems. In
particular it examines the use of automated procedures to
solve instances of the clausal satisfiability
problem [see Garey and Johnson 1979]
generated by the translation of instances of graph colouring
problem. The investigation focuses mainly upon the difficulty of
solving the problem instances and how this is affected by the method
of translation. Some other interesting effects were noticed towards
the end of the project and have been included in this report for
completeness and to indicate possible areas for future study.
Solving Non-Boolean Satisfiability Problems with Local Search
Timothy Peugniez
BSc Computer Science, March 1998
Abstract: Currently, the most widely used local search procedures for
finding assignments for satisfiability problems operate only on
Boolean problems, that is problems expressed in terms of variables
with domains of size two. Many naturally occurring problems are
non-Boolean, in other words, they are most concisely formulated in
terms of variables with domain size greater than two. Non-Boolean
problems are typically solved by translating them into equivalent
Boolean problems. However, this can cause either large increases in
the problem size, or enlargements of the search space.
This project considers extending Boolean local search to
operate directly on non-Boolean problems, thus avoiding the Boolean
translation entirely. Experimental evidence is presented which shows
that this method is superior to the previous approach.
Resources
Solving Non-Boolean Satisfiability Problems with the Davis-Putnam Method
Peter G. Stock
BSc Computer Science, March 2000
Abstract: The Davis-Putnam method has received recent attention for its ability
to solve large problems. Many of these problems are non-Boolean, in
that they are most naturally expressed as formulas containing variables
with domains of more than two values. There are two approaches to
solving non-Boolean formulas --- either translate the problem into
a Boolean equivalent and solve this with a Boolean procedure, or use
a non-Boolean procedure directly on the non-Boolean formula. This
project develops a direct non-Boolean Davis-Putnam procedure and compares
the results of using the two approaches.
Resources
Planning as Satisfiability: Boolean vs Non-Boolean Encodings
Matthew J. Slack
BSc Computer Science, March 2000
Abstract: Recently, the performance of planners has been increased
significantly. Many of the new methods responsible for the speed-up
have used SAT-compilation techniques. These methods convert the
planning problem specification into a Boolean CNF formula, which is
then solved by a range of fast SAT solvers. However, some of the
properties of the planning problems can be more concisely expressed
using a non-Boolean encoding.
This project explores the idea of automatically converting planning
problems into non-Boolean CNF formulae, which are then solved by
one of two non-Boolean SAT solvers, developed in previous projects.
Experimental evidence is presented to show that this approach has
significant performance increases over the original Boolean method,
for some types of planning problems.
Resources
Solving MAX-XOR-SAT Problems with Stochastic Local Search
Mark Minichiello
MMath degree in Computer Science and Mathematics, March 2002
Abstract: The MAX-SAT problem is to find a truth assignment that satisfies the maximum number of
clauses in a finite set of logical clauses. In the special case of MAX-XOR-SAT, arising from
Linear Cryptanalysis, each clause is a set of literals joined by exclusive-or (xor). Solving
MAX-XOR-SAT is useful in finding keys to decrypt intercepted encrypted messages.
This report presents and evaluates Xor-WalkSAT, a method for solving MAX-XOR-SAT. Xor-WalkSAT
is a modification to the WalkSAT stochastic local search procedure, which was
developed to solve SAT problems formulated in conjunctive normal form.
Two alternatives are also presented: an algebraic method for solving XOR-SAT, where all the
clauses are satisfiable, and a translation method, where the MAX-XOR-SAT problem is
translated into conjunctive normal form and solved by WalkSAT.
The conclusion of this report is that stochastic local search, in the form of Xor-WalkSAT, can
be used to solve MAX-XOR-SAT.
Resources
Investigating Multiple Noise Parameters in Stochastic Local Search
Peter Nightingale
MEng Computer Science, March 2002
Abstract: Walksat has proven to be an excellent method for solving large, difficult instances of the propositional satisfiability problem (SAT). It requires a user-specified noise parameter, which if set suboptimally can severely harm performance. It is possible that sets of clauses within a SAT instance have significantly different noise requirements, and as a result, the instance would perform badly with one noise parameter. This report addresses multiple noise parameters (each assigned to a set of clauses) as an idea for speeding up local search.
The use of multiple noise parameters requires some division of the clauses into sets. A likely candidate is the sets generated by encoding other problems into SAT. Two encoded problems are investigated and compared.
Resources
Solving Permutation Problems with Stochastic Local Search
Linus Thand
BSc Computer Science, March 2002
Abstract:
A new method for solving permutation problems with stochastic local search has been
investigated.
The old approach, in this paper called the translation method, is to encode a
problem in a non-Boolean Satisfiability (NB-SAT) formula, which then is solved
with the NB-WalskSAT algorithm.
This report will describe modifications made in order to let the algorithm
rule out assignments that are not consistent with a certain set of permutation
constraints, that can be defined in conjunction with the NB-SAT formulae.
The method is here referred to as the direct method, and it has been
hypothesised that it would be faster at finding solutions than the
translation method. This report shows that while this is true for some
problems, it is not true in the general case.
Out of three benchmark problems investigated, only two could actually
be solved faster with the new method, the Hamiltonian Cycle Problem
and Quasigroup Completion, where the time taken to find a
solution is roughly half of that of the translation method. In contrast,
for the Round Robin Sports Tournament Problem, the third benchmark problem,
the direct method takes orders of magnitude longer than the translation
method.
Solving Constraint Satisfaction Problems Through Transformation
Mark Minichiello
MMath Computer Science and Mathematics, May 2003
Abstract: One way to solve a constraint satisfaction problem (CSP) is to transform it to SAT and then solve it with a solver for SAT. A recent paper by Ian Gent [1] presents two ways to perform the transformation to SAT and compares on each translation the performance of two solvers --- one based on the Davis-Putnam-Loveland-Logemann procedure and one based on stochastic local search.
In this report, I explore a new way of solving a CSP: to transform it to NB-SAT and then solve it with a solver for NB-SAT.
Many desirable properties of Gent's transformations carry over to the new NB-SAT transformations I propose. Just as arc consistency in the original CSP can be established by unit propagation on the "support" SAT encoding, the same is also true for the new "NB-support" NB-SAT encoding, giving an optimal worst case time algorithm for arc consistency.
I consider the performance of the new translations with two NB-SAT solvers: NB-WalkSAT (based on stochastic local search) and NB-Satz (based on the DPLL procedure). I show that NB-WalkSAT on the NB-SAT transformations performs many times better than WalkSAT on the SAT transformations. None of the transformations give uniformly better performance when using DPLL based procedures.
[1] I. P. Gent, "Arc Consistency in SAT", in Proc. ECAI 2002, (2002).
Resources
Beyond SAT: Exploiting Structure in Walksat
Peter Nightingale
MEng Computer Science, May 2003
Abstract: Many techniques are currently used for solving structured constraint satisfaction problems (CSP), including variants of local search, and translation into other problems. NB-Walksat is a successful algorithm for the non-Boolean propositional satisfiability problem (NB-SAT), and is often used with translated CSPs. This report addresses building constraint expressions (such as all-different or less-than) into NB-Walksat, in place of their NB-SAT encodings. Direct expression of constraints is more compact than the encoding, and allows more focused repairs. The potential benefits are time and space savings, and reduced run length.
Resources
Enforcing Ordering Constraints during Stochastic Local Search
Vincent Armistead
MEng Computer Science, March 2003
Abstract: Stochastic Local Search (SLS) procedures have recently been
proven very effective for solving the propositional Satisfiability
problem (SAT) with many SLS solvers being able to deal with larger
formulas and find satisfying assignments faster than most alternative
systematic searches. This has generated considerable interest because
of the large variety of problems which can be encoded as propositional
formulas. One common feature in the specification of real world
problems is the presence of ordered variables, where setting the value
of one variable effectively restricts the domain of another variable
to ensure that a variable ordering is maintained. The current method
of dealing with these ordering constraints in SAT solvers is naturally
to encode the situation in propositional logic. As the number of
variables and the domain size of these variables increases, encoding
the ordering constraints into SAT requires larger and larger
propositional formulas, and more and more states appear in the search
where the ordering constraints are not maintained.
This report considers an alternative to encoding the ordering
constraints in SAT, instead allowing them to be specified directly,
and then enforcing these constraints to be true throughout the
search. In the report I am able to show through an empirical study
that, for problems where the ordering constraints are critical to
finding a solution, directly specifying and enforcing these ordering
constraints significantly increases the chance of finding a solution,
and significantly decreases the time required to find a solution.
Resources
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/~frisch