David G. Mitchell (Simon Fraser University), Modelling with FO(ID); Solving with SAT

The development of effective solver technology has made reduction to SAT an attractive method for solving a variety hard search problems. The approach has been very successful in hardware verification, which provided the driving force behind much recent development of SAT technology, and where SAT-based tools are now widely used.

Unfortunately, the broad application of this approach is impaired by the poor modelling capability of propositional CNF formulas, which is the input language for most SAT solvers. Many approaches to extending the methodology to more expressive constraint languages can be found. However, no satisfactory general framework has emerged.

We describe an approach to solving search problems in which problems are modelled in classical first-order logic extended with (non-monotone) inductive definitions, and solved by reduction to (extended) SAT. We give evidence that the approach is general, natural, and can be effective in practice, discuss some of the progress that has been made on tackling problems in modelling and solving of problems, and discuss some of the many remaining challenges.