All reports by Author Anastasia Sofronova:

__
TR22-054
| 21st April 2022
__

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

__
TR22-033
| 1st March 2022
__

Ivan Mihajlin, Anastasia Sofronova#### A better-than-$3\log{n}$ depth lower bound for De Morgan formulas with restrictions on top gates

Comments: 2

__
TR21-028
| 27th February 2021
__

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

__
TR19-069
| 6th May 2019
__

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova#### Bounded-depth Frege complexity of Tseitin formulas for all graphs

Revisions: 1

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

Ivan Mihajlin, Anastasia Sofronova

We prove that a modification of Andreev's function is not computable by $(3 + \alpha - \varepsilon) \log{n}$ depth De Morgan formula with $(2\alpha - \varepsilon)\log{n}$ layers of AND gates at the top for any $1/5 > \alpha > 0$ and any constant $\varepsilon > 0$. In order to do ... 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 >>>

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova

We prove that there is a constant $K$ such that \emph{Tseitin} formulas for an undirected graph $G$ requires proofs of

size $2^{\mathrm{tw}(G)^{\Omega(1/d)}}$ in depth-$d$ Frege systems for $d<\frac{K \log n}{\log \log n}$, where $\tw(G)$ is the treewidth of $G$. This extends H{\aa}stad recent lower bound for the grid graph ...
more >>>