Propositional satisfiability in answer-set programming

We show that propositional logic and its extensions can support answer-set programming in the same way stable logic programming and disjunctive logic programming do. To this end, we introduce a logic based on the logic of propositional schemata and on a version of the Closed World Assumption. We call it the extended logic of propositional schemata with CWA (PS⁺, in symbols). An important feature of the logic PS⁺ is that it supports explicit modeling of constraints on cardinalities of sets. In the paper, we characterize the class of problems that can be solved by finite PS⁺ theories. We implement a programming system based on the logic PS⁺ and design and implement a solver for processing theories in PS⁺. We present encouraging performance results for our approach — we show it to be competitive with smodels, a state-of-the-art answer-set programming system based on stable logic programming.