Minimal model generation with respect to an atom set

Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa

Research output: Contribution to journalConference articlepeer-review

12 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)49-59
Number of pages11
JournalCEUR Workshop Proceedings
Publication statusPublished - Dec 1 2009
Event7th International Workshop on First-Order Theorem Proving, FTP 2009 - Oslo, Norway
Duration: Jul 6 2009Jul 7 2009

All Science Journal Classification (ASJC) codes

  • Computer Science(all)


Dive into the research topics of 'Minimal model generation with respect to an atom set'. Together they form a unique fingerprint.

Cite this