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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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