This paper studies minimal model generation for SAT instances. In this study, we minimize models with respect to an atom set, and not to the whole atom set. In order to enumerate minimal models, we use an arbitrary SAT solver as a subroutine which returns models of satisfiable SAT instances. In this way, we benefit from the year-byyear progress of efficient SAT solvers for generating minimal models. As an application, we try to solve job-shop scheduling problems by encoding them into SAT instances whose minimal models represent optimum solutions.
|Number of pages||11|
|Journal||CEUR Workshop Proceedings|
|Publication status||Published - Dec 1 2009|
|Event||7th International Workshop on First-Order Theorem Proving, FTP 2009 - Oslo, Norway|
Duration: Jul 6 2009 → Jul 7 2009
All Science Journal Classification (ASJC) codes
- Computer Science(all)