Mining propositional simplification proofs for small validating clauses

MaRDI QIDQ2848691zbMATH OpenFDO

Authors Ian Wehrman, Aaron Stump

Publication date 26 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066106000090

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Grammars and rewriting systems (68Q42)

Recommendations

• NP-completeness of small conflict set generation for congruence closure
• Two techniques for minimizing resolution proofs
• Generalized conflict-clause strengthening for satisfiability solvers
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• An efficient and flexible approach to resolution proof reduction

Cited in

(4)

• Multi-completion with termination tools
• Propositional Satisfiability Algorithm to Find Minimal Reducts for Data Mining
• A lower bound of the number of rewrite rules obtained by homological methods
• Extending Maximal Completion (Invited Talk)

Describes a project that uses

Uses Software

• CVC Lite
• CVC

This page was built for publication: Mining propositional simplification proofs for small validating clauses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848691)