1. 
 Conneryd, Jonas, et al.
(författare)

Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz
 2023

Ingår i: Proceedings  2023 IEEE 64th Annual Symposium on Foundations of Computer Science, FOCS 2023.  02725428.  9798350318944 ; , s. 111

Konferensbidrag (refereegranskat)abstract
 We prove that polynomial calculus (and hence also Nullstellensatz) over any field requires linear degree to refute that sparse random regular graphs, as well as sparse ErdősRényi random graphs, are 3colourable.


2. 
 De Rezende, Susanna F., et al.
(författare)

KRW composition theorems via lifting
 2020

Ingår i: Proceedings  2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020.  02725428.  9781728196213  9781728196220 ; 2020November, s. 4349

Konferensbidrag (refereegranskat)abstract
 One of the major open problems in complexity theory is proving superlogarithmic lower bounds on the depth of circuits (i.e., mathrm{P} nsubseteq text{NC}{1}). Karchmer, Raz, and Wigderson [13] suggested to approach this problem by proving that depth complexity behaves'as expected' with respect to the composition of functions f diamond g. They showed that the validity of this conjecture would imply that mathrm{P} nsubseteq text{NC}{1}. Several works have made progress toward resolving this conjecture by proving special cases. In particular, these works proved the KRW conjecture for every outer function, but only for few inner functions. Thus, it is an important challenge to prove the KRW conjecture for a wider range of inner functions. In this work, we extend significantly the range of inner functions that can be handled. First, we consider the monotone version of the KRW conjecture. We prove it for every monotone inner function whose depth complexity can be lower bounded via a querytocommunication lifting theorem. This allows us to handle several new and wellstudied functions such as the stconnectivity, clique, and generation functions. In order to carry this progress back to the nonmonotone setting, we introduce a new notion of semimonotone composition, which combines the nonmonotone complexity of the outer function with the monotone complexity of the inner function. In this setting, we prove the KRW conjecture for a similar selection of inner functions, but only for a specific choice of the outer function f.


3. 
 De Rezende, Susanna, et al.
(författare)

Lifting with simple gadgets and applications to circuit and proof complexity
 2020

Ingår i: Proceedings  2020 IEEE 61st Annual Symposium on Foundations of Computer Science, FOCS 2020.  02725428.  9781728196213  9781728196220 ; 2020November, s. 2430

Konferensbidrag (refereegranskat)abstract
 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 greaterthan. We apply our generalized theorem to solve three 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 nonexplicit separation was known. •We give the strongest separation todate between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomialsize monotone Boolean circuits, requires monotone Boolean formulas of size 2{Omega(n text{polylog}(n))}. 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. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144.


4. 
 Kaufmann, Daniela, et al.
(författare)

Adding Dual Variables to Algebraic Reasoning for GateLevel Multiplier Verification
 2022

Ingår i: Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022.  9783981926361 ; , s. 14311436

Konferensbidrag (refereegranskat)abstract
 Algebraic reasoning has proven to be one of the most effective approaches for verifying gatelevel integer multipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.


5. 
 Liew, Vincent, et al.
(författare)

Verifying Properties of Bitvector Multiplication Using Cutting Planes Reasoning
 2020

Ingår i: Proceedings of the 20th Conference on Formal Methods in ComputerAided Design, FMCAD 2020.  9783854480426 ; , s. 194204

Konferensbidrag (refereegranskat)abstract
 Systems mixing Boolean logic and arithmetic have been a longstanding challenge for verification tools such as SATbased bitvector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bitlevel reasoning. We propose that pseudoBoolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses. Theoretically, we show that there are optimallength cutting planes proofs for a large class of bitlevel properties of some well known multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bitlevel consequences of wordlevel equations in exponentially fewer steps than methods based on Gröbner bases. Experimentally, we demonstrate that pseudoBoolean solvers can verify the wordlevel equivalence of adderbased multiplier architectures, as well as commutativity of bitvector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bitlevel. Finally, we find examples of simple nonlinear bitvector inequalities that are intractable for current bitvector and SAT solvers but easy for pseudoBoolean solvers.

