Declarative Solver Development: Case Studies

Bart Bogaerts, Tomi Janhunen, Shahab Tasharrofi

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

7 Citations (Scopus)


The formalisms for knowledge representation and reasoning (KR&R) typically have a variety of semantics, each one having its particular application scenarios. However, the KR&R community cannot readily benefit from such a variety due toa lack of efficient solver technology. This is partly caused by the fact that solver development is laborious and even accomplishing a working prototype can form a major effort. In this paper, we introduce a new framework that enables us to declaratively specify a given semantics in second-order logic and to automatically generate a solver from that specification. Hence, KR&R researchers can rapidly develop a solver prototype for their new/existing semantics with a minimal effort. Technically, our framework builds on a recent approach for nesting SAT solvers based on lazy clause generation. We evaluate our framework in the context of Dung’s argumentation frameworks, logic programming, and propositional logic subject to standard and non-standard semantics. We show for each of those formalisms that one can easily specify its semantics using a few second-order sentences and that one can effectively obtain a solver for that semantics using our automated solver generation procedure. For instance, in the case of argumentation frameworks, we obtain 16 different solvers, each solving one of four inference tasks for one of four major argumentation semantics and show that our solvers (slightly) outperform the best solver from the last system competition despite not being tuned for argumentation instances.
Original languageEnglish
Title of host publicationFifteenth International Conference on the Principles of Knowledge Representation and Reasoning
Subtitle of host publicationPrinciples of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, {KR} 2016, Cape Town, South Africa, April 25-29, 2016.
EditorsChitta Baral, James Delgrande, Frank Wolter
PublisherAAAI Press
ISBN (Print)978-1-57735-755-1
Publication statusPublished - 2016
MoE publication typeA4 Conference publication
EventInternational Conference on Principles of Knowledge Representation and Reasoning - Cape Town, South Africa
Duration: 25 Apr 201629 Apr 2016
Conference number: 15


ConferenceInternational Conference on Principles of Knowledge Representation and Reasoning
Abbreviated titleKR
Country/TerritorySouth Africa
CityCape Town


Dive into the research topics of 'Declarative Solver Development: Case Studies'. Together they form a unique fingerprint.

Cite this