Writing declarative specifications for clauses

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu



  • Institute for Informatics and Computational Science
  • University of Potsdam
  • INRIA Rennes - Bretagne Atlantique


Modern satisfiability (SAT) solvers provide an efficient implementation of classical propositional logic. Their input language, however, is based on the conjunctive normal form (CNF) of propositional formulas. To use SAT solver technology in practice, a user must create the input clauses in one way or another. A typical approach is to write a procedural program that generates formulas on the basis of some input data relevant for the problem domain and translates them into CNF. In this paper, we propose a declarative approach where the intended clauses are specified in terms of rules in analogy to answer set programming (ASP). This allows the user to write first-order specifications for intended clauses in a schematic way by exploiting term variables. We develop a formal framework required to define the semantics of such specifications. Moreover, we provide an implementation harnessing stateof-the-art ASP grounders to accomplish the grounding step of clauses. As a result, we obtain a general-purpose clause-level grounding approach for SAT solvers. Finally, we illustrate the capabilities of our specification methodology in terms of combinatorial and application problems.


OtsikkoLogics in Artificial Intelligence - 15th European Conference, JELIA 2016, Proceedings
TilaJulkaistu - 2016
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaEuropean Conference on Logics in Artificial Intelligence - Larnaca, Kypros
Kesto: 9 marraskuuta 201611 marraskuuta 2016
Konferenssinumero: 15


NimiLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vuosikerta10021 LNAI
ISSN (painettu)03029743
ISSN (elektroninen)16113349


ConferenceEuropean Conference on Logics in Artificial Intelligence

ID: 9531020