Optimal length tree-like resolution refutations for 2SAT formulas

DOI10.1145/976706.976711MaRDI QIDQ5277698zbMATH OpenOpenAlexFDO

Authors

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/976706.976711

zbMATH Keywords

2SAT formulasresolutiontree-like proofs

Mathematics Subject Classification ID

Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• scientific article; zbMATH DE number 1955763
• Minimum Witnesses for Unsatisfiable 2CNFs
• Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
• Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
• Parameterized and Exact Computation

Cited in

(8)

• Finding read-once resolution refutations in systems of 2CNF clauses
• Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
• Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• Efficient arbitrary and resolution proofs of unsatisfiability for restricted tree-width
• scientific article; zbMATH DE number 640293 (Why is no real title available?)
• scientific article; zbMATH DE number 1955763 (Why is no real title available?)
• Minimum Witnesses for Unsatisfiable 2CNFs

This page was built for publication: Optimal length tree-like resolution refutations for 2SAT formulas

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