Declarative Solver Development: Case Studies

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&Rcommunity cannot readily benefit from such a variety due toa lack of efficient solver technology. This is partly caused bythe 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 todeclaratively specify a given semantics in second-order logicand to automatically generate a solver from that specification. Hence, KR&R researchers can rapidly develop a solverprototype for their new/existing semantics with a minimal effort. Technically, our framework builds on a recent approachfor nesting SAT solvers based on lazy clause generation.We evaluate our framework in the context of Dung’s argumentation frameworks, logic programming, and propositionallogic subject to standard and non-standard semantics. Weshow for each of those formalisms that one can easily specify its semantics using a few second-order sentences and thatone can effectively obtain a solver for that semantics usingour automated solver generation procedure.For instance, in the case of argumentation frameworks, weobtain 16 different solvers, each solving one of four inference tasks for one of four major argumentation semantics andshow that our solvers (slightly) outperform the best solverfrom the last system competition despite not being tuned forargumentation instances.