Much excitement has been generated by rapid recent progress in solving SAT problems, both by systematic search procedures, such as the Davis-Putnam procedure and--rather surprisingly--by stochastic local search procedures (see below). Some methods can now routinely solve problems involving hundreds of variables, which is nothing short of astounding when one considers that the difficulty of SAT increases exponentially with the number of variables. This rapid advance has also led many researchers to apply SAT solvers to a wider range of problems including constraint-based planning, verification of hardware and software, circuit synthesis and diagnosis, scheduling, and problems in finite algebra.
Local search procedures operate by moving through a space of potential solutions to a problem guided by a heuristic that at each point chooses what appears to be the best move from among the alternatives. It has been found that such a procedure performs much better if at each step, with a predetermined probability (called the noise setting), it ignores the heuristic and randomly chooses a move from among the set of alternatives [2].
The formulas of propositional logic, which are involved in SAT, are said to be Boolean in that they can take on two possible values: TRUE and FALSE. But many naturally-occurring problems are non-Boolean, that is they are most naturally formulated in terms of variables with domain sizes greater than two. For example, in the problem of timetabling the university's courses, a particular lecture can be thought of as a variable that must be assigned a value from among the set of 50 weekly teaching slots.
The typical way to solve a non-Boolean problem is to translate it to an equivalent Boolean problem. An alternative method is to generalise Boolean SAT techniques to operate directly on non-Boolean problems [1]. The results of Tim Peugniez's project (1997-8) show that a local search procedure, NB-Walsksat, that operates directly on a non-Boolean formula, F, can outperform the corresponding procedure, Walksat, operating on a Boolean translation of F [1]. This work has been published in a the leading international conference on artificial intelligence. Furthermore, Peter Stock's project (1999-2000) shows similar benefits can be obtained by generalizing the Davis-Putnam procedure to handle non-Boolean formulas and Matthew Slack's project (1999-2000) shows how these benefits can be exploited to solve planning problems.
Each of these six projects can provide the excitement that comes with attempting to advance the state of the art. The results of these projects will be of interest to a community of researchers working in the area, so it is hoped that the products of the projects will be put on the internet as a resource for this community. A well-executed project has a good chance of leading to publication.
Previous student projects (Thand, 2002; Armistead, 2003; Nightingale, 2003) have built local search NB-SAT solvers that try to exploit problem structure. Each of these has approached the problem by extending NB-Walksat to handle NB-SAT problems that have been generalised to allow the expression of certain other constraints (e.g., that one variable must be assigned a larger value than another).
This project will attempt another approach to exploit problem structure in stochastic local search. In this approach the language of NB-SAT will not be generalized; instead the formulas will be annotated with information that reflects problem structure, which the solver can then use to influence its search strategy. For example, a set of clauses that arises from a single problem constraint could be grouped together, and when the solver selects the group for repair, it would focus its efforts solely on satisfying the group. Another possibility would be to introduce a hierarchical structure to a local search SAT solver, fixing one level of constraints before the lower level, then the search space at the lower level should be considerably smaller and less complex. If in fixing lower level constraints a higher level constraint is violated, the search will move back up to the higher level.
This project will involve designing search strategies such as the above, extending NB-Walksat to implement these strategies, and experimentally comparing their effectiveness to the original NB-Walksat.
Certain software will be made available to the student, including NB-Walsksat
and a suite of programs for translating various problems into NB-SAT.
McAllester, Selman and Kautz [1] argued that a certain invariance (henceforth called the "the MSK invariance") holds between the optimal noise setting for a problem instance and certain parameters that can measured on short executions of the algorithm on the instance. Furthermore, they conjectured that the MSK invariance could be exploited by a system to automatically set its noise parameter.
Anthony Doggett's undergraduate project [2] examined the MSK invariance and gave some experimental evidence that strongly suggested that in many cases the invariance doesn't hold. On the other hand, Henry Kautz and Don Patterson [3] have implemented a version Walksat, called Auto-Walksat, that uses the MSK invariance to automatically set its noise parameter and they have reported on its success.
The goal of this project is to reconcile these two apparently-contradictory assessments of the MSK invariance. Is it simply, that the two assessments look at different problem classes? If so, can the problem classes for which the MSK invariance holds be characterised? Or is it that the two assessments interpret the statement of the invariance differently? Whatever the case, it is likely that further experiments will be needed to clarify the situation.
A student undertaking this project will have access to Walksat, Auto-Walksat, problem instances and problem generators.
This problem is similar, but not identical, to the problem of assigning referees to review papers submitted to a conference. Software for automatically solving this problem is publically available. Perhaps the most popular system is the open-source system START. This project will start by studying a system such as START in order to understand its allocation algorithm and to access whether the system, or parts of it, can be adapted to the project allocation problem.
If undertaken by an MScIP student, this project could focus more
on developing interfaces and evaluating existing systems.
Non-Boolean SAT instances can be solved either directly by NB-WalkSat, or by transforming the instance to Boolean formula and using WalkSat. In the transformation approach, a preprocessor could be used on the before transformation (on the non-Boolean formula) or after transformation (on the Boolean formula). The central aim of this project will be to compare these two approaches to preprocessing. Through analysis, the two kinds of inference will be related and, through experiment, the effect of preprocessing on the efficiency of subsequent search will be considered.
A Boolean and Non-Boolean preprocessor will be made available to the
student undertaking this project. The project may entail extending
these preprocessors with new inference rules.