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.
Compiling problem specifications into SAT
SCHAERF, Andrea
2005-01-01
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
science.pdf
non disponibili
Tipologia:
Altro materiale allegato
Licenza:
Non pubblico
Dimensione
252.42 kB
Formato
Adobe PDF
|
252.42 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.