Solving Non-Boolean Satisfiability Problems

Alan Frisch

(York University)

State-of-the-art procedures for determining the satisfiability of formulas of Boolean logic have developed to the point where they can solve problem instances that are large enough to be of practical importance. Many of the problems on which satisfiability procedures have been effective are non-Boolean in that they are most naturally formulated in terms of variables with domain sizes greater than two. Boolean satisfiability procedures have been applied to these non-Boolean problems by reformulating the problem with Boolean variables. An alternative, previously unexplored approach, is to generalise satisfiability procedures to handle non-Boolean formulas directly. This talk compares these two approaches.

We begin by presenting two procedures that we have developed for solving non-Boolean formulas directly. We also present three methods for systematically transforming non-Boolean formulas to Boolean formulas. Finally, experimental results are reported on using all these methods to solve random formulas, graph colouring problems and planning problems.
Tuesday 27th May 2003, 14:00
Robert Recorde Room
Department of Computer Science