47 citations · 92 across the 12 of their papers we have counts for
14 papers
Herbrand Game Complexity
Sam Buss, Pavel Pudlák
The Student-Teacher game is an extension of Herbrand's theorem. In the game, Student and Teacher take turns giving values for existentially and universally quantified variables, an…
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…
On the Consistency of Circuit Lower Bounds for Non-Deterministic Time
Albert Atserias, Sam Buss, Moritz Müller
We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory…
Proof complexity of systems of (non-deterministic) decision trees and branching programs
Sam Buss, Anupam Das, Alexander Knop
This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs - deterministic and nondeterministic. The systems LDT and LNDT ar…
Strategies for Stable Merge Sorting
Sam Buss, Alexander Knop
We introduce new stable natural merge sort algorithms, called -merge sort and -merge sort. We prove upper and lower bounds for several merge sort algorithms, including Timsor…