9 citations · 19 across the 10 of their papers we have counts for
12 papers
On the trivial units property and the unique product property
Heiko Dietrich, Melissa Lee, Andre Nies +1
We report on some computational experiments related to the trivial units property and unique product property for group rings of torsion-free groups. These properties are related t…
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…
An Exponential Separation between Deterministic CDCL and DPLL Solvers
Sahil Samar, Marc Vinyals, Vijay Ganesh
We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instance…
Hardness of Approximation in PSPACE and Separation Results for Pebble Games
Siu Man Chan, Massimo Lauria, Jakob Nordström +1
We consider the pebble game on DAGs with bounded fan-in introduced in [Paterson and Hewitt '70] and the reversible version of this game in [Bennett '89], and study the question of…
Limits of CDCL Learning via Merge Resolution
Marc Vinyals, Chunxiao Li, Noah Fleming +2
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. Howeve…
Proving Unsatisfiability with Hitting Formulas
Yuval Filmus, Edward A. Hirsch, Artur Riazanov +2
Hitting formulas have been studied in many different contexts at least since [Iwama,89]. A hitting formula is a set of Boolean clauses such that any two of them cannot be simultane…
Irreducible subcube partitions
Yuval Filmus, Edward Hirsch, Sascha Kurz +4
A \emph{subcube partition} is a partition of the Boolean cube into subcubes. A subcube partition is irreducible if the only sub-partitions whose union is a subcube are…
On the Hierarchical Community Structure of Practical Boolean Formulas
Chunxiao Li, Jonathan Chung, Soham Mukherjee +5
Modern CDCL SAT solvers easily solve industrial instances containing tens of millions of variables and clauses, despite the theoretical intractability of the SAT problem. This gap…
Complexity Measures on the Symmetric Group and Beyond
Neta Dafni, Yuval Filmus, Noam Lifshitz +2
We extend the definitions of complexity measures of functions to domains such as the symmetric group. The complexity measures we consider include degree, approximate degree, decisi…
MaxSAT Resolution and Subcube Sums
Yuval Filmus, Meena Mahajan, Gaurav Sood +1
We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weaken…
Towards a Complexity-theoretic Understanding of Restarts in SAT solvers
Chunxiao Li, Noah Fleming, Marc Vinyals +2
Restarts are a widely-used class of techniques integral to the efficiency of Conflict-Driven Clause Learning (CDCL) Boolean SAT solvers. While the utility of such policies has been…
From Small Space to Small Width in Resolution
Yuval Filmus, Massimo Lauria, Mladen Mikša +2
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of CNF formulas is always an upper bound on…