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.

Special-purpose propagators speed up solving logic programs by inferring facts that are hard to deduce otherwise. However, implementing special-purpose propagators is a non-trivial task and requires expert knowledge of solvers. This paper proposes a novel approach in logic programming that allows (1) logical specification of both the problem itself and its propagators and (2) automatic incorporation of such propagators into the solving process. We call our proposed language P [ R ] and our solver SAT-to-SAT because it facilitates communication between several SAT solvers. Using our proposal, non-specialists can specify new reasoning methods (propagators) in a declarative fashion and obtain a solver that benefits from both state-of-the-art techniques implemented in SAT solvers as well as problem-specific reasoning methods that depend on the problem's structure. We implement our proposal and show that it outperforms the existing approach that only allows modeling a problem but does not allow modeling the reasoning methods for that problem.

Recent work by Janhunen, Tasharrofi, and Ternovska (2016) started from the following observation: "if SAT From the result of this oracle call, a learned clause is generated and added to ϕ. Now that formalism; (2) It can be immediately combined with other these highly-performant SATsolvers exist, research often SAT extensions (such as integer variables, acyclicity, or any stretches beyond SAT, either because of trying to tackle other theory propagator); (3) No dedicated propagators need problems of a complexity higher than NP or because the input to be developed for the new extension because the nested format of SAT solvers (propositional logic) is too limited solver is (automatically) used as a propagator for its internal to concisely and naturally express certain domain specific theory; for example, it was shown by Janhunen, Tasharrofi, constraints, such as graph properties.