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&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.