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. (C) 2004 Elsevier B.V. All rights reserved.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Compiling problem specifications into SAT|
|Data di pubblicazione:||2005|
|Appartiene alla tipologia:||01a Articolo in rivista|