All reports by Author Dmitry Sokolov:

__
TR22-054
| 21st April 2022
__

Anastasia Sofronova, Dmitry Sokolov#### A Lower Bound for $k$-DNF Resolution on Random CNF Formulas via Expansion

__
TR21-076
| 4th June 2021
__

Dmitry Sokolov#### Pseudorandom Generators, Resolution and Heavy Width

Revisions: 1

__
TR21-028
| 27th February 2021
__

Anastasia Sofronova, Dmitry Sokolov#### Branching Programs with Bounded Repetitions and $\mathrm{Flow}$ Formulas

__
TR20-073
| 5th May 2020
__

Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, Dmitry Sokolov#### Lower Bounds on OBDD Proofs with Several Orders

__
TR20-064
| 2nd May 2020
__

Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende#### Automating Algebraic Proof Systems is NP-Hard

Revisions: 2

__
TR20-012
| 14th February 2020
__

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

__
TR19-174
| 2nd December 2019
__

Susanna de Rezende, Jakob Nordström, Kilian Risse, Dmitry Sokolov#### Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs

__
TR19-001
| 5th January 2019
__

Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry Sokolov#### On OBDD-based algorithms and proof systems that dynamically change order of variables

__
TR18-163
| 18th September 2018
__

Mika Göös, Pritish Kamath, Robert Robere, Dmitry Sokolov#### Adventures in Monotone Complexity and TFNP

__
TR18-041
| 26th February 2018
__

Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov#### Reordering Rule Makes OBDD Proof Systems Stronger

__
TR17-175
| 13th November 2017
__

Ankit Garg, Mika Göös, Pritish Kamath, Dmitry Sokolov#### Monotone Circuit Lower Bounds from Resolution

Revisions: 1

__
TR16-202
| 19th December 2016
__

Dmitry Sokolov#### Dag-like Communication and Its Applications

Revisions: 1

__
TR15-174
| 18th October 2015
__

Dmitry Itsykson, Alexander Knop, Dmitry Sokolov#### Complexity of distributions and average-case hardness

__
TR14-178
| 5th December 2014
__

Dmitry Itsykson, Alexander Knop, Dmitry Sokolov#### Heuristic time hierarchies via hierarchies for sampling distributions

__
TR14-093
| 22nd July 2014
__

Dmitry Itsykson, Mikhail Slabodkin, Dmitry Sokolov#### Resolution complexity of perfect mathcing principles for sparse graphs

__
TR14-050
| 21st March 2014
__

Edward Hirsch, Dmitry Sokolov#### On the probabilistic closure of the loose unambiguous hierarchy

Revisions: 1

__
TR12-141
| 22nd October 2012
__

Dmitry Itsykson, Dmitry Sokolov#### Lower bounds for myopic DPLL algorithms with a cut heuristic

Anastasia Sofronova, Dmitry Sokolov

Random $\Delta$-CNF formulas are one of the few candidates that are expected to be hard to refute in any proof system. One of the frontiers in the direction of proving lower bounds on these formulas is the $k$-DNF Resolution proof system (aka $\mathrm{Res}(k)$). Assume we sample $m$ clauses over $n$ ... more >>>

Dmitry Sokolov

Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson \cite{ABRW04} we call a pseudorandom generator $\mathrm{PRG}\colon \{0, 1\}^n \to \{0, 1\}^m$ hard for for a propositional proof system $\mathrm{P}$ if $\mathrm{P}$ cannot efficiently prove the (properly encoded) statement $b \notin \mathrm{Im}(\mathrm{PRG})$ for any string $b \in \{0, 1\}^m$.

In \cite{ABRW04} authors ... more >>>

Anastasia Sofronova, Dmitry Sokolov

Restricted branching programs capture various complexity measures like space in Turing machines or length of proofs in proof systems. In this paper, we focus on the application in the proof complexity that was discovered by Lovasz et al. '95 who showed the equivalence between regular Resolution and read-once branching programs ... more >>>

Sam Buss, Dmitry Itsykson, Alexander Knop, Artur Riazanov, Dmitry Sokolov

This paper is motivated by seeking lower bounds on OBDD($\land$, weakening, reordering) refutations, namely OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1-NBP($\land$) refutations based on read-once nondeterministic branching programs. These generalize OBDD($\land$, reordering) refutations. There are polynomial size 1-NBP($\land$) refutations of the pigeonhole principle, hence ... more >>>

Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, Dmitry Sokolov, Susanna de Rezende

We show that algebraic proofs are hard to find: Given an unsatisfiable CNF formula $F$, it is NP-hard to find a refutation of $F$ in the Nullstellensatz, Polynomial Calculus, or Sherali--Adams proof systems in time polynomial in the size of the shortest such refutation. Our work extends, and gives a ... more >>>

Dmitry Sokolov

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 >>>

Susanna de Rezende, Jakob Nordström, Kilian Risse, Dmitry Sokolov

We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense ... more >>>

Dmitry Itsykson, Alexander Knop, Andrei Romashchenko, Dmitry Sokolov

In 2004 Atserias, Kolaitis and Vardi proposed OBDD-based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of identically false OBDD from OBDDs representing clauses of the initial formula. All OBDDs in such proofs have the same order of variables. We initiate the study of OBDD based ... more >>>

Mika Göös, Pritish Kamath, Robert Robere, Dmitry Sokolov

$\mathbf{Separations:}$ We introduce a monotone variant of XOR-SAT and show it has exponential monotone circuit complexity. Since XOR-SAT is in NC^2, this improves qualitatively on the monotone vs. non-monotone separation of Tardos (1988). We also show that monotone span programs over R can be exponentially more powerful than over finite ... more >>>

Sam Buss, Dmitry Itsykson, Alexander Knop, Dmitry Sokolov

Atserias, Kolaitis, and Vardi [AKV04] showed that the proof system of Ordered Binary Decision Diagrams with conjunction and weakening, OBDD($\land$, weakening), simulates CP* (Cutting Planes with unary coefficients). We show that OBDD($\land$, weakening) can give exponentially shorter proofs than dag-like cutting planes. This is proved by showing that the Clique-Coloring ... more >>>

Ankit Garg, Mika Göös, Pritish Kamath, Dmitry Sokolov

For any unsatisfiable CNF formula $F$ that is hard to refute in the Resolution proof system, we show that a gadget-composed version of $F$ is hard to refute in any proof system whose lines are computed by efficient communication protocols---or, equivalently, that a monotone function associated with $F$ has large ... more >>>

Dmitry Sokolov

In 1990 Karchmer and Widgerson considered the following communication problem $Bit$: Alice and Bob know a function $f: \{0, 1\}^n \to \{0, 1\}$, Alice receives a point $x \in f^{-1}(1)$, Bob receives $y \in f^{-1}(0)$, and their goal is to find a position $i$ such that $x_i \neq y_i$. Karchmer ... more >>>

Dmitry Itsykson, Alexander Knop, Dmitry Sokolov

We address a natural question in average-case complexity: does there exist a language $L$ such that for all easy distributions $D$ the distributional problem $(L, D)$ is easy on the average while there exists some more hard distribution $D'$ such that $(L, D')$ is hard on the average? We consider ... more >>>

Dmitry Itsykson, Alexander Knop, Dmitry Sokolov

We give a new simple proof of the time hierarchy theorem for heuristic BPP originally proved by Fortnow and Santhanam [FS04] and then simplified and improved by Pervyshev [P07]. In the proof we use a hierarchy theorem for sampling distributions recently proved by Watson [W13]. As a byproduct we get ... more >>>

Dmitry Itsykson, Mikhail Slabodkin, Dmitry Sokolov

The resolution complexity of the perfect matching principle was studied by Razborov [Raz04], who developed a technique for proving its lower bounds for dense graphs. We construct a constant degree bipartite graph $G_n$ such that the resolution complexity of the perfect matching principle for $G_n$ is $2^{\Omega(n)}$, where $n$ is ... more >>>

Edward Hirsch, Dmitry Sokolov

Unambiguous hierarchies [NR93,LR94,NR98] are defined similarly to the polynomial hierarchy; however, all witnesses must be unique. These hierarchies have subtle differences in the mode of using oracles. We consider a "loose" unambiguous hierarchy $prUH_\bullet$ with relaxed definition of oracle access to promise problems. Namely, we allow to make queries that ... more >>>

Dmitry Itsykson, Dmitry Sokolov

The paper is devoted to lower bounds on the time complexity of DPLL algorithms that solve the satisfiability problem using a splitting strategy. Exponential lower bounds on the running time of DPLL algorithms on unsatisfiable formulas follow from the lower bounds for resolution proofs. Lower bounds on satisfiable instances are ... more >>>