scholarly journals Computational and Proof Complexity of Partial String Avoidability

2021 ◽  
Vol 13 (1) ◽  
pp. 1-25
Author(s):  
Dmitry Itsykson ◽  
Alexander Okhotin ◽  
Vsevolod Oparin
Keyword(s):  
Lower Bounds ◽  
Circuit Complexity ◽  
Conjunctive Normal Form ◽  
Proof Complexity ◽  
Proof Systems ◽  
Finite Set ◽  
Propositional Proof Systems ◽  
Classical Proof ◽  
Exponential Size ◽  
Infinite String

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 PSPACE, and this article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, where each clause has 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 proof lines (such as clauses, inequalities, polynomials, etc.). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule but requires classical proofs of exponential size. At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.

Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds

2004 ◽  
Vol 69 (1) ◽  
pp. 265-286 ◽  
Author(s):  
Jan Krajíček
Keyword(s):  
Lower Bounds ◽  
Sparse Matrix ◽  
Proof System ◽  
Direct Construction ◽  
Proof Systems ◽  
Circuit Lower Bounds ◽  
Iterable Functions ◽  
Propositional Proof Systems ◽  
Propositional Proof ◽  
Surjective Function

AbstractThis article is a continuation of our search for tautologies that are hard even for strong propositional proof systems like EF. cf. [14, 15]. The particular tautologies we study, the τ-formulas. are obtained from any /poly map g; they express that a string is outside of the range of g, Maps g considered here are particular pseudorandom generators. The ultimate goal is to deduce the hardness of the τ-formulas for at least EF from some general, plausible computational hardness hypothesis.In this paper we introduce the notions of pseudo-surjective and iterable functions (related to free functions of [15]). These two properties imply the hardness of the τ-formulas from the function but unlike the hardness they are preserved under composition and iteration. We link the existence of maps with these two properties to the provability of circuit lower bounds, and we characterize maps g yielding hard τ-formulas in terms of a hitting set type property (all relative to a propositional proof system). We show that a proof system containing EF admits a pseudo-surjective function unless it simulates a proof system WF introduced by Jeřábek [11]. an extension of EF.We propose a concrete map g as a candidate function possibly pseudo-surjective or free for strong proof systems. The map is defined as a Nisan-Wigderson generator based on a random function and on a random sparse matrix. We prove that it is iterable in a particular way in resolution, yielding the output/input ratio n3 −ε (that improves upon a direct construction of Alekhnovich et al. [2]).

Disjoint NP-Pairs and Propositional Proof Systems

2014 ◽  
Vol 45 (4) ◽  
pp. 59-75 ◽  
Author(s):  
C. Glaßer ◽  
A. Hughes ◽  
A. L. Selman ◽  
N. Wisiol
Keyword(s):  
Proof Systems ◽  
Propositional Proof Systems ◽  
Propositional Proof

scholarly journals Proof Complexity of Modal Resolution

2021 ◽  
Author(s):  
Sarah Sigley ◽  
Olaf Beyersdorff
Keyword(s):  
Artificial Intelligence ◽  
Automated Reasoning ◽  
Proof Complexity ◽  
Pigeonhole Principle ◽  
Analytic Tableaux ◽  
Frege Systems ◽  
International Joint ◽  
Resolution Proofs ◽  
Exponential Size ◽  
Sixth International

AbstractWe investigate the proof complexity of modal resolution systems developed by Nalon and Dixon (J Algorithms 62(3–4):117–134, 2007) and Nalon et al. (in: Automated reasoning with analytic Tableaux and related methods—24th international conference, (TABLEAUX’15), pp 185–200, 2015), which form the basis of modal theorem proving (Nalon et al., in: Proceedings of the twenty-sixth international joint conference on artificial intelligence (IJCAI’17), pp 4919–4923, 2017). We complement these calculi by a new tighter variant and show that proofs can be efficiently translated between all these variants, meaning that the calculi are equivalent from a proof complexity perspective. We then develop the first lower bound technique for modal resolution using Prover–Delayer games, which can be used to establish “genuine” modal lower bounds for size of dag-like modal resolution proofs. We illustrate the technique by devising a new modal pigeonhole principle, which we demonstrate to require exponential-size proofs in modal resolution. Finally, we compare modal resolution to the modal Frege systems of Hrubeš (Ann Pure Appl Log 157(2–3):194–205, 2009) and obtain a “genuinely” modal separation.

Lower Bounds on OBDD Proofs with Several Orders

2021 ◽  
Vol 22 (4) ◽  
pp. 1-30
Author(s):  
Sam Buss ◽  
Dmitry Itsykson ◽  
Alexander Knop ◽  
Artur Riazanov ◽  
Dmitry Sokolov
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Communication Complexity ◽  
Multiparty Communication ◽  
Constant Degree ◽  
Polynomial Size ◽  
Explicit Constant ◽  
Open Question ◽  
System 1 ◽  
Exponential Size

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

Chapter 31. Quantified Boolean Formulas

2021 ◽  
Author(s):  
Olaf Beyersdorff ◽  
Mikoláš Janota ◽  
Florian Lonsing ◽  
Martina Seidl
Keyword(s):  
Performance Characteristics ◽  
Proof Complexity ◽  
Proof Systems ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
Clause Learning ◽  
Dependency Schemes

Solvers for quantified Boolean formulas (QBF) have become powerful tools for tackling hard computational problems from various application domains, even beyond the scope of SAT. This chapter gives a description of the main algorithmic paradigms for QBF solving, including quantified conflict driven clause learning (QCDCL), expansion-based solving, dependency schemes, and QBF preprocessing. Particular emphasis is laid on the connections of these solving approaches to QBF proof systems: Q-Resolution and its variants in the case of QCDCL, expansion QBF resolution calculi for expansion-based solving, and QRAT for preprocessing. The chapter also surveys the relations between the various QBF proof systems and results on their proof complexity, thereby shedding light on the diverse performance characteristics of different solving approaches that are observed in practice.

scholarly journals Computational aspects of relaxation complexity: possibilities and limitations

2021 ◽  
Author(s):  
Gennadiy Averkov ◽  
Christopher Hojny ◽  
Matthias Schymura
Keyword(s):  
Explicit Formula ◽  
Lower Bounds ◽  
Polynomial Time ◽  
Upper Bounds ◽  
Negative Answer ◽  
Integer Points ◽  
Finite Set ◽  
Computational Aspects

AbstractThe relaxation complexity $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) of the set of integer points X contained in a polyhedron is the smallest number of facets of any polyhedron P such that the integer points in P coincide with X. It is a useful tool to investigate the existence of compact linear descriptions of X. In this article, we derive tight and computable upper bounds on $${{\,\mathrm{rc}\,}}_\mathbb {Q}(X)$$ rc Q ( X ) , a variant of $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) in which the polyhedra P are required to be rational, and we show that $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) can be computed in polynomial time if X is 2-dimensional. Further, we investigate computable lower bounds on $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) with the particular focus on the existence of a finite set $$Y \subseteq \mathbb {Z}^d$$ Y ⊆ Z d such that separating X and $$Y \setminus X$$ Y \ X allows us to deduce $${{\,\mathrm{rc}\,}}(X) \ge k$$ rc ( X ) ≥ k . In particular, we show for some choices of X that no such finite set Y exists to certify the value of $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) , providing a negative answer to a question by Weltge (2015). We also obtain an explicit formula for $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) for specific classes of sets X and present the first practically applicable approach to compute $${{\,\mathrm{rc}\,}}(X)$$ rc ( X ) for sets X that admit a finite certificate.

Sign in / Sign up

Export Citation Format

Share Document