On tackling the limits of resolution in SAT solving

DOI10.1007/978-3-319-66263-3_11zbMath1496.68368arXiv1705.01477OpenAlexW2963321374MaRDI QIDQ1680253

Alexey Ignatiev, Antonio Morgado, João P. Marques-Silva

Publication date: 15 November 2017

Full work available at URL: https://arxiv.org/abs/1705.01477

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Related Items (6)

Learning a propagation complete formula ⋮ MaxSAT resolution for regular propositional logic ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Bounds on the size of PC and URC formulas ⋮ Propositional proof systems based on maximum satisfiability ⋮ MaxSAT Resolution and Subcube Sums

Uses Software

• CPLEX
• PicoSAT
• Sat4j
• QMaxSAT
• Open-WBO
• LMHS

This page was built for publication: On tackling the limits of resolution in SAT solving