Modelling in logic; solving with SAT
Seminar Room 2, Newton Institute Gatehouse
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.