arXiv subjects

Marc Vinyals

Publications and source records attributed to Marc Vinyals.

13 recordsLinked to original sources

arXiv2026

Proofdoors and Efficiency of CDCL Solvers

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) verification applications. Informally, given an unsatisfiable CNF formula F over n variables, a proofdoor decomposition consists of a chunking of the clauses into A_1, ..., A_k together with a sequence of interpolants connecting these chunks. Intuitively, a proofdoor captures the idea that an unsatisfiable formula can be refuted by reasoning chunk by chunk, while maintaining only a summary of the information (i.e., interpolants) gained so far for subsequent reasoning steps. We prove several theorems in support of the proposition that proofdoors can explain the efficiency of CDCL solvers for some class of circuit verification problems. First, we show that formulas with small proofdoors (i.e., where each interpolant is O(n) sized, each chunk A_i has small pathwidth, and each interpolant clause has at most O(log n) backward dependency on the previous interpolant) have short resolution (Res) proofs, and a certain configuration of CDCL solvers can compute such proofs in time polynomial in n. Second, we show that commutativity (miter) formulas over floating-point addition have small proofdoors and hence short Res proofs, even though they have large pathwidth. Third, we identify limits of the proofdoor framework: we show that a poor decomposition of arithmetic miter instances can force exponentially large interpolants, and hence our framework derives exponentially large Res refutations from such a decomposition, even when a different decomposition (i.e., a small proofdoor) yields short proofs. As a byproduct, these interpolant lower bounds imply new lower bounds for the partially ordered resolution proof system.

cs.CC↗

arXiv2026

On the trivial units property and the unique product property

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 to Kaplansky's unit and zero-divisor conjectures. Our investigations include a classification of certain symmetric non-trivial units in the binary group ring of the Hantzsche-Wendt group; this group was used in Gardam's refutal of Kaplansky's unit conjecture. We also exhibit and investigate a new candidate group that fails the unique units property but may satisfy the trivial unit property. No examples of groups with these properties are known to date.

math.GR↗

arXiv2026

An Exponential Separation between Deterministic CDCL and DPLL Solvers

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 instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.

cs.CC↗

arXiv2023

Hardness of Approximation in PSPACE and Separation Results for Pebble Games

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 how hard it is to decide exactly or approximately the number of pebbles needed for a given DAG in these games. We prove that the problem of eciding whether $s$~pebbles suffice to reversibly pebble a DAG $G$ is PSPACE-complete, as was previously shown for the standard pebble game in [Gilbert, Lengauer and Tarjan '80]. Via two different graph product constructions we then strengthen these results to establish that both standard and reversible pebbling space are PSPACE-hard to approximate to within any additive constant. To the best of our knowledge, these are the first hardness of approximation results for pebble games in an unrestricted setting (even for polynomial time). Also, since [Chan '13] proved that reversible pebbling is equivalent to the games in [Dymond and Tompa '85] and [Raz and McKenzie '99], our results apply to the Dymond--Tompa and Raz--McKenzie games as well, and from the same paper it follows that resolution depth is PSPACE-hard to determine up to any additive constant. We also obtain a multiplicative logarithmic separation between reversible and standard pebbling space. This improves on the additive logarithmic separation previously known and could plausibly be tight, although we are not able to prove this. We leave as an interesting open problem whether our additive hardness of approximation result could be strengthened to a multiplicative bound if the computational resources are decreased from polynomial space to the more common setting of polynomial time.

cs.CC↗

arXiv2023

Limits of CDCL Learning via Merge Resolution

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. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.

cs.CC↗

arXiv2023

Proving Unsatisfiability with Hitting Formulas

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 simultaneously falsified. [Peitl,Szeider,05] conjectured that hitting formulas should contain the hardest formulas for resolution. They supported their conjecture with experimental findings. Using the fact that hitting formulas are easy to check for satisfiability we use them to build a static proof system Hitting: a refutation of a CNF in Hitting is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. We show that tree-like resolution and Hitting are quasi-polynomially separated. We prove that Hitting is quasi-polynomially simulated by tree-like resolution, thus hitting formulas cannot be exponentially hard for resolution, so Peitl-Szeider's conjecture is partially refuted. Nevertheless Hitting is surprisingly difficult to polynomially simulate. Using the ideas of PIT for noncommutative circuits [Raz-Shpilka,05] we show that Hitting is simulated by Extended Frege. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in a deterministic polynomial time. We consider multiple extensions of Hitting. Hitting(+) formulas are conjunctions of clauses containing affine equations instead of just literals, and every assignment falsifies at most one clause. The resulting system is related to Res(+) proof system for which no superpolynomial lower bounds are known: Hitting(+) simulates the tree-like version of Res(+) and is at least quasi-polynomially stronger. We show an exponential lower bound for Hitting(+).

cs.CC↗

arXiv2022

Irreducible subcube partitions

A \emph{subcube partition} is a partition of the Boolean cube $\{0,1\}^n$ into subcubes. A subcube partition is irreducible if the only sub-partitions whose union is a subcube are singletons and the entire partition. A subcube partition is tight if it "mentions" all coordinates. We study extremal properties of tight irreducible subcube partitions: minimal size, minimal weight, maximal number of points, maximal size, and maximal minimum dimension. We also consider the existence of homogeneous tight irreducible subcube partitions, in which all subcubes have the same dimensions. We additionally study subcube partitions of $\{0,\dots,q-1\}^n$, and partitions of $\mathbb{F}_2^n$ into affine subspaces, in both cases focusing on the minimal size. Our constructions and computer experiments lead to several conjectures on the extremal values of the aforementioned properties.

math.CO↗

arXiv2021

On the Hierarchical Community Structure of Practical Boolean Formulas

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 between practice and theory is a central problem in solver research. It is believed that SAT solvers exploit structure inherent in industrial instances, and hence there have been numerous attempts over the last 25 years at characterizing this structure via parameters. These can be classified as rigorous, i.e., they serve as a basis for complexity-theoretic upper bounds (e.g., backdoors), or correlative, i.e., they correlate well with solver run time and are observed in industrial instances (e.g., community structure). Unfortunately, no parameter proposed to date has been shown to be both strongly correlative and rigorous over a large fraction of industrial instances. Given the sheer difficulty of the problem, we aim for an intermediate goal of proposing a set of parameters that is strongly correlative and has good theoretical properties. Specifically, we propose parameters based on a graph partitioning called Hierarchical Community Structure (HCS), which captures the recursive community structure of a graph of a Boolean formula. We show that HCS parameters are strongly correlative with solver run time using an Empirical Hardness Model, and further build a classifier based on HCS parameters that distinguishes between easy industrial and hard random/crafted instances with very high accuracy. We further strengthen our hypotheses via scaling studies. On the theoretical side, we show that counterexamples which plagued community structure do not apply to HCS, and that there is a subset of HCS parameters such that restricting them limits the size of embeddable expanders.

cs.LO↗

arXiv2020

Complexity Measures on the Symmetric Group and Beyond

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, decision tree complexity, sensitivity, block sensitivity, and a few others. We show that these complexity measures are polynomially related for the symmetric group and for many other domains. To show that all measures but sensitivity are polynomially related, we generalize classical arguments of Nisan and others. To add sensitivity to the mix, we reduce to Huang's sensitivity theorem using "pseudo-characters", which witness the degree of a function. Using similar ideas, we extend the characterization of Boolean degree 1 functions on the symmetric group due to Ellis, Friedgut and Pilpel to the perfect matching scheme. As another application of our ideas, we simplify the characterization of maximum-size $t$-intersecting families in the symmetric group and the perfect matching scheme.

cs.CC↗

arXiv2020

MaxSAT Resolution and Subcube Sums

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 weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, can be viewed as a special case of the semialgebraic Sherali-Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums.

cs.CC↗

arXiv2020

Towards a Complexity-theoretic Understanding of Restarts in SAT solvers

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 well-established empirically, a theoretical explanation of whether restarts are indeed crucial to the power of CDCL solvers is lacking. In this paper, we prove a series of theoretical results that characterize the power of restarts for various models of SAT solvers. More precisely, we make the following contributions. First, we prove an exponential separation between a {\it drunk} randomized CDCL solver model with restarts and the same model without restarts using a family of satisfiable instances. Second, we show that the configuration of CDCL solver with VSIDS branching and restarts (with activities erased after restarts) is exponentially more powerful than the same configuration without restarts for a family of unsatisfiable instances. To the best of our knowledge, these are the first separation results involving restarts in the context of SAT solvers. Third, we show that restarts do not add any proof complexity-theoretic power vis-a-vis a number of models of CDCL and DPLL solvers with non-deterministic static variable and value selection.

cs.CC↗

arXiv2020

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity

We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems: * We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. * We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal.

cs.CC↗

arXiv2014

From Small Space to Small Width in Resolution

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 the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies heavily on tools from finite model theory. We give an alternative, completely elementary proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds via a "static" complexity measure that works against any resolution refutation---previous techniques have been inherently adaptive. We conclude by showing that the related question for polynomial calculus (i.e., whether space is an upper bound on degree) seems unlikely to be resolvable by similar methods.

cs.CC↗