Unrestricted vs restricted cut in a tableau method for Boolean circuits
From MaRDI portal
Publication:812394
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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
