Constrained pseudo-propositional logic (Q2228353)

The authors consider the constrained pseudo-propositional logic (CPPL), based on pseudo-propositional logic, formulating counting constraints naturally, but keeping its Boolean nature preserved. CPPL is capable of encoding counting constraints, as well as SAT instances, much more succinctly than having them being encoded using conjunctive normal form. Solving SAT problem in CPPL allows for assigning truth values to a variety of propositional variables simultaneously. The resulting calculus in CPPL is similar to the cutting planes proof systems, but in distinction to it, CPPL does not require the set of linear inequalities to be finite. Although this restriction is made dispensable, CPPL is maintained to be sound and complete.