Writing declarative specifications for clauses

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

Researchers

Research units

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

Abstract

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.

Details

Original languageEnglish
Title of host publicationLogics in Artificial Intelligence - 15th European Conference, JELIA 2016, Proceedings
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

Conference

ConferenceEuropean Conference on Logics in Artificial Intelligence
Abbreviated titleJELIA
CountryCyprus
CityLarnaca
Period09/11/201611/11/2016

ID: 9531020