Constrained pseudo-propositional logic
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.
- Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
- scientific article; zbMATH DE number 204193 (Why is no real title available?)
- In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
- New Encodings of Pseudo-Boolean Constraints into CNF
- On the complexity of cutting-plane proofs
- The complexity of theorem-proving procedures
This page was built for publication: Constrained pseudo-propositional logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2228353)
