: Compiling problem specifications into SAT

11 years 6 months ago
: Compiling problem specifications into SAT
We present a compiler that translates a problem specification into a propositional satisfiability test (SAT). Problems are specified in a logic-based language, called NP-SPEC, which allows the definition of complex problems in a highly declarative way, and whose expressive power is such as to capture all problems which belong to the complexity class NP. The target SAT instance is solved using any of the various state-of-the-art solvers available from the community. The system obtained is an executable specification language for all NP problems which shows interesting computational properties. The performance of the system has been tested on a few classical problems, namely graph coloring, Hamiltonian cycle, job-shop scheduling, and on a real-world scheduling application, namely the tournament scheduling problem. 2004 Elsevier B.V. All rights reserved.
Marco Cadoli, Andrea Schaerf
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where AI
Authors Marco Cadoli, Andrea Schaerf
Comments (0)