Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with Random formulas:
TR13-018 | 29th January 2013
Luke Friedman, Yixin Xu

Exponential Lower Bounds for Refuting Random Formulas Using Ordered Binary Decision Diagrams

A propositional proof system based on ordered binary decision diagrams (OBDDs) was introduced by Atserias et al. Krajicek proved exponential lower bounds for a strong variant of this system using feasible interpolation, and Tveretina et al. proved exponential lower bounds for restricted versions of this system for refuting formulas derived ... more >>>

TR13-027 | 29th January 2013
Luke Friedman

A Framework for Proving Proof Complexity Lower Bounds on Random CNFs Using Encoding Techniques

Propositional proof complexity is an area of complexity theory that addresses the question of whether the class NP is closed under complement, and also provides a theoretical framework for studying practical applications such as SAT solving.
Some of the most well-studied contradictions are random $k$-CNF formulas where each clause of ... more >>>

TR17-042 | 6th March 2017
Pavel Hrubes, Pavel Pudlak

Random formulas, monotone circuits, and interpolation

We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept that we call "unsatisfiability certificate". This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we ... more >>>

TR17-137 | 11th September 2017
Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde

Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs

As a natural extension of the SAT problem, different proof systems for quantified Boolean formulas (QBF) have been proposed. Many of these extend a propositional system to handle universal quantifiers.

By formalising the construction of the QBF proof system from a propositional proof system, by the addition of the ... more >>>

TR20-012 | 14th February 2020
Dmitry Sokolov

(Semi)Algebraic Proofs over $\{\pm 1\}$ Variables

One of the major open problems in proof complexity is to prove lower bounds on $AC_0[p]$-Frege proof
systems. As a step toward this goal Impagliazzo, Mouli and Pitassi in a recent paper suggested to prove
lower bounds on the size for Polynomial Calculus over the $\{\pm 1\}$ basis. In this ... more >>>

ISSN 1433-8092 | Imprint