Writing declarative specifications for clauses

Martin Gebser, Tomi Janhunen*, Roland Kaminski, Torsten Schaub, Shahab Tasharrofi

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

2 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationLogics in Artificial Intelligence - 15th European Conference, JELIA 2016, Proceedings
PublisherSpringer Verlag
Number of pages16
Volume10021 LNAI
ISBN (Print)9783319487571
Publication statusPublished - 2016
MoE publication typeA4 Article in a conference publication
EventEuropean Conference on Logics in Artificial Intelligence - Larnaca, Cyprus
Duration: 9 Nov 201611 Nov 2016
Conference number: 15

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10021 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349


ConferenceEuropean Conference on Logics in Artificial Intelligence
Abbreviated titleJELIA

Fingerprint Dive into the research topics of 'Writing declarative specifications for clauses'. Together they form a unique fingerprint.

Cite this