Two techniques for minimizing resolution proofs

DOI10.1007/978-3-642-14186-7_26MaRDI QIDQ4930598zbMATH OpenOpenAlexFDO

Authors Scott Cotton

Publication date 29 September 2010

Published in Theory and Applications of Satisfiability Testing – SAT 2010 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14186-7_26

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• An efficient and flexible approach to resolution proof reduction
• Resolution proof transformation for compression and interpolation
• Improved single pass algorithms for resolution proof reduction
• Data compression for proof replay
• Minimizing models for Tseitin-encoded SAT instances

Cited in

(13)

• Data compression for proof replay
• Efficient algorithms to detect and restore minimality, an extension of the regular restriction of resolution
• Parallelizing SMT solving: lazy decomposition and conciliation
• Mining propositional simplification proofs for small validating clauses
• Implementation and evaluation of contextual natural deduction for minimal logic
• Boundary Points and Resolution
• On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\)
• Improved single pass algorithms for resolution proof reduction
• Resolution proof transformation for compression and interpolation
• Compression of propositional resolution proofs via partial regularization
• Minimizing models for Tseitin-encoded SAT instances
• An efficient and flexible approach to resolution proof reduction
• Optimization techniques for Craig interpolant compaction in unbounded model checking

Describes a project that uses

Uses Software

• MiniSat
• PicoSAT

This page was built for publication: Two techniques for minimizing resolution proofs

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