Vilhelm Dahllöf, Linköping University 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.4143^n) (where n is the number of variables) regardless of i if we allow exponential space. For polynomial space, we present an algorithm solving XiSAT in strictly less than 2^n steps for all i. For i=2, i=3 and i=4 we obtain upper time bounds in O(1.5157^n), O(1.6202^n) and O(1.6844^n), respectively. We also present a dedicated X2SAT algorithm running in polynomial space and time O(1.4511^n).