Next

__
TR24-081
| 2nd April 2024
__

Sravanthi Chede, Leroy Chew, Anil Shukla#### Circuits, Proofs and Propositional Model Counting

__
TR24-080
| 16th April 2024
__

Robert Andrews, Avi Wigderson#### Constant-Depth Arithmetic Circuits for Linear Algebra Problems

__
TR24-079
| 20th April 2024
__

Tuomas Hakoniemi , Nutan Limaye, Iddo Tzameret#### Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

Next

Sravanthi Chede, Leroy Chew, Anil Shukla

In this paper we present a new proof system framework CLIP (Cumulation Linear Induction Proposition) for propositional model counting. A CLIP proof firstly involves a circuit, calculating the cumulative function (or running count) of models counted up to a point, and secondly a propositional proof arguing for the correctness of ... more >>>

Robert Andrews, Avi Wigderson

We design polynomial size, constant depth (namely, $AC^0$) arithmetic formulae for the greatest common divisor (GCD) of two polynomials, as well as the related problems of the discriminant, resultant, Bézout coefficients, squarefree decomposition, and the inversion of structured matrices like Sylvester and Bézout matrices. Our GCD algorithm extends to any ... more >>>

Tuomas Hakoniemi , Nutan Limaye, Iddo Tzameret

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi JACM 2018) offer a general model for

deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound ...
more >>>

Next