SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators

Tomi Janhunen, Shahab Tasharrofi, Eugenia Ternovska

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu


Special-purpose propagators speed up solving logic programs by inferring facts that are hard to deduce otherwise. However, implementing special-purpose propagators is a non-trivial task and requires expert knowledge of solvers. This paper proposes a novel approach in logic programming that allows (1) logical specification of both the problem itself and its propagators and (2) automatic incorporation of such propagators into the solving process. We call our proposed language P[R] and our solver SAT-to-SAT because it facilitates communication between several SAT solvers. Using our proposal, non-specialists can specify new reasoning methods (propagators) in a declarative fashion and obtain a solver that benefits from both state-of-the-art techniques implemented in SAT solvers as well as problem-specific reasoning methods that depend on the problem's structure. We implement our proposal and show that it outperforms the existing approach that only allows modeling a problem but does not allow modeling the reasoning methods for that problem.
OtsikkoProceedings of the Thirtieth AAAI Conference on Artificial Intelligence (AAAI-16)
KustantajaAAAI PRESS
TilaJulkaistu - 2016
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaAAAI Conference on Artificial Intelligence - Phoenix, Yhdysvallat
Kesto: 12 helmikuuta 201617 helmikuuta 2016
Konferenssinumero: 30


ISSN (painettu)2374-3468


ConferenceAAAI Conference on Artificial Intelligence

Sormenjälki Sukella tutkimusaiheisiin 'SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä