On Linear Resolution
type: Item
instance of: scholarly article
title: On Linear Resolution
zbMATH Open document ID: 1484.03120
DOI: 10.3233/SAT190112
author: Jan Johannsen
author: Samuel R. Buss
published in: Journal on Satisfiability, Boolean Modeling and Computation
publication date: 2021-12-09T00:00:00Z
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 7441857
zbMATH Keywords: s-resolution
zbMATH Keywords: linear resolution
zbMATH Keywords: tree-like resolution
zbMATH Keywords: regular resolution
zbMATH Keywords: proof complexity
MaRDI profile type: MaRDI publication profile
cites work: Q3002781
cites work: Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
cites work: Q5715680
cites work: Separation results for the size of constant-depth propositional proofs
cites work: Q5503674
cites work: An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
cites work: Improved Separations of Regular Resolution from Clause Learning Proof Systems
cites work: Optimality of size-width tradeoffs for resolution
cites work: The complexity of resolution refinements
cites work: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
cites work: Optimality of size-degree tradeoffs for polynomial calculus
cites work: An Exponential Lower Bound for Width-Restricted Clause Learning
cites work: Linear resolution with selection function
cites work: Short proofs for tricky formulas
cites work: Q5600875
cites work: Q5619635
cites work: GRASP: a search algorithm for propositional satisfiability
cites work: Q4282522
cites work: On the power of clause-learning SAT solvers as resolution engines
cites work: A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
cites work: Short resolution proofs for a sequence of tricky formulas
cites work: Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
cites work: The relative complexity of analytic tableaux and SL-resolution
cites work: Q5639372
description: scientific article; zbMATH DE number 7441857