Author name cluster

Dmitry Itsykson

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

1 author row

STOC Conference 2025 Conference Paper

Lifting to Bounded-Depth and Regular Resolutions over Parities via Games

Yaroslav Alekseev
Dmitry Itsykson

Proving superpolynomial lower bounds on proof size in the proof system resolution over parities (Res(⊕)) remains a significant open challenge. A recent breakthrough by Efremenko, Garlik, and Itsykson (STOC 2024) established an exponential lower bound for regular Res(⊕). In this work, we introduce a lifting technique for regular Res(⊕), applicable to a wide range of formulas. Specifically, we develop a method that transforms any formula with large resolution depth into a formula requiring exponential-size regular Res(⊕) refutations. This transformation is achieved through a combination of mixing and constant-size lifting. Using this approach, we provide an alternative and improved separation between resolution and regular Res(⊕), originally proved by Bhattacharya, Chattopadhyay, and Dvorak (CCC 2024). We construct an n -variable formula with a polynomial-size resolution refutation of depth O (√ n ), yet requires regular Res(⊕) refutations of size 2 Ω(√ n ) . Furthermore, we apply our technique to establish an exponential lower bound on the size of depth- cn loglog n Res(⊕) refutations, where n is the number of variables in the refuted formula, and c is a constant. The hard instances in this setting are Tseitin formulas lifted with the Maj 5 gadget. Since even depth- n Res(⊕) captures all possible definitions of regular Res(⊕), our result yields an exponential lower bound for top-regular Res(⊕), resolving an open question posed by Gryaznov, Pudlák, and Talebanfard (CCC 2022).

Details

STOC Conference 2024 Conference Paper

Lower Bounds for Regular Resolution over Parities

Klim Efremenko
Michal Garlík
Dmitry Itsykson

The proof system resolution over parities (Res(⊕)) operates with disjunctions of linear equations (linear clauses) over GF(2); it extends the resolution proof system by incorporating linear algebra over GF(2). Over the years, several exponential lower bounds on the size of tree-like refutations have been established. However, proving a superpolynomial lower bound on the size of dag-like Res(⊕) refutations remains a highly challenging open question. We prove an exponential lower bound for regular Res(⊕). Regular Res(⊕) is a subsystem of dag-like Res(⊕) that naturally extends regular resolution. This is the first known superpolynomial lower bound for a fragment of dag-like Res(⊕) which is exponentially stronger than tree-like Res(⊕). In the regular regime, resolving linear clauses C 1 and C 2 on a linear form f is permitted only if, for both i ∈ {1,2}, the linear form f does not lie within the linear span of all linear forms that were used in resolution rules during the derivation of C i . Namely, we show that the size of any regular Res(⊕) refutation of the binary pigeonhole principle BPHP n n +1 is at least 2 Ω(∛ n /log n ) . A corollary of our result is an exponential lower bound on the size of a strongly read-once linear branching program solving a search problem. This resolves an open question raised by Gryaznov, Pudlak, and Talebanfard (CCC 2022). As a byproduct of our technique, we prove that the size of any tree-like Res(⊕) refutation of the weak binary pigeonhole principle BPHP n m is at least 2 Ω( n ) using Prover-Delayer games. We also give a direct proof of a width lower bound: we show that any dag-like Res(⊕) refutation of BPHP n m contains a linear clause C with Ω( n ) linearly independent equations.

Details

SAT Conference 2024 Conference Paper

On Limits of Symbolic Approach to SAT Solving

Dmitry Itsykson
Sergei Ovcharov

We study the symbolic approach to the propositional satisfiability problem proposed by Aguirre and Vardi in 2001 based on OBDDs and symbolic quantifier elimination. We study the theoretical limitations of the most general version of this approach where it is allowed to dynamically change variable order in OBDD. We refer to algorithms based on this approach as OBDD(∧, ∃, reordering) algorithms. We prove the first exponential lower bound of OBDD(∧, ∃, reordering) algorithms on unsatisfiable formulas, and give an example of formulas having short tree-like resolution proofs that are exponentially hard for OBDD(∧, ∃, reordering) algorithms. We also present the first exponential lower bound for natural formulas with clear combinatorial meaning: every OBDD(∧, ∃, reordering) algorithm runs exponentially long on the binary pigeonhole principle BPHP^{n+1}_n.

Details

MFCS Conference 2022 Conference Paper

Automating OBDD proofs is NP-hard

Dmitry Itsykson
Artur Riazanov

We prove that the proof system OBDD(∧, weakening) is not automatable unless P = NP. The proof is based upon the celebrated result of [Albert Atserias and Moritz Müller, 2019] about the hardness of automatability for resolution. The heart of the proof is lifting with multi-output indexing gadget from resolution block-width to dag-like multiparty number-in-hand communication protocol size with o(n) parties, where n is the number of variables in the non-lifted formula. A similar lifting theorem for protocols with n+1 participants was proved by [Göös et al. , 2020] to establish the hardness of automatability result for Cutting Planes.

Details

SAT Conference 2022 Conference Paper

Tight Bounds for Tseitin Formulas

Dmitry Itsykson
Artur Riazanov
Petr Smirnov

We show that for any connected graph G the size of any regular resolution or OBDD(∧, reordering) refutation of a Tseitin formula based on G is at least 2^Ω(tw(G)), where tw(G) is the treewidth of G. These lower bounds improve upon the previously known bounds and, moreover, they are tight. For both of the proof systems, there are constructive upper bounds that almost match the obtained lower bounds, hence the class of Tseitin formulas is almost automatable for regular resolution and for OBDD(∧, reordering).

Details

MFCS Conference 2019 Conference Paper

Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs

Nicola Galesi
Dmitry Itsykson
Artur Riazanov
Anastasia Sofronova

We prove that there is a constant K such that Tseitin formulas for an undirected graph G requires proofs of size 2^{tw(G)^{Omega(1/d)}} in depth-d Frege systems for d<(K log n)/(log log n), where tw(G) is the treewidth of G. This extends Håstad recent lower bound for the grid graph to any graph. Furthermore, we prove tightness of our bound up to a multiplicative constant in the top exponent. Namely, we show that if a Tseitin formula for a graph G has size s, then for all large enough d, it has a depth-d Frege proof of size 2^{tw(G)^{O(1/d)}} poly(s). Through this result we settle the question posed by M. Alekhnovich and A. Razborov of showing that the class of Tseitin formulas is quasi-automatizable for resolution.

Details

SAT Conference 2017 Conference Paper

Hard Satisfiable Formulas for Splittings by Linear Combinations

Dmitry Itsykson
Alexander Knop

Abstract Itsykson and Sokolov in 2014 introduced the class of \(\mathrm {DPLL}(\oplus )\) algorithms that solve Boolean satisfiability problem using the splitting by linear combinations of variables modulo 2. This class extends the class of \(\mathrm {DPLL}\) algorithms that split by variables. \(\mathrm {DPLL}(\oplus )\) algorithms solve in polynomial time systems of linear equations modulo 2 that are hard for \(\mathrm {DPLL}\), \(\mathrm {PPSZ}\) and \(\mathrm {CDCL}\) algorithms. Itsykson and Sokolov have proved first exponential lower bounds for \(\mathrm {DPLL}(\oplus )\) algorithms on unsatisfiable formulas. In this paper we consider a subclass of \(\mathrm {DPLL}(\oplus )\) algorithms that arbitrary choose a linear form for splitting and randomly (with equal probabilities) choose a value to investigate first; we call such algorithms drunken \(\mathrm {DPLL}(\oplus )\). We give a construction of a family of satisfiable CNF formulas \(\varPsi _n\) of size \(\mathrm {poly}(n)\) such that any drunken \(\mathrm {DPLL}(\oplus )\) algorithm with probability at least \(1 - 2^{-\varOmega (n)}\) runs at least \(2^{\varOmega (n)}\) steps on \(\varPsi _n\); thus we solve an open question stated in the paper [ 12 ]. This lower bound extends the result of Alekhnovich, Hirsch and Itsykson [ 1 ] from drunken \(\mathrm {DPLL}\) to drunken \(\mathrm {DPLL}(\oplus )\).

Details

MFCS Conference 2017 Conference Paper

Satisfiable Tseitin Formulas Are Hard for Nondeterministic Read-Once Branching Programs

Ludmila Glinskih
Dmitry Itsykson

We consider satisfiable Tseitin formulas TS_{G, c} based on d-regular expanders G with the absolute value of the second largest eigenvalue less than d/3. We prove that any nondeterministic read-once branching program (1-NBP) representing TS_{G, c} has size 2^{\Omega(n)}, where n is the number of vertices in G. It extends the recent result by Itsykson at el. [STACS 2017] from OBDD to 1-NBP. On the other hand it is easy to see that TS_{G, c} can be represented as a read-2 branching program (2-BP) of size O(n), as the negation of a nondeterministic read-once branching program (1-coNBP) of size O(n) and as a CNF formula of size O(n). Thus TS_{G, c} gives the best possible separations (up to a constant in the exponent) between 1-NBP and 2-BP, 1-NBP and 1-coNBP and between 1-NBP and CNF.

Details

MFCS Conference 2016 Conference Paper

Computational and Proof Complexity of Partial String Avoidability

Dmitry Itsykson
Alexander Okhotin
Vsevolod Oparin

The partial string avoidability problem, also known as partial word avoidability, is stated as follows: given a finite set of strings with possible ``holes'' (undefined symbols), determine whether there exists any 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 PSPACE, and this paper establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form (CNF) satisfiability problem (SAT), with each clause having infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting constraints (such as clauses, inequalities, polynomials, etc). Two results on their proof complexity are established. First, there is a particular formula that has a short refutation in Resolution with shift, but requires classical proofs of exponential size (Resolution, Cutting Plane, Polynomial Calculus, etc.). At the same time, exponential lower bounds for shifted versions of classical proof systems are established.

Details