Unrestricted vs restricted cut in a tableau method for Boolean circuits

DOI10.1007/s10472-005-7034-1zbMath1086.03048OpenAlexW2061876041MaRDI QIDQ812394

Tommi Junttila, Matti Järvisalo, Ilkka Niemelä

Publication date: 23 January 2006

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-005-7034-1

zbMATH Keywords

satisfiabilitycut ruletableau methodproof complexityBoolean circuitsDPLL

Mathematics Subject Classification ID

Related Items (7)

Implementing Preferences with asprin ⋮ Algorithms for Solving Satisfiability Problems with Qualitative Preferences ⋮ Solving satisfiability problems with preferences ⋮ A general framework for preferences in answer set programming ⋮ Limitations of Restricted Branching in Clause Learning ⋮ Limitations of restricted branching in clause learning ⋮ On Exponential Lower Bounds for Partially Ordered Resolution

Uses Software

• Walksat
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• A structure-preserving clause form translation
• A deterministic \((2-2/(k+1))^{n}\) algorithm for \(k\)-SAT based on local search.
• The Efficiency of Resolution and Davis--Putnam Procedures
• The Taming of the Cut. Classical Refutations with Analytic Cut
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Principles and Practice of Constraint Programming – CP 2004
• Bounded model checking using satisfiability solving

This page was built for publication: Unrestricted vs restricted cut in a tableau method for Boolean circuits