47 citations · 92 across the 12 of their papers we have counts for
8 papers · 1 filter
Extended Resolution Clause Learning via Dual Implication Points
Sam Buss, Jonathan Chung, Vijay Ganesh +1
We present a new extended resolution clause learning (ERCL) algorithm, implemented as part of a conflict-driven clause-learning (CDCL) SAT solver, wherein new variables are dynamic…
Regular resolution effectively simulates resolution
Sam Buss, Emre Yolcu
Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist…
Sub-computable Boundedness Randomness
Sam Buss, Douglas Cenzer, Jeffrey B. Remmel
This paper defines a new notion of bounded computable randomness for certain classes of sub-computable functions which lack a universal machine. In particular, we define such versi…
Small Stone in Pool
Samuel R. Buss, Leszek Aleksander Kolodziejczyk
The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polyn…
Improved Separations of Regular Resolution from Clause Learning Proof Systems
Maria Luisa Bonet, Sam Buss, Jan Johannsen
We prove that the graph tautology formulas of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned c…
An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning
Maria Luisa Bonet, Sam Buss
We prove that the graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned…