skip to content

Modelling in logic; solving with SAT

Monday 26th June 2006 - 11:00 to 12:00
INI Seminar Room 2

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.

University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons