All reports by Author Dmitry Itsykson:

__
TR24-128
| 27th August 2024
__

Yaroslav Alekseev, Dmitry Itsykson#### Lifting to regular resolution over parities via games

__
TR23-187
| 27th November 2023
__

Klim Efremenko, Michal Garlik, Dmitry Itsykson#### Lower bounds for regular resolution over parities

Revisions: 1

__
TR22-046
| 4th April 2022
__

Dmitry Itsykson, Artur Riazanov#### Automating OBDD proofs is NP-hard

__
TR20-184
| 10th December 2020
__

Dmitry Itsykson, Artur Riazanov#### Proof complexity of natural formulas via communication arguments

__
TR20-073
| 5th May 2020
__

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

__
TR20-067
| 30th April 2020
__

Dmitry Itsykson, Alexander Okhotin, Vsevolod Oparin#### Computational and proof complexity of partial string avoidability

__
TR19-178
| 5th December 2019
__

Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov#### Almost Tight Lower Bounds on Regular Resolution Refutations of Tseitin Formulas for All Constant-Degree Graphs

__
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

__
TR19-020
| 4th February 2019
__

Ludmila Glinskih, Dmitry Itsykson#### On Tseitin formulas, read-once branching programs and treewidth

Revisions: 1

__
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-041
| 26th February 2018
__

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

__
TR17-117
| 20th July 2017
__

Dmitry Itsykson, Alexander Knop#### Hard satisfiable formulas for splittings by linear combinations

__
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

__
TR12-141
| 22nd October 2012
__

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

__
TR11-091
| 20th May 2011
__

Edward Hirsch, Dmitry Itsykson, Valeria Nikolaenko, Alexander Smal#### Optimal heuristic algorithms for the image of an injective function

__
TR10-193
| 5th December 2010
__

Edward Hirsch, Dmitry Itsykson, Ivan Monakhov, Alexander Smal#### On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography

__
TR08-073
| 4th August 2008
__

Dmitry Itsykson#### Structural complexity of AvgBPP

__
TR07-117
| 8th November 2007
__

Edward Hirsch, Dmitry Itsykson#### An infinitely-often one-way function based on an average-case assumption

__
TR04-041
| 18th May 2004
__

Michael Alekhnovich, Edward Hirsch, Dmitry Itsykson#### Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas

Yaroslav Alekseev, Dmitry Itsykson

The propositional proof system resolution over parities (Res($\oplus$)) combines resolution and the linear algebra over GF(2). It is a challenging open question to prove a superpolynomial lower bound on the proof size in this system. For many years, superpolynomial lower bounds were known only in tree-like cases. Recently, Efremenko, Garlik, ... more >>>

Klim Efremenko, Michal Garlik, Dmitry Itsykson

The proof system resolution over parities (Res($\oplus$)) operates with disjunctions of linear equations (linear clauses) over $\mathbb{F}_2$; it extends the resolution proof system by incorporating linear algebra over $\mathbb{F}_2$. Over the years, several exponential lower bounds on the size of tree-like Res($\oplus$) refutations have been established. However, proving a superpolynomial ... more >>>

Dmitry Itsykson, Artur Riazanov

We prove that the proof system OBDD(and, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of Atserias and Muller [FOCS 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with a multi-output indexing gadget from resolution ... more >>>

Dmitry Itsykson, Artur Riazanov

A canonical communication problem ${\rm Search}(\phi)$ is defined for every unsatisfiable CNF $\phi$: an assignment to the variables of $\phi$ is distributed among the communicating parties, they are to find a clause of $\phi$ falsified by this assignment. Lower bounds on the randomized $k$-party communication complexity of ${\rm Search}(\phi)$ in ... 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 >>>

Dmitry Itsykson, Alexander Okhotin, Vsevolod Oparin

The partial string avoidability problem is stated as follows: given a finite set of strings with possible ``holes'' (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in ... more >>>

Dmitry Itsykson, Artur Riazanov, Danil Sagunov, Petr Smirnov

We show that the size of any regular resolution refutation of Tseitin formula $T(G,c)$ based on a graph $G$ is at least $2^{\Omega(tw(G)/\log n)}$, where $n$ is the number of vertices in $G$ and $tw(G)$ is the treewidth of $G$. For constant degree graphs there is known upper bound $2^{O(tw(G))}$ ... 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 >>>

Ludmila Glinskih, Dmitry Itsykson

We show that any nondeterministic read-once branching program that computes a satisfiable Tseitin formula based on an $n\times n$ grid graph has size at least $2^{\Omega(n)}$. Then using the Excluded Grid Theorem by Robertson and Seymour we show that for arbitrary graph $G(V,E)$ any nondeterministic read-once branching program that computes ... 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 >>>

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

Dmitry Itsykson, Alexander Knop

Itsykson and Sokolov in 2014 introduced the class of DPLL($\oplus$) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of DPLL algorithms that split by variables. DPLL($\oplus$) algorithms solve in polynomial time systems of linear equations modulo two ... 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 >>>

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

Edward Hirsch, Dmitry Itsykson, Valeria Nikolaenko, Alexander Smal

The existence of optimal algorithms is not known for any decision problem in NP$\setminus$P. We consider the problem of testing the membership in the image of an injective function. We construct optimal heuristic algorithms for this problem in both randomized and deterministic settings (a heuristic algorithm can err on a ... more >>>

Edward Hirsch, Dmitry Itsykson, Ivan Monakhov, Alexander Smal

The existence of an optimal propositional proof system is a major open question in proof complexity; many people conjecture that such systems do not exist. Krajicek and Pudlak (1989) show that this question is equivalent to the existence of an algorithm that is optimal on all propositional tautologies. Monroe (2009) ... more >>>

Dmitry Itsykson

We study class AvgBPP that consists of distributional problems that can be solved in average polynomial time (in terms of Levin's average-case complexity) by randomized algorithms with bounded error. We prove that there exists a distributional problem that is complete for AvgBPP under polynomial-time samplable distributions. Since we use deterministic ... more >>>

Edward Hirsch, Dmitry Itsykson

We assume the existence of a function f that is computable in polynomial time but its inverse function is not computable in randomized average-case polynomial time. The cryptographic setting is, however, different: even for a weak one-way function, every possible adversary should fail on a polynomial fraction of inputs. Nevertheless, ... more >>>

Michael Alekhnovich, Edward Hirsch, Dmitry Itsykson

DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satisfiability problem) and are widely used in applications. The recursion trees of DPLL algorithm executions on unsatisfiable formulas are equivalent to tree-like resolution proofs. Therefore, lower bounds for tree-like resolution (which ... more >>>