On linear resolution

DOI10.3233/SAT190112MaRDI QIDQ5015599zbMATH OpenFDO

Authors Jan Johannsen, Samuel R. Buss

Publication date 9 December 2021

Published in Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/SAT190112

zbMATH Keywords

linear resolutionproof complexityregular resolutions-resolutiontree-like resolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• Short proofs are narrow—resolution made simple
• Short proofs are narrow -- resolution made simple
• Resolution over linear equations and multilinear proofs
• On resolution strategies with weak factorization
• Linear semi-look resolution

Cites work

• A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
• An Exponential Lower Bound for Width-Restricted Clause Learning
• An improved separation of regular resolution from pool resolution and clause learning
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 5899257 (Why is no real title available?)
• scientific article; zbMATH DE number 517000 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 3320385 (Why is no real title available?)
• scientific article; zbMATH DE number 3343519 (Why is no real title available?)
• scientific article; zbMATH DE number 3366543 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Improved separations of regular resolution from clause learning proof systems
• Linear resolution with selection function
• On the power of clause-learning SAT solvers as resolution engines
• Optimality of size-degree tradeoffs for polynomial calculus
• Optimality of size-width tradeoffs for resolution
• Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Separation results for the size of constant-depth propositional proofs
• Short proofs for tricky formulas
• Short resolution proofs for a sequence of tricky formulas
• The complexity of resolution refinements
• The relative complexity of analytic tableaux and SL-resolution

Cited in

(9)

• Array resolutions of linear maps
• Linear semi-look resolution
• Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning
• scientific article; zbMATH DE number 1614709 (Why is no real title available?)
• scientific article; zbMATH DE number 3982556 (Why is no real title available?)
• scientific article; zbMATH DE number 1769205 (Why is no real title available?)
• On the Capacity of the Precision-Resolution System
• Regular resolution effectively simulates resolution
• Linearity and regularity with negation normal form

This page was built for publication: On linear resolution

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