2 papers
math.LO2026
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…
cs.LO2026
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…