The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

An Isaac Newton Institute Programme

Logic and Algorithms

Modelling in Logic; Solving with SAT

26th June 2006

Author: David Mitchell (Simon Fraser)


he seminal theorem of Fagin states that existential second-order logic (ESO) captures NP. This and other results in descriptive complexity suggest that logics could be viewed as programming languages for their corresponding complexity classes. Despite the conceptual attractiveness, general application of this idea remains far from practical. We describe a project which can be seen as using the idea to produce practical tools for modelling and solving search problems. A problem instance is a finite structure, and a problem specification is a formula defining the relationship between an instance and its solutions. Solving a problem amounts to expanding the structure with new relations (witnessing ESO quantifiers), to satisfy the formula. Finding these is reduced to SAT, or a suitable extension, to take advantage of recent remarkable progress in solver technology. We discuss some progress and problems to date.