skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Towards Verifying Nonlinear Integer Arithmetic
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 properties of the most widely used multiplier circuits. Such short proofs were conjectured not to exist. More precisely, we give n^{O(1)} size regular resolution proofs for arbitrary degree 2 identities on array, diagonal, and Booth multipliers and n^{O(log n)} size proofs for these identities on Wallace tree multipliers.  more » « less
Award ID(s):
1714593 1524246
PAR ID:
10068019
Author(s) / Creator(s):
;
Date Published:
Journal Name:
arXiv.org
ISSN:
2331-8422
Page Range / eLocation ID:
arxiv:1705.04302
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Braverman, Mark (Ed.)
    We further the study of supercritical tradeoffs in proof and circuit complexity, which is a type of tradeoff between complexity parameters where restricting one complexity parameter forces another to exceed its worst-case upper bound. In particular, we prove a new family of supercritical tradeoffs between depth and size for Resolution, Res(k), and Cutting Planes proofs. For each of these proof systems we construct, for each c ≤ n^{1-ε}, a formula with n^{O(c)} clauses and n variables that has a proof of size n^{O(c)} but in which any proof of size no more than roughly exponential in n^{1-ε}/c must necessarily have depth ≈ n^c. By setting c = o(n^{1-ε}) we therefore obtain exponential lower bounds on proof depth; this far exceeds the trivial worst-case upper bound of n. In doing so we give a simplified proof of a supercritical depth/width tradeoff for tree-like Resolution from [Alexander A. Razborov, 2016]. Finally, we outline several conjectures that would imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting theorems. 
    more » « less
  2. Chambers, Erin W.; Gudmundsson, Joachim (Ed.)
    In SoCG 2022, Conroy and Tóth presented several constructions of sparse, low-hop spanners in geometric intersection graphs, including an O(nlog n)-size 3-hop spanner for n disks (or fat convex objects) in the plane, and an O(nlog² n)-size 3-hop spanner for n axis-aligned rectangles in the plane. Their work left open two major questions: (i) can the size be made closer to linear by allowing larger constant stretch? and (ii) can near-linear size be achieved for more general classes of intersection graphs? We address both questions simultaneously, by presenting new constructions of constant-hop spanners that have almost linear size and that hold for a much larger class of intersection graphs. More precisely, we prove the existence of an O(1)-hop spanner for arbitrary string graphs with O(nα_k(n)) size for any constant k, where α_k(n) denotes the k-th function in the inverse Ackermann hierarchy. We similarly prove the existence of an O(1)-hop spanner for intersection graphs of d-dimensional fat objects with O(nα_k(n)) size for any constant k and d. We also improve on some of Conroy and Tóth’s specific previous results, in either the number of hops or the size: we describe an O(nlog n)-size 2-hop spanner for disks (or more generally objects with linear union complexity) in the plane, and an O(nlog n)-size 3-hop spanner for axis-aligned rectangles in the plane. Our proofs are all simple, using separator theorems, recursion, shifted quadtrees, and shallow cuttings. 
    more » « less
  3. We prove an Omega(n^{1−1/k} log k /2^k) lower bound on the k-party number-in-hand communication complexity of collision-finding. This implies a 2^{n^{1−o(1)}} lower bound on the size of tree-like cutting-planes proofs of the bit pigeonhole principle, a compact and natural propositional encoding of the pigeonhole principle, improving on the best previous lower bound of 2^{Omega(sqrt{n})}. 
    more » « less
  4. We study the following question raised by Erdős and Hajnal in the early 90’s. Over all n n -vertex graphs G G what is the smallest possible value of m m for which any m m vertices of G G contain both a clique and an independent set of size log ⁡ n \log n ? We construct examples showing that m m is at most 2 2 ( log ⁡ log ⁡ n ) 1 / 2 + o ( 1 ) 2^{2^{(\log \log n)^{1/2+o(1)}}} obtaining a twofold sub-polynomial improvement over the upper bound of about n \sqrt {n} coming from the natural guess, the random graph. Our (probabilistic) construction gives rise to new examples of Ramsey graphs, which while having no very large homogenous subsets contain both cliques and independent sets of size log ⁡ n \log n in any small subset of vertices. This is very far from being true in random graphs. Our proofs are based on an interplay between taking lexicographic products and using randomness. 
    more » « less
  5. We prove that unary Sherali-Adams requires proofs of size n^Ω(d) to rule out the existence o f an n^Θ(1)-clique in Erdős-Rényi random graphs whose maximum clique is of size d ≤ 2log n. This lower bound is tight up to the multiplicative constant in the exponent. We obtain this result by introducing a technique inspired by pseudo-calibration which may be of independent interest. The technique involves defining a measure on monomials that precisely captures the contribution of a monomial to a refutation . This measure intuitively captures progress and should have further applications in proof complexity. 
    more » « less