Applications of general exact satisfiability in propositional logic modelling

Abstract

There is a trend to study extended variants of propositional logic which have explicit means to represent cardinality constraints. That is accomplished using so-called c-atoms. We show that c-atoms can be efficiently reduced to a general form of Exact Satisfiability. The general XiSAT problem is to find an assignment for a CNF such that exactly i literals are true in each clause for any i ≥ 1. We show that this problem is solvable in time O(1.4143n) (where n is the number of variables) regardless of i if we allow exponential space. For polynomial space, we present an algorithm solving XiSAT for all i strictly better than the trivial O(2n) bound. For i = 2, i = 3 and i = 4 we obtain upper time bounds in O(1.5157 n), O(1.6202n) and O(1.6844n), respectively. We also present a dedicated X2SAT algorithm running in polynomial space and time O(1.4511n). © Springer-Verlag Berlin Heidelberg 2005.