PC 2014 ABSTRACTS: PAPERS WITH ABSTRACTS

ABSTRACT. We extend results of Bonet, Buss and Pitassi on Bondy's Theorem and of Nozaki, Arai and Arai on Boolobas's Theorem by proving that Frankl's Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parameter t, we prove that Frankl's Theorem has polynomial size, constant depth proofs from instances of the pigeonhole principle.

ABSTRACT. We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n^Omega(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. Moreover, our lower bounds can be generalized to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however---the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.

ABSTRACT. We show Ω(n^2) lower bounds on the total space used in resolution refutations of random k-CNFs over n variables, and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the long-standing open problem of whether there are families of k-CNF formulas of size O(n) requiring total space Ω(n^2) in resolution, and gives the first truly quadratic lower bounds on total space. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width.

ABSTRACT. We consider the quantified constraint satisfaction problem (QCSP) which is to decide, given a structure and a first-order sentence (not assumed here to be in prenex form) built from conjunction and quantification, whether or not the sentence is true on the structure. We present a proof system for certifying the falsity of QCSP instances and develop its basic theory; for instance, we provide an algorithmic interpretation of its behavior. Our proof system places the established Q-resolution proof system in a broader context, and also allows us to derive QCSP tractability results.

ABSTRACT. We present n^O(log log n) -size proofs in the (tree-like) monotone sequent calculus of the pigeonhole principle with (1 + ε)n pigeons and n holes, for ε = 1/polylog n. This improves on the bound of n^O(log n) inherited from proofs of the usual pigeonhole principle, with n + 1 pigeons and n holes, by Atserias et al., and supports the more general conjecture that the monotone sequent calculus polynomially simulates Hilbert-Frege systems.

ABSTRACT. In 2003, Atserias and Dalmau established that the space complexity of formulas in resolution is an upper bound on the width needed to refute them. Their proof is beautiful but somewhat mysterious in that it relies on tools from finite model theory. We give an alternative proof that works by simple syntactic manipulations of resolution refutations. As a by-product, we develop a "black-box" technique for proving space lower bounds.

ABSTRACT. Recently, an active line of research has been into the space complexity of proofs. We prove that if a formula requires large resolution width, then making XOR substitution yields a formula requiring large PC space. This yields formulas that exhibiting a degree-space separation similar to what is known for resolution. Using related ideas, we show that Tseitin formulas over random 4-regular graphs almost surely require space at least Omega(sqrt(n)).

Our proofs use techniques from [Bonacina-Galesi '13]. Our final contribution, however, is to show that these techniques cannot yield non-constant space lower bounds for the functional pigeonhole principle, which is conjectured to be hard for PC space. This talk is based on [FLMNV '13].

ABSTRACT. A typical DPLL algorithm for the Boolean satisfiability problem splits the input problem into two by assigning the two possible values to a variable; then it simplifies the two resulting formulas.

In this paper we consider an extension of the DPLL paradigm. Our algorithms can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that encode linear systems modulo two, which were used for proving exponential lower bounds for conventional DPLL algorithms.

We prove exponential lower bounds on the running time of DPLL with splitting by linear combinations on 2-fold Tseitin formulas and on formulas that encode the pigeonhole principle.

We introdice an extension of the resolution proof system that operates with disjunctions of linear equalities; we call this system Res-Lin. Tree-like proofs in Res-Lin are equivalent to the behaiviour of our algorithms on unsatisfiable instances. We prove that Res-Lin is implication complete and also prove that Res-Lin is polynomially equivalent to its semantic version.

ABSTRACT. In the area of strong fragments of Peano arithmetic, it proved fruitful to study not just the usual induction fragments~$I\Sigma_i$, but also fragments axiomatized by \emph{parameter-free} induction schemata \[\tag{$\fii\text-\indf$}\fii(0)\land\forall x\,(\fii(x)\to\fii(x+1))\to\forall x\,\fii(x)\] where $\fii$ has no free variable other than~$x$, and theories axiomatized using the closely related induction \emph{inference rules} \[\tag{$\fii\text-\indr$}\frac{\fii(0,\vec y)\quad\fii(x,\vec y)\to\fii(x+1,\vec y)}{\fii(x,\vec y)}.\] See e.g.~\cite{kpd,bekl:indru,bekl:parfree}; in particular, the last two papers detail the connection of induction rules and parameter-free schemata to reflection principles.

In contrast, induction rules and parameter-free schemata have been largely ignored in bounded arithmetic literature. Apart from $IE_i^-$ briefly discussed in~\cite{kaye:dio}, the corresponding fragments of Buss's~$S_2$ were only studied in~\cite{bloch,cffmlm}. Many basic questions about these fragments were disregarded, in particular, neither paper even mentions $\pii i$-induction rules and parameter-free schemata, despite that they could be expected to behave rather differently from $\sig i$ rules by analogy with the case of strong fragments.

In this talk, we will try to systematically investigate parameter-free and inference rule versions of the theories $T^i_2$ and~$S^i_2$: that is, $\sih i\text-\indf$, $\pih i\text-\indf$, $\sih i\text-\indr$, $\pih i\text-\indr$, and the corresponding variants of~$\pind$. (While there are many other ways how to make parameter-free schemata or rules out of the various induction or minimization schemata equivalent to $S^i_2$ or~$T^i_2$, most turn out to be equivalent to one of those above; in particular, parameter-free \emph{rules} $\sih i/\pih i\text-\ppind^{R-}$ are equivalent to their versions with parameters.)

We will particularly focus on the following questions: \begin{itemize} \item Reductions between the various rules and schemata. (A rule $R$ reduces to a rule~$R'$ if $T+R\sset T+R'$ for every theory $T\Sset\tpv$.) See Fig.~\ref{fig:rules} for a summary. \item Conservativity results between the fragments, and the formula complexity of axioms. \item The number of instances (nesting) of~$R$ needed to generate the closure $T+R$, and finite axiomatizability of fragments. \item Reformulation of axioms and rules in terms of reflection principles for propositional proof systems. \item Conditional or relativized separations between the fragments. \end{itemize}

ABSTRACT. A long line of research has shown that conflict-driven clause learning viewed as a proof system can polynomially simulate resolution. We give a more explicit description of this CDCL proof system, which allows us to define proof size and space in a natural way and also capture aspects such as clause learning schemes and restart policies. This in turn makes it possible to study which upper and lower bounds on size, space and size-space trade-offs in general resolution carry over to proofs actually realizable by CDCL solvers.

ABSTRACT. We formulate precisely several formalizations of theorems from computational complexity theory in bounded arithmetic that are presented in literature with various degrees of accuracy, and formalize the PCP theorem in the theory $PV_1$ (no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the $(n,d,\lambda)$-graphs in $PV_1$.

ABSTRACT. Please, see attached pdf file.

ABSTRACT. Parity games are a class of two player games played by moving a token around a finite graph. They have important applications in automata theory, logic and verification. The main computational problem for such games is to decide which player has a winning strategy. This problem is reducible to a search problem in the intersection of the classes PLS and PPAD, but is not known to be in P, despite intensive research work.

A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if resolution is weakly automatizable, then the decision problem for parity games is in P.

We also give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to the related classes of mean payoff games and simple stochastic games, reproving results from [1, 3].

We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.

Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.

This work has been accepted for publication as [2].