Search

It is well-known that Resolution proofs can be efficiently simulated by Sherali–Adams (SA) proofs. We show, however, that any such simulation needs to exploit huge coefficients: Resolution cannot be efficiently simulated by SA when the coefficients are written in unary. We also show that Reversible Resolution (a variant of MaxSAT Resolution) cannot be efficiently simulated by Nullstellensatz (NS). These results have consequences for total NP search problems. First, we characterise the classes PPADS, PPAD, SOPL by unary-SA, unary-NS, and Reversible Resolution, respectively. Second, we show that, relative to an oracle, \({\text{ PLS}} \not\subseteq {\text{ PPP}}\) , \({\text{ SOPL}} \not\subseteq {\text{ PPA}}\) , and \({\text{ EOPL}} \not\subseteq {\text{ UEOPL}}\). In particular, together with prior work, this gives a complete picture of the black-box relationships between all classical TFNP classes introduced in the 1990s. [ABSTRACT FROM AUTHOR]

In Quantified Boolean Formulas QBFs, dependency schemes help to detect spurious or superfluous dependencies that are implied by the variable ordering in the quantifier prefix but are not essential for constructing countermodels. This detection can provably shorten refutations in specific proof systems, and is expected to speed up runs of QBF solvers. The proof system QCDCL recently defined by Beyersdorff and Boehm (LMCS 2023) abstracts the reasoning employed by QBF solvers based on conflict-driven clause-learning (CDCL) techniques. We show how to incorporate the use of dependency schemes into this proof system, either in a preprocessing phase, or in the propagations and clause learning, or both. We then show that when the reflexive resolution path dependency scheme D rrs is used, a mixed picture emerges: the proof systems that add D rrs to QCDCL in these three ways are not only incomparable with each other, but are also incomparable with the basic QCDCL proof system that does not use D rrs at all, as well as with several other resolution-based QBF proof systems. A notable fact is that all our separations are achieved through QBFs with bounded quantifier alternation. [ABSTRACT FROM AUTHOR]

We introduce the binary value principle, which is a simple subset-sum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a well-known hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi [J. ACM, 65 (2018), 37]. Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semialgebraic proof systems. Our results extend to unrestricted IPS the paradigm introduced by Forbes, Shpilka, Tzameret, and Wigderson [Theory Comput., 17 (2021), pp. 1--88], whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semialgebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following. (1) Conditional IPS lower bounds: The Shub--Smale hypothesis [Duke Math. J., 81 (1995), pp. 47--54] implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation.... Further, the related and more widely known \tau -conjecture [Duke Math. J., 81 (1995), pp. 47--54] implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or apparently weaker propositional proof systems such as Frege systems (though our lower bounds do not translate to Frege lower bounds since the hard instances are not Boolean formulas). (2) Algebraic versus semialgebraic proofs: Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semialgebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semialgebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semialgebraic analogue of the IPS: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sum-of-squares proofs (and extensions) as algebraic circuits. We prove that IPS polynomially simulates CPS iff IPS admits polynomial-size refutations of the binary value principle (for the language of systems of equations that have no 0/1-solutions), over both Z and Q. [ABSTRACT FROM AUTHOR]

Quantified conflict-driven clause learning (QCDCL) is one of the main solving approaches for quantified Boolean formulas (QBF). One of the differences between QCDCL and propositional CDCL is that QCDCL typically follows the prefix order of the QBF for making decisions. We investigate an alternative model for QCDCL solving where decisions can be made in arbitrary order. The resulting system QCDCL A NY is still sound and terminating, but does not necessarily allow to always learn asserting clauses or cubes. To address this potential drawback, we additionally introduce two subsystems that guarantee to always learn asserting clauses ( QCDCL U NI - A NY ) and asserting cubes ( QCDCL E XI - A NY ), respectively. We model all four approaches by formal proof systems and show that QCDCL U NI - A NY is exponentially better than QCDCL on false formulas, whereas QCDCL E XI - A NY is exponentially better than QCDCL on true QBFs. Technically, this involves constructing specific QBF families and showing lower and upper bounds in the respective proof systems. We complement our theoretical study with some initial experiments that confirm our theoretical findings. [ABSTRACT FROM AUTHOR]

The ε -elimination method of Hilbert's ε -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert's ε -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses of the extended first ε -theorem, even if the formalisation incorporates so-called ε -equality axioms. [ABSTRACT FROM AUTHOR]

Stabbing Planes (also known as Branch and Cut) is a proof system introduced very recently which, informally speaking, extends the DPLL method by branching on integer linear inequalities instead of single variables. The techniques known so far to prove size and depth lower bounds for Stabbing Planes are generalizations of those used for the Cutting Planes proof system. For size lower bounds these are established by monotone circuit arguments, while for depth these are found via communication complexity and protection. As such these bounds apply for lifted versions of combinatorial statements. Rank lower bounds for Cutting Planes are also obtained by geometric arguments called protection lemmas. In this work we introduce two new geometric approaches to prove size/depth lower bounds in Stabbing Planes working for any formula: (1) the antichain method, relying on Sperner's Theorem and (2) the covering method which uses results on essential coverings of the boolean cube by linear polynomials, which in turn relies on Alon's combinatorial Nullenstellensatz. We demonstrate their use on classes of combinatorial principles such as the Pigeonhole principle, the Tseitin contradictions and the Linear Ordering Principle. By the first method we prove almost linear size lower bounds and optimal logarithmic depth lower bounds for the Pigeonhole principle and analogous lower bounds for the Tseitin contradictions over the complete graph and for the Linear Ordering Principle. By the covering method we obtain a superlinear size lower bound and a logarithmic depth lower bound for Stabbing Planes proof of Tseitin contradictions over a grid graph. [ABSTRACT FROM AUTHOR]

QCDCL is one of the main algorithmic paradigms for solving quantified Boolean formulas (QBF). We design a new technique to show lower bounds for the running time in QCDCL algorithms. For this we model QCDCL by concisely defined proof systems and identify a new width measure for formulas, which we call gauge. We show that for a large class of QBFs, large (e.g. linear) gauge implies exponential lower bounds for QCDCL proof size. We illustrate our technique by computing the gauge for a number of sample QBFs, thereby providing new exponential lower bounds for QCDCL. Our technique is the first bespoke lower bound technique for QCDCL. [ABSTRACT FROM AUTHOR]

Satisfiability is considered the canonical NP‐complete problem and is used as a starting point for hardness reductions in theory, while in practice heuristic SAT solving algorithms can solve large‐scale industrial SAT instances very efficiently. This disparity between theory and practice is believed to be a result of inherent properties of industrial SAT instances that make them tractable. Two characteristic properties seem to be prevalent in the majority of real‐world SAT instances, heterogeneous degree distribution and locality. To understand the impact of these two properties on SAT, we study the proof complexity of random k$$ k $$‐SAT models that allow to control heterogeneity and locality. Our findings show that heterogeneity alone does not make SAT easy as heterogeneous random k$$ k $$‐SAT instances have superpolynomial resolution size. This implies intractability of these instances for modern SAT‐solvers. In contrast, modeling locality with underlying geometry leads to small unsatisfiable subformulas, which can be found within polynomial time. [ABSTRACT FROM AUTHOR]

We identify two new clusters of proof complexity measures equal up to polynomial and log ⁡ n factors. The first cluster contains the logarithm of tree-like resolution size, regularized clause and monomial space, and clause space, ordinary and regularized, in regular and tree-like resolution. Consequently, separating clause or monomial space from the logarithm of tree-like resolution size is equivalent to showing strong trade-offs between clause space and length, and equivalent to showing super-critical trade-offs between clause space and depth. The second cluster contains width, Σ 2 space (a generalization of clause space to depth 2 Frege systems), ordinary and regularized, and the logarithm of tree-like R (log ⁡) size. As an application, we improve a known size-space trade-off for polynomial calculus with resolution. We further show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space 4, and introduce a measure intermediate between depth and the logarithm of tree-like resolution size. [ABSTRACT FROM AUTHOR]

An account of mathematical understanding should account for the differences between theorems whose proofs are “easy” to discover, and those whose proofs are difficult to discover. Though Hilbert seems to have created proof theory with the idea that it would address this kind of “discovermental complexity”, much more attention has been paid to the lengths of proofs, a measure of the difficulty of verifying of a given formal object that it is a proof of a given formula in a given formal system. In this paper we will shift attention back to discovermental complexity, by addressing a “topological” measure of proof complexity recently highlighted by Alessandra Carbone (2009). Though we will contend that Carbone’s measure fails as a measure of discovermental complexity, it forefronts numerous important formal and epistemological issues that we will discuss, including the structure of proofs and the question of whether impure proofs are systematically simpler than pure proofs. [ABSTRACT FROM AUTHOR]

We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution. Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the minimum number of variables needed to distinguish two graphs with n vertices each, then there is an nO(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2k−1 and k for the treelike resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp(Ω(k²/n)) for the case of colored graphs with constant color class sizes. Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach. [ABSTRACT FROM AUTHOR]

Proofs in propositional logic are typically presented as trees of derived formulas or, alternatively, as directed acyclic graphs of derived formulas. This distinction between tree-like vs. dag-like structure is particularly relevant when making quantitative considerations regarding, for example, proof size. Here we analyze a more general type of structural restriction for proofs in rule-based proof systems. In this definition, proofs are directed graphs of derived formulas in which cycles are allowed as long as every formula is derived at least as many times as it is required as a premise. We call such proofs “circular”. We show that, for all sets of standard inference rules with single or multiple conclusions, circular proofs are sound. We start the study of the proof complexity of circular proofs at Circular Resolution, the circular version of Resolution. We immediately see that Circular Resolution is stronger than dag-like Resolution since, as we show, the propositional encoding of the pigeonhole principle has circular Resolution proofs of polynomial size. Furthermore, for derivations of clauses from clauses, we show that Circular Resolution is, surprisingly, equivalent to Sherali-Adams, a proof system for reasoning through polynomial inequalities that has linear programming at its base. As corollaries we get: (1) polynomial-time (LP-based) algorithms that find Circular Resolution proofs of constant width, (2) examples that separate Circular from dag-like Resolution, such as the pigeonhole principle and its variants, and (3) exponentially hard cases for Circular Resolution. Contrary to the case of Circular Resolution, for Frege we show that circular proofs can be converted into tree-like proofs with at most polynomial overhead. [ABSTRACT FROM AUTHOR]

QBF solvers implementing the QCDCL paradigm are powerful algorithms that successfully tackle many computationally complex applications. However, our theoretical understanding of the strength and limitations of these QCDCL solvers is very limited. In this paper we suggest to formally model QCDCL solvers as proof systems. We define different policies that can be used for decision heuristics and unit propagation and give rise to a number of sound and complete QBF proof systems (and hence new QCDCL algorithms). With respect to the standard policies used in practical QCDCL solving, we show that the corresponding QCDCL proof system is incomparable (via exponential separations) to Q-resolution, the classical QBF resolution system used in the literature. This is in stark contrast to the propositional setting where CDCL and resolution are known to be p-equivalent. This raises the question what formulas are hard for standard QCDCL, since Q-resolution lower bounds do not necessarily apply to QCDCL as we show here. In answer to this question we prove several lower bounds for QCDCL, including exponential lower bounds for a large class of random QBFs. We also introduce a strengthening of the decision heuristic used in classical QCDCL, which does not necessarily decide variables in order of the prefix, but still allows to learn asserting clauses. We show that with this decision policy, QCDCL can be exponentially faster on some formulas. We further exhibit a QCDCL proof system that is p-equivalent to Q-resolution. In comparison to classical QCDCL, this new QCDCL version adapts both decision and unit propagation policies. [ABSTRACT FROM AUTHOR]

We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) via circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems [16], but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs. Our characterisation works for both Q-Resolution and QU-Resolution. Using our characterisation, we obtain a size-width relation for QBF resolution in the spirit of the celebrated result for propositional resolution [4]. However, our result is not just a replication of the propositional relation--intriguingly ruled out for QBF in previous research [12]--but shows a different dependence between size, width, and quantifier complexity. An essential ingredient is an improved relation between the size and width of term decision lists; this may be of independent interest. We demonstrate that our new technique elegantly reproves known QBF hardness results and unifies previous lower-bound techniques in the QBF domain. [ABSTRACT FROM AUTHOR]

We study the MaxSAT Resolution (MaxRes) rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, can be viewed as a special case of the semi-algebraic Sherali-Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums. [ABSTRACT FROM AUTHOR]

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving variants via proof complexity techniques. Our results show that almost all of the QCDCL variants are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL. [ABSTRACT FROM AUTHOR]

MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem. Weighted Polynomial Calculus is a natural generalization of the systems MaxSAT-Resolution and weighted Resolution. Unlike such systems, weighted Polynomial Calculus manipulates polynomials with coefficients in a finite field and either weights in N or Z. We show the soundness and completeness of weighted Polynomial Calculus via an algorithmic procedure. Weighted Polynomial Calculus, with weights in N and coefficients in F 2 , is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in Z , it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable. [ABSTRACT FROM AUTHOR]

We present a sequent calculus with the Henkin constants in the place of the free variables. By disposing of the eigenvariable condition, we obtained a proof system with a strong locality property—the validity of each inference step depends only on its active formulas, not its context. Our major outcomes are: the cut elimination via a non-Gentzen-style algorithm without resorting to regularization and the elimination of Skolem functions with linear increase in the proof length for a subclass of derivations with cuts. [ABSTRACT FROM AUTHOR]

Copyright of Proceedings of the YSU A: Physical & Mathematical Sciences is the property of Publishing House of Yerevan State University and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

We 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. [ABSTRACT FROM AUTHOR]

This paper is motivated by seeking the exact complexity of resolution refutation of Tseitin formulas. We prove that the size of any regular resolution refutation of a Tseitin formula T (G , c) based on a connected graph G = (V , E) is at least 2 Ω (tw (G) / log | V |) , where tw (G) denotes the treewidth of a graph G. For constant-degree graphs, there is a known upper bound 2 O (tw (G)) poly (| V |) (Alekhnovich & Razborov Comput. Compl. 2011; Galesi, Talebanfard & Torán ACM Trans. Comput. Theory 2020), so our lower bound is tight up to a logarithmic factor in the exponent. Our proof consists of two steps. First, we show that any regular resolution refutation of an unsatisfiable Tseitin formula T (G , c) of size S can be converted to a read-once branching program computing a satisfiable Tseitin formula T (G , c ′) of size S O (log | V |) and this bound is tight. Second, we give the exact characterization of the nondeterministic read-once branching program (1-NBP) complexity of satisfiable Tseitin formulas in terms of structural properties of underlying graphs. Namely, we introduce a new graph measure, the component width (compw) and show that the size of a minimal 1 - NBP computing a satisfiable Tseitin formula T (G , c ′) based on a graph G = (V , E) equals 2 compw (G) up to a polynomial factor. Then we show that Ω (tw (G)) ≤ compw (G) ≤ O (tw (G) log (| V |)) and both of these bounds are tight. The lower bound improves the recent result by Glinskih & Itsykson (Theory Comput. Syst. 2021). [ABSTRACT FROM AUTHOR]

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 readonce 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 Gn on n vertices and an ϵ > 0, such that 1-NBP (∧, ∃ϵn ) refutations of the Tseitin formula for Gn 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 = ϵ logn, where n is the number of variables and ϵ > 0 is a constant. The lower bound is based on multiparty communication complexity. [ABSTRACT FROM AUTHOR]

Algebraic proof systems, such as Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR), refute contradictions using polynomials. Space complexity for such systems measures the number of distinct monomials to be kept in memory while verifying a proof. We introduce a new combinatorial framework for proving space lower bounds in algebraic proof systems. As an immediate application, we obtain the space lower bounds previously provided for PC/PCR [Alekhnovich et al. 2002; Filmus et al. 2012]. More importantly, using our approach in its full potential, we prove Ω (n) space lower bounds in PC/PCR for random &#954:-CNFs (κ ≥ 4) in n variables, thus solving an open problem posed in Alekhnovich et al. [2002] and Filmus et al. [2012]. Our method also applies to the Graph Pigeonhole Principle, which is a variant of the Pigeonhole Principle defined over a constant (left) degree expander graph. [ABSTRACT FROM AUTHOR]

Learners' difficulties with proof have been ascribed to their lack of understanding of functions that proof performs in mathematics, namely, verification, explanation, communication, discovery, and systematization. However, the extant mathematics education literature on validation of instruments designed to measure learners' beliefs about the functions of proof is scant. The purpose of this mixed methods study was to use the Standards for Educational and Psychological Testing (as discussed by the American Educational Research Association/American Psychological Association/National Council on Measurement in Education (AERA/APA/NCME), 2014) as a theoretical and methodological platform to support arguments for the validity of the learners' beliefs about the functions of proof (BAFP) instrument. Scale items were generated from de Villiers' model and a review of the literature, panel of experts, and key informants. The resulting instrument, comprising 28 Likert-scale items and 5 open questions that assessed the five functions of proof, was administered to 87 grade 11 learners in one high school in the Pinetown Education District, KwaZulu-Natal, South Africa. The results put the validity of the scores on the BAFP instrument into question. The study was an exploration of validity arguments based on the evidence from various data sources. Confirmatory factor analysis with a larger sample in a different context needs to be conducted to warrant the use of the BAFP instrument. The key contribution of this study to the field is that it sheds light on the complexities of instrument validation; the scope of the effort may explain why comprehensive validation efforts have not been documented extensively in literature. [ABSTRACT FROM AUTHOR]

We show a new connection between the clause space measure in tree-like resolution and the reversible pebble game on graphs. Using this connection, we provide several formula classes for which there is a logarithmic factor separation between the clause space complexity measure in tree-like and general resolution. We also provide upper bounds for tree-like resolution clause space in terms of general resolution clause and variable space. In particular, we show that for any formula F, its tree-like resolution clause space is upper bounded by space (π) (log (time (π)) , where π is any general resolution refutation of F. This holds considering as space (π) the clause space of the refutation as well as considering its variable space. For the concrete case of Tseitin formulas, we are able to improve this bound to the optimal bound space (π) log n , where n is the number of vertices of the corresponding graph [ABSTRACT FROM AUTHOR]

We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if and only if there is a Nullstellensatz refutation of the pebbling formula over G in size t + 1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system. [ABSTRACT FROM AUTHOR]

Resolution over linear equations is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res (lin R) , this refutation system operates with disjunctions of linear equations with Boolean variables over a ring R, to refute unsatisfiable sets of such disjunctions. Beginning in the work of Raz & Tzameret (2008), through the work of Itsykson & Sokolov (2020) which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. Garlik & Kołodziejczyk 2018; Itsykson & Sokolov 2020; Krajícek 2017; Krajícek & Oliveira 2018) made it evident that establishing lower bounds against general Res (lin R) refutations is a challenging and interesting task since the system captures a ``minimal'' extension of resolution with counting gates for which no super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds against general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular, we prove that the subset-sum principle 1 + ∑ i = 1 n 2 i x i = 0 requires refutations of exponential size over Q . We use a novel lower bound technique: We show that under certain conditions every refutation of a subset-sum instance f = 0 must pass through a fat clause consisting of the equation f = α for every α in the image of f under Boolean assignments, or can be efficiently reduced to a proof containing such a clause. We then modify this approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on n variables, hence also separating tree-like from dag-like refutations over the rationals. We then turn to the finite fields regime, showing that the work of Itsykson & Sokolov (2020), where tree-like lower bounds over F 2 were obtained, can be carried over and extended to every finite field. We establish new lower bounds and separations as follows: (i) For every pair of distinct primes p , q , there exist CNF formulas with short tree-like refutations in Res (lin F p) that require exponential-size tree-like Res (lin F q) refutations; (ii) random k-CNF formulas require exponential-size tree-like Res (lin F p) refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like Res (lin F) refutations of the pigeonhole principle, for every field F . [ABSTRACT FROM AUTHOR]

Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the first QBF system where (partial) strategies are built into the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-style calculus for DQBF, thus opening future avenues into CDCL-based DQBF solving. [ABSTRACT FROM AUTHOR]

We give a constructive account of Kripke–Curry's method which was used to establish the decidability of implicational relevance logic ( R → ). To sustain our approach, we mechanize this method in axiom-free Coq, abstracting away from the specific features of R → to keep only the essential ingredients of the technique. In particular we show how to replace Kripke/Dickson's lemma by a constructive form of Ramsey's theorem based on the notion of almost full relation. We also explain how to replace König's lemma with an inductive form of Brouwer's Fan theorem. We instantiate our abstract proof to get a constructive decision procedure for R → and discuss potential applications to other logical decidability problems. [ABSTRACT FROM AUTHOR]

Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution—introduced by Tseitin in the sixties—allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that—from the viewpoint of proof complexity—these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann's proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems. [ABSTRACT FROM AUTHOR]