Minimal model generation with respect to an atom set

Miyuki Koshimura, Hidetomo Nabeshima, Hiroshi Fujita, Ryuzo Hasegawa

Research output: Contribution to journalConference article

8 Citations (Scopus)

Abstract

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
Volume556
Publication statusPublished - Dec 1 2009
Event7th International Workshop on First-Order Theorem Proving, FTP 2009 - Oslo, Norway
Duration: Jul 6 2009Jul 7 2009

Fingerprint

Atoms
Subroutines

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Cite this

Minimal model generation with respect to an atom set. / Koshimura, Miyuki; Nabeshima, Hidetomo; Fujita, Hiroshi; Hasegawa, Ryuzo.

In: CEUR Workshop Proceedings, Vol. 556, 01.12.2009, p. 49-59.

Research output: Contribution to journalConference article

Koshimura, Miyuki ; Nabeshima, Hidetomo ; Fujita, Hiroshi ; Hasegawa, Ryuzo. / Minimal model generation with respect to an atom set. In: CEUR Workshop Proceedings. 2009 ; Vol. 556. pp. 49-59.
@article{0f9daaf893274253b9ad2421d1900be1,
title = "Minimal model generation with respect to an atom set",
abstract = "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.",
author = "Miyuki Koshimura and Hidetomo Nabeshima and Hiroshi Fujita and Ryuzo Hasegawa",
year = "2009",
month = "12",
day = "1",
language = "English",
volume = "556",
pages = "49--59",
journal = "CEUR Workshop Proceedings",
issn = "1613-0073",

}

TY - JOUR

T1 - Minimal model generation with respect to an atom set

AU - Koshimura, Miyuki

AU - Nabeshima, Hidetomo

AU - Fujita, Hiroshi

AU - Hasegawa, Ryuzo

PY - 2009/12/1

Y1 - 2009/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84888230407&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84888230407&partnerID=8YFLogxK

M3 - Conference article

VL - 556

SP - 49

EP - 59

JO - CEUR Workshop Proceedings

JF - CEUR Workshop Proceedings

SN - 1613-0073

ER -