19 citations · 19 across the 4 of their papers we have counts for
5 papers
Associativity of Multiplication Is Hard for Resolution
Vincent Liew
SAT solvers are empirically known to perform poorly when reasoning about multiplication. Yet for over a decade we have lacked a theoretical explanation for this phenomenon. CDCL SA…
Proofdoors and Efficiency of CDCL Solvers
Sunidhi Singh, Vincent Liew, Marc Vinyals +1
We propose a new parameter called proofdoor in an attempt to explain the efficiency of CDCL SAT solvers over a certain class of formulas derived from circuit (esp., arithmetic) ver…
Towards Verifying Nonlinear Integer Arithmetic
Paul Beame, Vincent Liew
We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properti…
New Limits for Knowledge Compilation and Applications to Exact Model Counting
Paul Beame, Vincent Liew
We show new limits on the efficiency of using current techniques to make exact probabilistic inference for large classes of natural problems. In particular we show new lower bounds…
Finding the Median (Obliviously) with Bounded Space
Paul Beame, Vincent Liew, Mihai Pǎtraşcu
We prove that any oblivious algorithm using space to find the median of a list of integers from requires time . This bound also applies to…