- For every part of my research, only the last version is provided (subsuming previous publications, if any). In case I deserve a citation, here is the BibTeX file for your convenience.
The pdf's on this page are drafts (as updated as possible). In a few cases of very copyrighted material, a link to the publisher's page is provided instead.

*Tropical proof systems*(with Y.Alekseev, D.Grigoriev). (Updated on June 11!)*Proving unsatisfiability with hitting formulas*(with Y.Filmus, A.Riazanov, A.Smal, M.Vinyals).*Irreducible subcube partitions*(with Y.Filmus, S.Kurz, F.Ihringer, A.Riazanov, A.Smal, M.Vinyals).*The power of the Binary Value Principle*(with Y.Alekseev).*Semi-algebraic proofs, IPS lower bounds and the τ-conjecture: can a natural number be negative?*(with Y.Alekseev, D.Grigoriev, I.Tzameret).*On the limits of gate elimination*(with A.Golovnev, A.Knop, A.Kulikov).-
*Improving 3n circuit complexity lower bounds*(with M.G.Find, A.Golovnev, A.Kulikov). -
*On the probabilistic closure of the loose unambiguous hierarchy*(with D.Sokolov). -
*Succinct interactive proofs for quantified boolean formulas*(with D.van Melkebeek, A.Smal). -
*On an optimal randomized acceptor for graph nonisomorphism*(with D.Itsykson). -
*Optimal heuristic algorithms for the image of an injective function*(with D.Itsykson, V.Nikolaenko, A.Smal). -
*On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography*(with D.Itsykson, I.Monakhov, A.Smal). -
*Optimal acceptors and optimal proof systems*. -
*Feebly secure cryptographic primitives*(with O.Melanich, S.I.Nikolenko). -
*Satisfiability certificates verifiable in subexponential time*(with E.Dantsin). -
*Complexity of semialgebraic proofs with restricted degree of falsity*(with A.Kojevnikov, A.S.Kulikov, S.I.Nikolenko). -
*[2021 edition!] Worst-case upper bounds*(with E.Dantsin) [links from publisher: 1, 2]. -
*Exact algorithms for general CNF SAT*. -
*An infinitely-often one-way function based on an average-case assumption*(with D.Itsykson). -
*A complete public-key cryptosystem*(with D.Grigoriev, K.Pervyshev). -
*Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms*(with E.Dantsin, A.Wolpert) -
*Time hierarchies for cryptographic function inversion with advice*(with D.Grigoriev, K.Pervyshev). -
*Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas*(with M.Alekhnovich, D.Itsykson). -
*Algorithms for SAT based on search in Hamming balls*(with E.Dantsin, A.Wolpert). -
*Several notes on the power of Gomory-Chvátal cuts*(with A.Kojevnikov). -
*Complexity of semialgebraic proofs*(with D.Grigoriev, D.Pasechnik). -
*UnitWalk: A new SAT solver that uses local search guided by unit clause elimination*(with A.Kojevnikov). -
*The SAT2002 Competition*(with L.Simon, D.Le Berre). -
*Algebraic proof systems over formulas*(with D.Grigoriev). -
*Algorithms for SAT and upper bounds on their complexity*(with E.Dantsin, S.Ivanov, M.Vsemirnov). -
*A Deterministic (2-2/(k+1))^n Algorithm for k-SAT Based on Local Search*(with E.Dantsin, A.Goerdt, R.Kannan, J.Kleinberg, C.Papadimitriou, P.Raghavan, U.Schöning). -
*Worst-case study of local search for MAX-k-SAT*. -
*New Worst-Case Upper Bounds for MAX-2-SAT with Application to MAX-CUT*(with J.Gramm, R.Niedermeier, P.Rossmanith). -
*SAT local search algorithms: worst-case study*. -
*New worst-case upper bounds for SAT*. -
*MAX SAT approximation beyond the limits of polynomial-time approximation*(with E.Dantsin, M.R.Gavrilovich, B.Konev). -
*Separating sings in the propositional satisfiability problem*. -
*A fast deterministic algorithm for formulas that have many satisfying assignments*. -
*On symbolic realization of hyperbolic automorphisms of torus*. -
*Picture (array) grammars and plane automata*.