# weighted_circular_and_semialgebraic_proofs__eb85375b.pdf

Journal of Artificial Intelligence Research 79 (2024) 447-482 Submitted 06/2023; published 02/2024

Weighted, Circular and Semi-Algebraic Proofs

Ilario Bonacina bonacina@cs.upc.edu Maria Luisa Bonet bonet@cs.upc.edu UPC Universitat Politecnica de Catalunya Jordi Girona, 1-3 08034 Barcelona, Spain

Jordi Levy levy@iiia.csic.es Artificial Intelligence Research Institute (IIIA) Spanish Research Council (CSIC) Campus UAB Carrer de Can Planas, Zona 2 08193 Barcelona, Spain

In recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs. In this paper we consider the proof systems circular Resolution, Sherali-Adams, Nullstellensatz and Weighted Resolution and we study their relative power from a theoretical perspective. We prove that circular Resolution, Sherali-Adams and Weighted Resolution are polynomially equivalent proof systems. We also prove that Nullstellensatz is polynomially equivalent to a restricted version of Weighted Resolution. The equivalences carry on also for versions of the systems where the coefficients/weights are expressed in unary. The practical interest in these systems comes from the fact that they admit efficient algorithms to find proofs in case these have small width/degree.

1. Introduction

The Satisfiability (SAT) and Maximum Satisfiability (Max SAT) problems are central in computer science. SAT is the problem of deciding if a given CNF formula has an assignment of 0/1 values that satisfies it. Max SAT is the optimization version of SAT. Given a CNF formula, we want to know what is the maximum number of clauses that can be satisfied by an assignment. SAT and the decision version of Max SAT are NP-complete. Problems in many different areas like planning, computational biology, circuit design and verification, etc. can be solved by encoding them into SAT or Max SAT, and then using a SAT or a Max SAT solver. Resolution-based SAT solvers can handle huge industrial instances successfully, but on the other hand, seemingly easy tautologies like the Pigeonhole Principle require exponentially long Resolution proofs (Haken, 1985). An important research direction is to implement SAT-solvers based on stronger proof systems than Resolution. To be able to do that, the proof systems should not be too strong, given that it is commonly believed that the stronger a proof system is, the harder it is to build efficient algorithms to find refutations for the

2024 The Authors. Published by AI Access Foundation under Creative Commons Attribution License CC BY 4.0.

Bonacina, Bonet, & Levy

sets of clauses. This is related to the notion of automatability (Bonet, Pitassi, & Raz, 2000; Atserias & M uller, 2019). To overcome the limitations of Resolution, in the last few years, a number of proof systems somewhat stronger than Resolution or with similar strength have been defined. Among them are proof systems based on Max SAT, such as Max SAT Resolution with Extension (Larrosa & Roll on, 2020), or Dual-Rail Max SAT (Ignatiev et al., 2017, Bonet et al., 2021, Morgado et al., 2019), or Weighted Dual-Rail Max SAT (Bonet et al., 2018, 2021), or the SAT-to-Max2SAT strategy (Ans otegui & Levy, 2021), or proof systems based on semialgebraic reasoning, for instance Sherali-Adams (Sherali & Adams, 1994; Dantchev, Martin, & Rhodes, 2009b) and Sub Cube Sum (Filmus et al., 2020), or proof systems allowing more general proof structures such as circular Resolution (Atserias & Lauria, 2019). A common feature of all these systems is that they have polynomial-size proofs of the Pigeonhole Principle. Sherali-Adams (SA) is equivalent to circular Resolution (c-Res) (Atserias & Lauria, 2019) and low degree version of SA is connected to the TFNP class PPADS (G o os, Hollender, Jain, Maystre, Pires, Robere, & Tao, 2022). Max SAT Resolution with Extension simulates Dual-Rail Max SAT (Larrosa & Roll on, 2020), and weighted Dual-Rail Max SAT simulates Resolution (Bonet et al., 2018). In the preliminary version of this work, Bonet and Levy (2020) defined weighted Resolution (w-Res), a system handling multisets of clauses with integer weights and proved the equivalence between weighted Resolution and circular Resolution. Concurrently and independently, Larrosa and Rollon (2020) and Rollon and Larrosa (2022) also proved a version of this equivalence for a proof system similar to weighted Resolution but working with infinite weights. The definition of weighted Resolution was inspired by the proof system Max SAT Resolution with Extension (Larrosa & Roll on, 2020). Indeed, weighted Resolution with weights in Z is equivalent to Max SAT Resolution with Extension, and it simulates Dual-Rail Max SAT.

1.1 Our Contributions

This paper uses the framework of weighted Resolution that can be applied to solve both SAT and Max SAT, the only difference being the presence or not of limitations on the weights of the initial clauses (see also Remark 1.1). In this paper we substantially extend and simplify the results on weighted Resolution by Bonet and Levy (Bonet & Levy, 2020). In weighted Resolution the initial clauses have positive weights and from them we infer new weighted clauses using substitution rules, i.e. rules that substitute the premises by the conclusions, in the manner of Max SAT Resolution. Arbitrary clauses may be introduced as assumptions at any time together with the same clause with the corresponding negative weight. The negative weights are a way to control these assumptions. The clauses with negative weights are eliminated by obtaining the same clause with positive weight. At the end of the proof we have a multiset of clauses containing the goal clause. In this multiset all weights must be positive, and therefore all the assumptions will have been justified. We simplify the equivalence between weighted Resolution and circular Resolution from (Bonet & Levy, 2020) (Theorem 4.3) and we give a direct proof of the equivalence of weighted

Weighted, Circular and Semi-Algebraic Proofs

Resolution and Sherali-Adams (Theorem 5.7). Unlike (Larrosa & Rollon, 2020; Rollon & Larrosa, 2022) working with finite weights allows us to have an explicit correspondence between weights in weighted proofs and flows in circular proofs. We also define a restricted version of weighted Resolution where at the end of the proof not only all weights are positive but also all the final clauses, except the goal one, are weakenings of the initial clauses. We prove that restricted weighted Resolution is equivalent to Nullstellensatz (NS), a well-studied algebraic proof system. This is also a new contribution. Both weighted Resolution and its restricted version might be considered with weights in unary (i.e. only 1). Those systems are equivalent to unary versions of Sherali-Adams and Nullstellensatz, proof systems that recently have been studied in connection with TFNP complexity classes (G o os et al., 2022). This is also a new contribution. Fig. 1 summarizes the simulations and equivalences among the proof systems we analyse in this paper.

Sherali-Adams (SA)

unary Sherali-Adams

tree-like Resolution

Nullstellensatz (NS)

unary Nullstellensatz

weighted Resolution (w-Res) Thm. 5.7

Circular Resolution (c-Res)

(Atserias & Lauria, 2019)

unary w-Res Thm. 5.7

restr. w-Res Thm. 5.7

restr. unary w-Res Thm. 5.7

Figure 1: Diagram of known p-simulations. P Q means that P p-simulates Q.

P Q means that P does not p-simulates Q. We omit from the figure the

arrows implied by transitivity. For instance, w-Res unary w-Res but we omit the arrow.

Remark 1.1 (SAT vs Max SAT proofs). Notice that the format of weighted Resolution can be used both in the context of SAT and weighted Max SAT, the only difference being that for weighted Max SAT the weights of the initial clauses are given as part of the input.

Bonacina, Bonet, & Levy

Instead, for SAT, the weights of the premises could be arbitrary. The equivalences between the weighted Resolution and the other systems equally hold in the context of Max SAT.

Bonacina and Bonet (2022) also showed that a well studied logic-based proof system (bounded-depth Frege) plus a weighted version of the Pigeonhole principle (that is given as axioms) simulates Sherali-Adams, and this is a limitation on the strength of the system given that Sherali-Adams efficiently proves that principle. Despite this limitation, we show that Sherali-Adams has polynomial refutations of combinatorial principles like the HEX principle (Section see 6), which is shown to be hard for Resolution (Buss, 2006).

1.2 Proof Search Algorithms

One of the reasons to study Sherali-Adams (circular Resolution, weighted Resolution) and Nullstellensatz (restricted weighted Resolution) is that they are in a sweet spot: they are powerful and yet not so powerful as to prohibit the existence of an efficient proof search algorithm (under some restrictions, such as width or degree). The question of finding refutations is a central question in automated theorem proving and SAT-solving that can be addressed more formally by the notion of automatability (Bonet, Pitassi, & Raz, 1997). A proof system P is automatable if there is an algorithm that, given as input an unsatisfiable CNF formula F, outputs a refutation of F in P and runs in time polynomial in the shortest P-refutation of F. Atserias and M uller (2020) showed that Resolution is not automatable, unless P = NP. Therefore, any SAT-solver based on Resolution (for instance CDCL-solvers) will likely require super-polynomial time even on unsatisfiable formulas that are easy to refute in Resolution. Similarly, de Rezende et al. (2021a) showed that NS is not automatable , unless P = NP. SA is also believed to be not automatable.1

Although the above systems are not automatable, they possess a weaker notion of automatability which allows refutations of small width/degree to be found efficiently: the degree/width-automatability. Given a formula in n variables, it is well-known that Resolution refutations of width w can be found in time n O(w) (Beame & Pitassi, 1996). Similarly, NS/SA refutations of degree d can be found by linear programming in time n O(d), see for instance the monograph on this subject by Fleming, Kothari, and Pitassi (2019). The fastest known algorithm to search for refutations of a CNF formula F in SA runs in time 2O( n log S), where S is the size of the smallest SA-refutation of F. This follows from Atserias and Hakoniemi s (2019) size-degree tradeoff for SA and the degree-automatability of SA. Despite the fact that the algorithms to find proofs in SA are not competitive with stateof-the-art SAT-solvers, this view of SA as circular/weighted Resolution might be useful to inspire better algorithms to find refutations in these systems which are stronger than Resolution.

1. de Rezende et al. (2021a) prove the non-automatability of NS and Polynomial Calculus, a sort of dynamic version of NS. In the same article there is the claim that SA is non-automatable, but this claim has been dropped. The non-automatability of SA is open.

Weighted, Circular and Semi-Algebraic Proofs

1.3 Organization of the Paper

Section 2 fixes preliminary definitions and notation. In Section 3, we introduce the notion of weighted proofs, weighted Resolution and restricted weighted Resolution and we prove basic facts about those systems. In Section 4, we recall the notion of circular proofs and circular Resolution and we show the equivalence between weighted and circular Resolution. In Section 5, we recall the definitions and basic properties of the algebraic proof systems Nullstellensatz and Sherali-Adams, and then we prove the equivalences between these systems and (restricted) weighted Resolution. In Section 6, we give examples of small degree Sherali-Adams refutations of some natural combinatorial principles.

2. Preliminaries

This section contains preliminaries and notation used through the whole paper. We postpone preliminaries only relevant to specific sections. For instance, the notion of circular proofs is only used in Section 4 and therefore it is presented there, and similarly the notions of Nullstellensatz and Sherali-Adams are used in Section 5 and therefore introduced there. For n N, let [n] := {1, 2, . . . , n}.

2.1 Clauses and CNF Formulas

A clause is a finite disjunction of literals, i.e. Boolean variables x or negated Boolean variables x. A clause C = ℓ1 ℓr has width r, noted as |C| = r. The empty clause is denoted as , and has width 0. A CNF formula is a set of clauses. The size of a formula is the total number of symbols in it. A truth-assignment is a function α : {x1, . . . , xn} {1, 0}, that is a function that assigns to each variable a truth-value True (1) or False (0). Truth-assignments evaluate literals, clauses, and CNF formulas in the natural way through the usual interpretation of negations and disjunctions. A truth assignment satisfies a clause C if it evaluates C to 1, if it evaluates C to 0 we say it falsifies F. A clause C is a logical consequence of a set of clauses S if every truth-assignment satisfying all clauses in S also satisfies C. For every truth-assignment, the clause evaluates to 0. A truth-assignment satisfies a CNF if it satisfies all the clauses in it. A CNF formula is a contradiction if every truth-assignment falsifies it.

2.2 Propositional Proof Systems

A propositional proof system is a polynomial-time function from {0, 1} to the set of propositional tautologies. A propositional proof system P p-simulates a propositional proof system Q if there is a polynomial-time function f such that P f = Q. If P p-simulates Q and Q p-simulates P we say that P and Q are p-equivalent. Several common proof systems are based on inference rules. An inference rule is given by two multisets of clauses F, G. The clauses in F are called antecedents (or premises), the clauses in G are called consequents (or conclusions). We denote inference rules as F G in inline math, and as F

Bonacina, Bonet, & Levy

in displayed equations. An instance of an inference rule F G is obtained by applying a substitution to the variables of the clauses in F and G.

Definition 2.1 (soundness). An inference rule F G is sound if any truth-assignment that satisfies all clauses in F, also satisfies all the clauses in G.

Definition 2.2 (strong soundness). An inference rule F G is strongly sound if for any truth-assignment, the number of falsified clauses in F equals the number of falsified clauses in G.

The notion of strong soundness was introduced in the context of Max SAT proof systems as an analogue of the classical soundness.

Definition 2.3 (inference-based proof). Given a set of sound inference rules R, a set H1, . . . , Hm of hypotheses clauses, and a goal clause G, a proof of G from H1, . . . , Hm (using the rules in R) is a sequence of clauses that starts with the clauses H1, . . . , Hm, ends in G, and such that every clause in the sequence is one of the consequents of an instance of an inference rule from R with all antecedents appearing earlier in the sequence. A refutation of H1, . . . , Hm is a proof of from H1, . . . , Hm. The size is the sum of the sizes of all the clauses in the sequence. The width is the maximum width of a clause in the sequence.

Resolution The propositional proof system Resolution (Res) is a well-known inferencebased proof system with inference rules

A B Weakening x x Excluded Middle ,

where A, B are clauses and x is a variable. For us, it is convenient to use the split rule instead of the weakening and the symmetric cut instead of the cut:

A Symm. Cut A

x A x A Split . (1)

This change results in a p-equivalent proof system with rules of Res strongly sound. Res is sound and complete, that is, if a clause is a logical consequence of a set of clauses there is a Res derivation of it and vice versa. It is well-known that if a CNF formula in n variables has Resolution refutations of width w then it has a Resolution refutation of size n O(w) (Beame & Pitassi, 1996). This result is tight: Atserias, Lauria, and Nordstr om (2016) showed that there are 3-CNF formulas that can be refuted in width w but require Resolution size nΩ(w). It is also well-known that Res is width-automatable, that is, if a CNF formula F in n variables has a Resolution refutation of width w then there is an algorithm running in time n O(w) that finds a Resolution refutation of F. See Section 1.2 for more details on automatability.

2.3 Proof Systems for Max SAT

Given a CNF formula F as input, SAT is the problem of determining if F is satisfiable, i.e. there exists a truth assignment satisfying all the clauses in F. Max SAT is the problem of

Weighted, Circular and Semi-Algebraic Proofs

finding an assigment that maximizes the number of satisfied clauses of F (or equivalently, an assignment which minimizes the number of unsatisfied clauses of F). Inference-based proof systems have also been used in the context of Max SAT to certify that, for a given CNF formula F, any truth assignment must falsify at least some number k of the clauses in F. Regarding the inference rules, it is convenient to use strongly sound inference rules (see Definition 2.2) and use them as substitution rules.

Definition 2.4 (inference-based proof for Max SAT). Given a set of strongly sound inference rules R, a multiset of clauses {H1, . . . , Hm} (hypotheses), and a goal clause G, a Max SATproof of G from H1, . . . , Hm (using the rules in R) is a sequence of multisets of clauses L1, . . . , Ls such that

1. L1 = {H1, . . . , Hm},

2. G Ls, and

3. for each i [s 1], there is a rule in R of the form A1, . . . , Aℓ B1, . . . , Br such that {A1, . . . , Aℓ} Li and Li+1 = Li \ {A1, . . . , Aℓ} {B1, . . . , Br}.

The size is the sum of the sizes of all the clauses in the sequence. A proof from H1, . . . , Hm of k copies of is certifying that every truth assignment falsifies at least k clauses among H1, . . . , Hm.

Examples of inference-based proof systems for Max SAT are Max SAT-Resolution (Larrosa & Heras, 2005) and the Max SAT system that uses R = {split, symm. cut}. G o os et al. (2022) defined a similar propositional proof system called reversible Resolution that also uses the split and symm. cut rules. The difference between our Max SAT system and reversible Resolution is that in our system the initial clauses are allowed to appear only once, since we are in the context of Max SAT. The notion of an inference-based proof system that replaces premises with conclusions was originally proposed in the context of Max SAT. However it can also be used in the context of SAT, since a derivation of a certifies the unsatifiability of the initial CNF formula. In the context of showing unsatisfiability of a set of clauses, these two systems above are p-simulated by Res, and probably strictly weaker, given that the rules are substitution rules and the same clause cannot be used multiple times. Some progress towards solving this open problem was achieved by Py et al. (2022) and Cherif et al. (2022). They show that if the Resolution refutation is crossing-free , then it can be converted into Max SAT Resolution with a polynomial increase in size. There are several possible ways to overcome the limitations imposed by the use of substitution rules. The easiest one is to allow an arbitrary number of multiple copies of the initial clauses or to use initial clauses with weights. Another is to use clever encodings of the initial clauses and then use the max SAT-Resolution rule. Examples of these encodings are the Dual-Rail encoding of Ignatiev et al. (2017), Morgado et al. (2019), and Bonet et al. (2018, 2021), and the SAT-to-Max2SAT strategy of Ans otegui and Levy (2021). The use of weighted clauses can be extended to a more powerful system allowing negative weights, intuitively meaning that a negative-weighted clause is an assumption yet to be justified.

Bonacina, Bonet, & Levy

3. Weighted Proofs and Weighted Resolution

In this section we develop formally the notion of weighted clauses and weighted Resolution with weights in Z.

Definition 3.1 (weighted clause). A weighted clause is a pair (C, w) where C is a clause and w Z. The width of a weighted clause (C, w) is the width of the clause C.

We consider multisets of weighted clauses modulo an equivalence relation, the fold-unfold equivalence.

Definition 3.2 (fold-unfold equivalence). Two multisets of weighted clauses F and G are fold-unfold equivalent (F G) if for every clause C, X

u:(C,u) F u = X

u:(C,u) G u .

For instance, for any clause C and u Z,

{(C, 2u)} {(C, u), (C, u)},

{(C, u), (C, u)}.

The fold-unfold equivalence between two multisets of weighted clauses may be seen as the application of the following inference rules as substitution rules:

(C, u) (C, v)

(C, u + v) Fold , (C, u + v)

(C, u) (C, v) Unfold ,

(C, 0) 0-Fold , (C, 0)

where C is a clause and u, v Z. The rules Fold/Unfold were previously considered in the context of weights in N, for instance in (Bonet et al., 2021) under the name Extraction/Contraction. The use of negative weights was used for the first time in the context of Resolution in (Larrosa & Roll on, 2020). In the context of Constraint Satisfaction Problems, negative weights were introduced by Cooper, de Givry, and Schiex (2007). The inference rules generalize to weighted clauses and the same happens with the notion of strongly sound inference rule (see Definition 2.2). Given any inference rule A1, . . . , As B1, . . . , Br we can transform it into the inference rule (A1, u), . . . , (As, u) (B1, u), . . . , (Br, u) on weighted clauses, where u Z. The following definition is the generalization of the notion of strong soundness to the context of weighted clauses.

Definition 3.3 (soundess for weighted inferences). The inference rule F G on weighted clauses is (strongly) sound if for any truth-assignment, the total weight of the falsified clauses in F equals the total weight of the falsified clauses in G, i.e. for every truth-assignment α, X

(C,u) F α(C)=0

(C,u) G α(C)=0

Weighted, Circular and Semi-Algebraic Proofs

We give now a notion of inference-based proof system in this context of weighted clauses. We use the fold-unfold equivalence and the inference rules as substitution rules, but we have to be careful with the negative weights. For instance, we saw that {(C, u), (C, u)}, this does not mean we have derived the weighted clause (C, u), but, we could see this as the fact that we are assuming the weighted clause (C, u), and (C, u) is there as bookkeeping : a reminder that eventually we have to prove (C, u). Formally the definition is the following.

Definition 3.4 (weighted proofs). Given a set of strongly sound inference rules R for weighted clauses, a set H of weighted clauses as hypotheses, and a goal weighted clause (C, u) with u > 0, a weighted proof of (C, u) from H is a sequence of multisets of weighted clauses (F1, . . . , Fs) such that:

2. For every proof step i [s 1], either it is a fold-unfold equivalence: Fi+1 Fi, or a regular inference: an instance of a rule in R of the form

(A1, u1) (As, us)

(B1, w1) (Br, wr)

where Fi+1 = Fi {(A1, u1), . . . , (As, us), (B1, w1), . . . , (Br, wr)}.

3. Fs contains (C, u), and possibly other weighted clauses, all of them with non-negative weights.

The size of a weighted proof is the total number of symbols occurring in F1, . . . , Fs including the encoding of the weights. A weighted refutation over R is a weighted proof of ( , u) for some positive u.

Notice that, in presence of fold-unfold equivalence item 2 in the definition of weighted proofs is equivalent to

2 . For every proof step i, either it is a fold-unfold equivalence: Fi+1 Fi, or a regular inference: an instance of a rule in R of the form

(A1, u1) (As, us)

(B1, w1) (Br, wr)

such that {(A1, u1), . . . , (As, us)} Fi and

Fi+1 = Fi \ {(A1, u1), . . . , (As, us)} {(B1, w1), . . . , (Br, wr)}.

We use this alternative presentation in the examples since it allows the use of slightly smaller multisets of clauses. In the proofs we instead use the presentation from the definition. A special case of weighted proofs is weighted Resolution.

Bonacina, Bonet, & Levy

Definition 3.5 (weighted Resolution, w-Res). A weighted Resolution (w-Res) derivation is a weighted proof where the set of inference rules for weighted clauses are the following, used as substitution rules:

(x A, u) ( x A, u)

(A, u) Symmetric-Cut (A, u)

(x A, u) ( x A, u) Split

(x x, u) Excluded Middle

where A is a clause, x is a variable, and u Z. Notice that, due to the fold-unfold, the Split and Symmetric-Cut can be seen as the same rule with opposite weights (one positive and one negative).

Without loss of generality we assume the weights of the application of the Excluded Middle to be always positive. The definition of w-Res generalizes ideas of Larrosa and Heras (2005) and Bonet et al. (2006, 2007) for weights in N and was introduced by Larrosa and Roll on (2020). The notion of w-Res could be generalized further to clauses with weights in arbitrary ordered monoids, like Q or Z { }. For simplicity, we focus on weights in Z since using weights in Q gives a p-equivalent system. This is easy to see by multiplying all the weights in Q by the minimum common multiple of the denominators. Notice that, we have two natural ways of representing the weights. We can represent a weight u in unary, or we can represent u in binary using ( log |u| + 1)-many bits. By the fold-unfold equivalence, the unary representation can be equivalently seen as restricting all the weights appearing in a weighted proof to be 1. Another way of restricting w-Res is by restricting the condition on the final multiset of a w-Res derivation.

Definition 3.6 (restricted weighted proofs, restricted w-Res). Given a set of strongly sound inference rules R for weighted clauses, a set H of weighted clauses as hypotheses, and a goal weighted clause (C, u) with u > 0, a restricted weighted proof of (C, u) from H is a sequence of multisets of weighted clauses (F1, . . . , Fs) satisfying the same conditions of Definition 3.4 with the exception of item 3. Instead, the multiset Fs satisfies the following condition.

3 . Fs contains (C, u), and possibly other weighted clauses, all of them with non-negative weights and weakening of weighted clauses in H, i.e. of the form (C D, w) where (C, w ) H, D is some clause, and w, w Z.

If we consider this for the set of inference rules in Definition 3.5, we call it restricted w-Res.

The system restricted w-Res is similar to the system reversible Resolution with terminals defined in (G o os et al., 2022). The difference between our system and theirs is that in reversible Resolution with terminals the weights are only allowed to be 1, therefore the clauses are considered with multiplicity. (Restricted) weighted proofs make sense both in the context of SAT and Max SAT. If we have a CNF formula F = {C1, . . . , Cm} over n variables we may work using some set

Weighted, Circular and Semi-Algebraic Proofs

of inference rules and use a (restricted) weighted proof to show the unsatisfiability of F: we have the freedom to choose the weights to give to C1, . . . , Cm, i.e. we look for weighted refutations of {(C1, u1), . . . , (Cm, um)} for some ui N. In the case of Max SAT we don t have this freedom: all the uis are 1. Similarly, in weighted Max SAT the uis are also given.

Theorem 3.7 (Soundness of weighted proofs). Let R a set of strongly sound inference rules on weighted clauses and F a multiset of weighted clauses. If there exists a weighted proof of ( , s) from F (using the rules in R), then every truth-assignment must falsify clauses in F with combined weight at least s, i.e. for every truth-assignment α X

(C,u) F α(C)=0

Proof. Let (F1, F2, . . . , Fℓ) be a weighted proof of ( , s) from F. Let α be a truthassignment and let cost(Fi, α) = X

(C,u) Fi α(C)=0

that is, cost(Fi, α) is the total-weight of the clauses from Fi falsified by α. Since F = F1, our goal is to show that cost(F1, α) s. By the soundness of the weighted inference rules, we have that

cost(F1, α) = cost(F2, α) = = cost(Fℓ, α) ,

and cost(Fℓ, α) = s + u1 + + ur where u1, . . . , ur are the weights of the other clauses in Fℓfalsified by α. All the weighted clauses in Fℓmust have positive weights, hence, cost(Fℓ, α) s and therefore cost(F1, α) s.

Notice that this proof generalizes trivially to sets of rules R satisfying a relaxed version of the strong soundness, where whenever F G the total weight of the falsified clauses in F is at least the total weight of the falsified clauses in G. That is for every truth-assignment α, X

(C,u) F α(C)=0

(C,u) G α(C)=0

Corollary 3.8 (soundness of (restricted) w-Res). Both w-Res and restricted w-Res are sound.

Theorem 3.9 (completeness of (restricted) w-Res). Both w-Res and restricted w-Res are complete, i.e. given a multiset of weighted clauses F, if for every truth-assignment α X

(C,u) F α(C)=0

then there exists a (restricted) w-Res derivation of ( , s) from F.

Bonacina, Bonet, & Levy

Proof. Using the fold-unfold equivalence expand each clause (C, u) in F into u copies of (C, 1). Then apply the split to each of those clauses on all the possible variables. If the clause C had width w all the split rules generate 2n w many clauses of width n and all of them weakening of C. After having done this for each clause in F, let L be the obtained multiset. Let CTn be the complete tree CNF formula on n variables, i.e. the set containing all possible 2n distinct clauses of width exactly n. Let w CTn = {(C, 1) : C CTn}, be the weighted version of CTn. The multiset L contains s copies of w CTn, where s is the minimum weight of the falsified clauses in F. To see this, suppose in L there are k copies of w CTn together with a satisfiable set of clauses A. Then there is a total assignment that satisfies all the clauses in A and falsifies exactly one clause in each w CTn, for a total of k clauses. By the strong-soundness then k s. It is immediate to see that w CTn has a w-Res derivation of ( , 1) where one only uses the symm. cut rule and the last multiset is just {( , 1)} (using Definition 3.4 item 2 ). Therefore, form L just using the symm. cut rule we obtain a ( , s). Since we apply the split rule only to weakenings of the initial axioms, the w-Res derivation we just described is also a restricted w-Res derivation.

Notice that, the completeness of weighted Max SAT Resolution, proved by Bonet et al. (2007), already implies the completeness of w-Res, since w-Res p-simulates weighted Max SAT Resolution. We conclude this section showing a sort of normal form for (restricted) w-Res derivations.

Lemma 3.10 (Normal form of w-Res). Any w-Res derivation (F1, . . . , Fs) can be converted in polynomial time, with a polynomial increase in size and identical width, to a w-Res derivation (F 1, . . . , F s) where all the regular inference steps have positive weights and there is a single application of the fold-unfold rule between F s 1 and F s. The same holds for restricted w-Res too.

Proof. Consider the w-Res derivation (F1, . . . , Fs). First we observe how to get rid of the negative weights in the applications of inference rules which could only be in Split and Symm. Cut. If from Fi to Fi+1 we applied a symm. cut {(x A, u), ( x A, u)} (A, u) with u 0 we have Fi+1 = Fi {(x A, u), ( x A, u), (A, u)} ,

which is the same as applying the split rule (A, u) {(x A, u), ( x A, u)} on Fi. Similarly, for the split (A, u) {(x A, u), ( x A, u)} with u 0 we use the symm. cut rule with weight u. Now, we want to push all the fold-unfold towards the end of the derivation. Let R be an instantiation of a rule and SR be the set of weighted clauses corresponding to the premises and conclusions of the rule, where the premises will have negative weight and the

Weighted, Circular and Semi-Algebraic Proofs

conclusions will have positive weight. We have that

F {(C, u1) . . . (C, us)} (u1 + . . . + us = v1 + . . . + vr) F {(C, v1) . . . (C, vr)} R F {(C, v1) . . . (C, vr)} SR

and F {(C, u1) . . . (C, us)} R F {(C, u1) . . . (C, us)} SR (u1 + . . . + us = v1 + . . . + vr) F {(C, v1) . . . (C, vr)} SR

are both valid derivations and the increase in size is just |SR|. This means that with just a polynomial increase in size we can push all the at the end of the derivation. Now, by the transitivity of , all of them can be done at once using fold-unfold equivalence.

4. Circular Proofs as Weighted Proofs

We show that weighted proofs are the equivalent to circular proofs. Atserias and Lauria (2019) introduced the notion of circular proofs as a way to enrich the structure of the proofs allowed in Frege systems. We recall the notion of circular Resolution and then we show the equivalence with weighted Resolution.

Definition 4.1 (circular Proof). Given a set of inference rules R , a set of hypotheses clauses H and a goal clause G, a circular derivation of G from H (over R) is a bipartite directed graph (I, J , E) where I, J are multisets, nodes are either inference rules (R I) or clauses (A J ), edges A R E denote the occurrence of clause A as an antecedent of the rule R, and edges R A E the occurrence of clause A as a consequence of the rule R. A function Flow : I N+ is called flow-assignment. Given a flow-assignment Flow, the balance of a clause A is

Bal(A, Flow) = X

R Nin(A) Flow(R) X

R Nout(A) Flow(R) ,

where Nin(A) = {R I | R A E} and Nout(A) = {R I | A R E} are the sets of neighbours of A. We will use Bal(A) to mean Bal(A, Flow) when the Flow function is clear from the context. To ensure the soundness, we require the existence of a flow-assignment Flow satisfying Bal(A, Flow) 0, for any clause A J \ H, and Bal(G, Flow) > 0, for the goal clause G. The clauses in H may have negative balance. The size of a circular proof derivation is the number of nodes in the bipartite graph and the width is the maximum width of a clause in it.

Definition 4.2 (circular Resolution, c-Res). A circular Resolution (c-Res) derivation is a circular proof using the set of inference rules R = {split, symmetric cut}.

Bonacina, Bonet, & Levy

Theorem 4.3. c-Res and w-Res are p-equivalent. Moreover, the width is either preserved (w-Res p-simulation of c-Res) or it increases by one (c-Res p-simulation of w-Res).

The two simulations in this theorem are proved separately in Lemma 4.5 and Lemma 4.6 below. Before proving formally the connections between c-Res derivations and w-Res derivations we give an example.

Example 4.4. We give an example of a c-Res derivation of {x, y, x y} from {x y z, x y z, x y, x}. See Figure 2 and Figure 4. Next to the c-Res derivation we show the corresponding w-Res derivation. To improve readability we apply immediately after each inference rule a fold-unfold equivalence. In the c-Res derivation we highlight in red the premises and in green the conclusions. Notice that in the symm. cut 1, we need to apply it with both premises with weight 2, and since x y only has weight 1, we are left with x y with weight 1 in the conclusions of the rule, and therefore it needs to be justified. Notice also that we proved the clause x with weight 2, but it is only used as a premise with weight 1, hence it remains in the conclusions of the proof.

symm. cut Flow=1 0

x y z x y z

symm. cut 1 Flow = 2

symm. cut 2 Flow=1

split 3 Flow=1

split 4 Flow=1

(x y z, 1) (x y z, 1) (x y, 2) ( x, 1) symm.cut & 0 (x y, 2) ( x, 1) (x y, 1) symm.cut & 1 ( x, 1) (x, 2) (x y, 1) symm.cut & 2 ( , 1) (x, 1) (x y, 1) split & 3 (y, 1) ( y, 1) (x, 1) (x y, 1) split & 4 ( y, 1) ( x y, 1) (x, 1)

Figure 2: A circular proof and its corresponding weighted proof.

Lemma 4.5. c-Res p-simulates w-Res. The weights of w-Res become the flows of c-Res (except on the initial clauses where they take the opposite sign).

Proof. Assume we have a w-Res derivation (F1, F2, . . . , Fℓ) of a weighted clause (C, w) with w > 0, from a multiset of weighted clauses F. That is, in particular, F1 = F and Fℓ

Weighted, Circular and Semi-Algebraic Proofs

Split Flow = 1

Symmetric-Cut Flow = 1

Figure 3: A constant size c-Res derivation of C from C.

contains the weighted clause (C, w) and the rest of weighted clauses in Fℓhave positive weights. Let H be the set of distinct clauses appearing in F. If the goal clause C is already in H, we just construct the c-Res derivation of C from C appearing in Figure 3. This c-Res derivation might increase the width in 1 and in a c-Res derivation the goal clause needs to have positive balance. Therefore the multiset of inference nodes cannot be empty since then C would have balance 0. In the rest of the argument we assume the goal clause C / H. By Lemma 3.10, we can suppose in (F1, F2, . . . , Fℓ) the regular inference rules are always applied with positive weights and there is a single fold-unfold step between Fℓ 1 and Fℓ. Recall that, if from Fi to Fi+1 we apply the rule

(A1, u) (As, u)

(B1, u), . . . , (Br, u) Rule R (2)

where u > 0, then Fi+1 = Fi {(A1, u), . . . , (As, u), (B1, u) (Br, u)}. We construct now a c-Res derivation associated to (F1, F2, . . . , Fℓ) and at the same time a flow-assignment. Consider the set J of all the distinct (unweighted) clauses appearing in Sl i=1 Fi and the multiset I of all the regular inference rules in (F1, F2, . . . , Fℓ), i.e. we do not consider the last fold-unfold inference step. For each instantiation of a Rule R as in eq. (2), we have an inference node R, we set Flow(R) = u and we create edges Ai R, for 1 = 1, . . . , s, and R Bj, for j = 1, . . . , r. Let G be the directed graph resulting from this construction. For each clause node A in G we have that its balance is

Bal(A, Flow) = X

R Nin(A) Flow(R) X

R Nout(A) Flow(R) .

From the construction of G and the assumptions on (F1, F2, . . . , Fℓ), for each clause A / H we have

{(A, Flow(R)) : R Nin(A)} {(A, Flow(R)) : R Nout(A)} Fℓ 1 ,

that is, in Fℓ, we have the clause (A, Bal(A)). By assumption this is a w-Res derivation of (C, w), therefore it must be that Bal(A) 0 for each J \ H and Bal(C) > 0.

Bonacina, Bonet, & Levy

Lemma 4.6. w-Res p-simulates c-Res. Given a flow-assignment of a c-Res proof, the corresponding balance will be the weights in w-Res (exept for the initial clauses where it takes the opposite sign).

Proof. Assume we have a c-Res derivation (I, J, E) with clauses nodes J, inference nodes I, edges E, hypotheses H J and goal clause C J. That is, there is a Flow assignment such that for each A J

Bal(A, Flow) = X

R Nin(A) Flow(R) X

R Nout(A) Flow(R) , (3)

where Bal(C, Flow) > 0, and for each A J \H, Bal(A, Flow) 0. Moreover, by elementary facts of linear programming, we can assume that for each R I, Flow(R) has bit-complexity polynomial in |I| + |J|. Without loss of generality, we assume that the hypotheses clauses do not have incoming edges, i.e. for any A H, Nin(A) = . If there was an incoming edge to A H, we can make a copy of A and use it to redirect the previous edge from the old A H to the new copy of A. Notice that redirecting these incoming edges in a circular proof only decreases the balance of hypotheses clauses (that are already allowed to have negative balance) and increases the balance of the copy. Without loss of generality we also assume the goal clause C is not in H. We produce a w-Res derivation by first placing the hypotheses H at the beginning, then introducing all the remaining clauses C J \ H, and, finally, applying all the rules R1, . . . , R|I| one by one with appropriate weights. More precisely, we construct multisets F 0 , F 0, F0, F1, . . . , F|I|, F|I|+1 such that in this order they form a valid w-Res derivation of (C, Bal(C, Flow)). The first multiset F 0 corresponds to all the hypotheses clauses with the appropriate weight: F 0 = {(A, Bal(A)) | A H} .

The second multiset F 0 is obtained from F 0 by fold-unfold equivalence and is the following:

F 0 = {(A, Bal(A)) | A H} {(A, Bal(A)), (A, Bal(A)) | A J \ H} .

The third multiset F0 is again fold-unfold equivalent to F 0 and is obtained expanding Bal(A) for all A J:

F0 = {(A, Bal(A)) | A J \ H} {(A, Flow(R)) | A J R Nout(A)} {(A, Flow(R)) | A J R Nin(A)} .

For i = 1, . . . , |I| we define

Fi = Fi 1 {(A, Flow(Ri)) | A Nin(Ri)} {(A, Flow(Ri)) | A Nout(Ri)} .

Weighted, Circular and Semi-Algebraic Proofs

Finally, F|I|+1 = {(A, Bal(A)) | A J \ H} .

Now, we prove that this is really a valid w-Res derivation of (C, Bal(C)). First we have to check that all weights in F 0 are non-negative. This is because all clauses A H only have outgoing edges, and therefore Bal(A) 0, and the weights in F 0 are positive. Then multisets F 0 , F 0 and F0 are all fold-unfold equivalent and hence valid steps in w-Res. Now, for each i [I] we see the step from Fi 1 to Fi as the application of the rule Ri with weight Flow(Ri). The premises of Ri are the clauses A such that A Nin(Ri) and the conclusions are the clauses A such that A Nout(Ri). The multiset F|I| then is the following:

F|I| = F0 {(A, Flow(R)) | R I A Nin(R)} {(A, Flow(R)) | R I A Nout(R)}

= {(A, Bal(A)) | A J \ H} {(A, Flow(R)) | A J R Nout(A)} {(A, Flow(R)) | A J R Nin(A)} {(A, Flow(R)) | R I A Nin(R)} {(A, Flow(R)) | R I A Nout(R)} ,

Now, trivially, for R I and A J we have R Nin(A) if and only if A Nout(R) and, similarly, R Nout(A) if and only if A Nin(R), therefore

F|I|+1 = {(A, Bal(A)) | A J \ H} F|I| .

Moreover, all the weights in F|I|+1 are non-negative and (C, Bal(C)) F|I|+1.

Notice that the same argument we used in Theorem 4.3 generalizes trivially to a generic set of inference rules, provided that Lemma 3.10 holds and the rules allow having constant size c-Res derivations of clauses from themselves as in Figure 3.

5. Algebraic Proofs as Weighted Proofs

In Section 4 we showed that w-Res and c-Res are equivalent proof systems. In this section we show the connection between weighted proofs and (semi)-algebraic proof systems in particular the Nullstellensatz proof system and the Sherali-Adams proof system.

5.1 Extra Preliminaries

Let X be the set of variables x1, . . . , xn, x1, . . . , xn. The variables in X are intended to be Boolean and the xi s are new variables with intended meaning the negation of the xi s. By Z[X] we denote the set of polynomials in the variables X and coefficients in Z.

5.1.1 Nullstellensatz

The Nullstellensatz proof system (NS) was introduced by Beame, Impagliazzo, Krajicek, Pitassi, and Pudlak (1994) and it is a way to get a proof system from (the weak form of) Hilbert s Nullstellensatz.

Bonacina, Bonet, & Levy

Definition 5.1 (Nullstellensatz, NSZ). Given polynomials p1, . . . , pm, s in Z[X], a Nullstellensatz (NSZ) derivation of the equality s = 0 from the set of equalities {p1 = 0, . . . , pm = 0} is a polynomial identity of the form

i [m] qipi +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) = s , (4)

where qi, rj, r j Z[X]. A refutation of {p1 = 0, . . . , pm = 0} is a derivation of c = 0 where c is a non-zero constant. The size of the polynomial identity in (4) is the length of a bit-string representing the polynomials qi, rj, r j, including the coefficients. If all the coefficients are 1 we call the system unary NS. The degree of the polynomial identity in (4) is

max{deg qi + deg pi, deg rj + 2, deg r j + 1: i [m], j [n]} ,

where deg p is the degree of the polynomial p.

Notice that in the left hand side (LHS) of (4) we don t have a sum corresponding to polynomials x2 i xi. The reason is that they are not needed to enforce the variables xi to be Boolean, indeed:

x2 i xi = ( xi xi)(xi + xi 1) + (x2 i xi) .

NS is sound and complete, i.e. the set of equations {p1 = 0, . . . , pm = 0} is unsatisfiable over {0, 1}-assignments if and only if there is a NS refutation of it. NS together with an encoding of CNF formulas into sets of polynomials is a propositional proof system. A CNF formula {C1, . . . , Cm} is encoded as the set of polynomial equations {MCi = 0, . . . , MCm = 0}, where if C = W i I xi W j J xj, then MC is the monomial Q i I xi Q j J xj. This encoding has the property that if a truth-assignment α satisfies the clause C, then α satisfies the equation MC = 0, and if a truth-assignment α falsisfies the clause C, then α satisfies the equation MC = 1. It is not hard to see that unary NS p-simulates tree-like Res. NS is exponentially stronger than tree-like Res since it can prove efficiently the onto-functional pigeonhole principle. Interestingly, Bonacina and Bonet (2022) showed that, in some intuitive sense, the principles that NS can prove efficiently, and (tree-like) Res cannot, are just formulas easily reducible to the onto-functional pigeonhole principle. G o os et al. (2022) showed that degree-polylog(n) unary NS corresponds to the TFNP class PPAD. If a CNF formula in n variables has a degree-d NS refutation, then it has a refutation of size n O(d) and coefficients of size n O(1) when expressed in binary. This bound is also asymptotically tight, i.e. there are CNF formulas that can be refuted in degree-d NS but require size nΩ(d) (Loera et al., 2009). The main reason we have the formal variables xi is to allow this succinct encoding. Semantically the variable xi is equivalent to the polynomial 1 xi, but encoding the clause W i [n] xi as the equation Q i [n] xi = 0 is very different from encoding it as the polynomial equation Q i [n](1 xi) = 0 in terms of number of monomials. In NS we are not allowed to handle arbitrary algebraic expressions like Q i [n](1 xi), but only polynomials, that is sums of monomials. So, once written as a polynomial, Q i [n](1 xi) has an exponential number of monomials.

Weighted, Circular and Semi-Algebraic Proofs

A variant of NS without the xi variables (NS without twin variables) has been considered in the literature. Essentially it amounts to an identity as in (4) where each instance of xi is substituted with 1 xi and the resulting algebraic expression is expanded as a sum of monomials. This system is not suited to refute arbitrary CNF formulas due to the potential exponential size encoding of CNFs, but it might be used to refute k-CNF formulas for k = O(log n). de Rezende et al. (2021b) showed that this version of NS without twin variables is exponentially weaker than NS.

Remark 5.2. The Nullstellensatz proof system could be defined for polynomials with coefficients in arbitrary rings, and a special case of interest is polynomials with coefficients in finite fields such as GF(2). The characterization of Nullstellensatz as restricted w-Res (Lemmas 5.13 and 5.11) could be adapted to this more general context. Indeed, while w-Res cannot be generalized to GF(2), restricted w-Res could and, it would correspond to Nullstellensatz over GF(2) with minor adaptations of the arguments in Lemmas 5.13 and 5.11. For simplicity we focus on Nullstellensatz and polynomials with integer coefficients.

5.1.2 Sherali-Adams

The Sherali-Adams proof system was introduced by Dantchev (2007) and Dantchev, Martin, and Rhodes (2009a) as a way to get proof systems out of the hierarchy of relaxations introduced by Sherali and Adams (1990) to solve Integer Linear Programs.

Definition 5.3 (Sherali-Adams, SA). Given a set of polynomials p1, . . . , pm and a polynomial s in Z[X], a Sherali-Adams (SAZ) derivation of s 0 from p1 0, . . . , pm 0 is a polynomial identity of the form

i [m] qipi +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) + q = s , (5)

where q, qi, rj, r j Z[X] and additionally q, qi have only positive coefficients. A refutation of {p1 0, . . . , pm 0} is a derivation of c 0 for a positive constant c. The size of the polynomial identity in (5) is the length of a bit-string representing the polynomials q, qp, rj, r j, including the coefficients. If all the coefficients are 1 we call the system unary SA. The degree of the polynomial identity in (5) is

max{deg qi + deg pi, deg rj + 2, deg r j + 1, deg q: i [m], j [n]} ,

where deg p is the degree of the polynomial p.

An example of a SA derivation is in Example 5.8. In this section, we consider only Sherali-Adams over the ring Z, hence we refer to SAZ simply as SA, omitting the reference to Z. Similarly as for NS, in (5) we might want to eliminate the variables x1, . . . , xn, and hence consider the algebraic equality in (5) after the substitution xi for 1 xi, for each i [n]. As for NS, de Rezende et al. (2021b) showed that the resulting system is known to be exponentially weaker than SA. SA is sound and complete, i.e. the system of inequalities {p1 0, . . . , pℓ 0} is unsatisfiable over {0, 1}-assignments if and only if there is a SA refutation of it. SA together

Bonacina, Bonet, & Levy

with an encoding of CNF clauses into sets of polynomials is a propositional proof system. We use the same encoding as for NS with the only difference that an equality is encoded as two inequalities, i.e. the clause C = W i I xi W j J xj is encoded as the two inequalities

j J xj 0, Y

Notice that, the inequality Q i I xi Q j J xj 0 is indeed redundant since the corresponding polynomial could be thought as being part of the polynomial q in (5). Thus we say that the encoding of the clause C is just Q i I xi Q j J xj 0. We will not use it in this work, but the clause C could also be encoded as the linear inequality P i I xi + P j J xj 1. If a CNF formula in n variables has a degree-d SA refutation, then it has a refutation of size n O(d). See Section 1.2 for more details. This bound is also asymptotically tight, i.e. there are CNF formulas that can be refuted in degree-d SA but require size nΩ(d) regardless of the degree (Atserias et al., 2016). Under this encoding of CNF formulas, it is immediate to see that SA p-simulates NS and it is also well-known that SA p-simulates Res, see for instance Lemma 3.5 of (Atserias & Ochremiak, 2018). Moreover, SA is exponentially stronger than Res since it can prove efficiently the pigeonhole principle. Interestingly, Bonacina and Bonet (2022) showed that, in some intuitive sense, what SA can prove efficiently and Res cannot, are just principles reducible to a weighted version of the pigeonhole principle. G o os et al. (2022) showed that degree-polylog(n) unary SA corresponds to the TFNP class PPADS.

5.2 Weighted Resolution and NS/SA

We now prove the equivalence between w-Res and SA, and between restricted w-Res and NS. To show that w-Res p-simulates SA we need a simple lemma giving a sort of normal form for SA/NS derivations. This lemma was implicitly used by Bonacina and Bonet (2022) and Fleming et al. (2022). The p-simulation of w-Res by SA generalizes and follows the known simulation of Res by SA. The next lemmas show that the qis in the definitions of NS and SA can be taken as positive constants. The first lemma shows that each product qipi, from the definitions of NS and SA, can be expressed in a different way.

Lemma 5.4. Given polynomials p, q Z[X], there are polynomials r1, . . . , rn, a polynomial q in Z[X] and a non-negative constant a such that

qp = (a q )p + X

j [n] rj(xj + xj 1) , (6)

where q has all coefficients non-negative. The degrees of q and rj(xj + xj 1) are at most the degree of q.

Proof. Let bxjm be a monomial in q, where b Z. If b < 0 consider the monomial bxjm to be part of q . If b > 0 then we can rewrite bmxjp as

bmxjp = bmp(xj + xj 1) bm xjp + bmp .

Weighted, Circular and Semi-Algebraic Proofs

Now we consider bmp(xj + xj 1) as an element of P j rj(xj + xj 1), and the monomial bm xj as part of q . The procedure is repeated now on the polynomial bmp exhausting all the variables in m one by one. If the monomial in q is bm xj the identity used is analogous. At the end we are left with a positive constant a equal to the sum of all positive coefficients b corresponding to monomials in q.

From this auxiliary lemma we have two normal forms, one for NS and one for SA. Notice that, Atserias and Lauria (2019) also introduce a notion of normal form for SA proofs but this form is not related to the one we introduce here.

Lemma 5.5 (Normal form for NS proofs). Given a NS derivation as in eq. (4), it is possible to transform it, in polynomial time, into a NS derivation of the same degree and polynomially larger size, where all the polynomials qi have the form ai q i, ai is a positive constant and q i has positive coefficients.

Proof. Immediate from Lemma 5.4.

Lemma 5.6 (Normal form for SA proofs). Given a SA derivation as in eq. (5), if all the polynomials pi have negative coefficients then it is possible to transform it, in polynomial time, into a SA derivation

i [m] aipi +

rj(x2 j xj) + r j(xj + xj 1) + q = s , (7)

where ai s are positive constants, q, rj, r j Z[X], q has only positive coefficients, the degree is the same of the original derivation and the size is polynomially larger.

Proof. It is immediate from Lemma 5.4:

qipi = (ai q i)pi + X

j [n] rij(xj + xj 1) ,

but, by assumption pi has negative coefficients, hence the polynomial q ipi has positive coefficients and can be seen as part of the q-part of the SA derivation.

Notice, in particular, this normal form for SA holds when the initial set of polynomials is the encoding of a CNF formula.

Theorem 5.7. SA is p-equivalent to w-Res and NSZ is p-equivalent to restricted w-Res. The same p-equivalences hold between the unary version of the systems. Moreover, degree-d NS/SA derivations correspond to width-d w-Res derivations.

By Theorem 4.3, w-Res is p-equivalent to c-Res, and Atserias and Lauria (2019) showed that c-Res is p-equivalent to SA, therefore w-Res and SA are p-equivalent. We give now a direct and self-contained argument showing the p-equivalence of w-Res and SA that works also in the cases of NS and the systems with unary weights/coefficients. Before proving the equivalence between w-Res and SA, we complete Example 4.4.

Bonacina, Bonet, & Levy

Example 5.8 (Example 4.4 cont d). This is the continuation of Example 4.4 and Figure 2, that is an example of a c-Res/w-Res/SA derivation of {x, y, x y} from {x y z, x y z, x y, x}. In the language of SA, this means the polynomial inequality x y x y 0 is derivable from the set of inequalities { x y z 0, x yz 0, xy 0, x 0}. See Figure 4 below.

symm. cut Flow=1 0

x y z x y z

symm. cut 1 Flow = 2

symm. cut 2 Flow=1

split 3 Flow=1

split 4 Flow=1

(x y z, 1) (x y z, 1) (x y, 2) ( x, 1) symm.cut & 0 (x y, 2) ( x, 1) (x y, 1) symm.cut & 1 ( x, 1) (x, 2) (x y, 1) symm.cut & 2 ( , 1) (x, 1) (x y, 1) split & 3 (y, 1) ( y, 1) (x, 1) (x y, 1) split & 4 ( y, 1) ( x y, 1) (x, 1)

x y z x yz 2 xy x

+ x y(z + z 1) 0

+ 2 x(y + y 1) 1

+ (x + x 1) 2

(y + y 1) 3

y(x + x 1) 4

Figure 4: A circular proof, its corresponding weighted proof and the related Sherali-Adams proof.

To prove Theorem 5.7, we adopt a slightly more syntactic view of the clauses in a w-Res derivation: we consider clauses C = ℓ1 ℓr where literals might be repeated. In Res, w-Res, and c-Res those clauses are handled implicitly, i.e. identifying C ℓ ℓwith C ℓ. To facilitate the proof of Theorem 5.7, we consider w-Res derivations where this identification is done explicitly via the idempotency rule:

(C ℓ, u) Idempotency ,

Weighted, Circular and Semi-Algebraic Proofs

where C is a clause and ℓis a literal and u Z. Notice that this rule is redundant since the same conclusion could be obtained using Excluded Middle, Split and Symm. Cut in the following way:

(C ℓ ℓ, u) Excluded Middle (C ℓ ℓ, u) (ℓ ℓ, u) Split ... Split (C ℓ ℓ, u) (C ℓ ℓ, u) Symm. Cut (C ℓ, u)

For a clause C = W i I xi W j J xj, let

and vice versa, given a monomial m = Q i I xi Q j J xj, let

Using this translation, a clause C is encoded as the equality M(C) = 0 in NS, and as the inequality M(C) 0 in SA.

Lemma 5.9. Given multisets of weighted clauses F, G, we have that F and G are fold-unfold equivalent, F G, if and only if X

(C,w) F w M(C) = X

(C,w) G w M(C) .

Proof. By definition, F G means that for every clause C, X

w:(C,w) F w = X

w:(C,w) G w ,

w:(C,w) F w X

w:(C,w) G w

and therefore X

(C,w) F w M(C) = X

(C,w) G w M(C) .

Vice versa, if X

(C,w) F w M(C) = X

(C,w) G w M(C)

Bonacina, Bonet, & Levy

it means that X

w:(C,w) F w X

w:(C,w) G w

hence for each M(C) the coefficient in front of it must be 0 and the fact that F G follows immediately.

We split the various p-simulations in Theorem 5.7 into distinct lemmas.

Lemma 5.10. w-Res p-simulates SA.

Proof. Let F = {C1, . . . , Cℓ}. By Lemma 5.6, without loss of generality, an SA refutation of F has the form

i=1 ai M(Ci) +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) + X

i J a im i , (8)

for some positive constants c, ai, a i, polynomials rj, r j, and monomials m i. Or, equivalently

i J a im i =

i=1 ai M(Ci) +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) . (9)

Notice that the LHS of eq. (9) has only negative coefficients. The constant c is the weighted clause ( , c) and ai M(Ci) is (Ci, ai). We construct a w-Res refutation (L1, . . . , Ls) of F. The multiset

L1 = {(C1, a1), . . . , (Cℓ, aℓ)}

corresponds to Pℓ i=1 ai M(Ci). Suppose we already constructed Lt, then pick any binomial of the form am(x2 j xj), not already picked from the sum Pn j=1 rj(x2 j xj), and let

Lt+1 = Lt {(C(m) xj xj, a), (C(m) xj, a)} .

This is an application of the Idempotency rule. Continue this way until all the binomials from Pn j=1 rj(x2 j xj) are picked. Then continue with the trinomials from Pn j=1 r j(xj + xj 1). Suppose we constructed Lk, then pick any trinomial of the form am(xj + xj 1), not already picked from the sum Pn j=1 r j(xj + xj 1), and let

Lk+1 = Lk {(C(m) xj, a), (C(m) xj, a), (C(m), a)} .

This is an application of a symmetric cut. Continue this process until all the trinomials from Pn j=1 r j(xj + xj 1) are picked. Then, let Ls be the multiset we obtained, that is Ls is constructed by exhausting all the terms from the RHS of eq. (9). By the equality (9) and Lemma 5.9 this gives

Ls {( , c)} {(C(m i), a i) : i I} ,

Weighted, Circular and Semi-Algebraic Proofs

where recall that a i 0. Lemma 5.9 justifies that every clause with negative weight in the constructed proof has to have the same clause with the corresponding positive weight in Ls . Given the translation from monomials to clauses, we have constructed a w-Res derivation of width equal to the degree of the SA. Moreover, if the coefficients of the SA derivation are 1, the weights of the clauses in the w-Res derivation are 1 too.

Lemma 5.11. Restricted w-Res p-simulates NS.

Proof. In the case of a NS derivation the argument is analogous to the previous lemma. Let F = {C1, . . . , Cℓ}. A NS refutation of {M(C1) = 0, . . . , M(Cℓ) = 0} has the form

i [m] qi M(Ci) +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) , (10)

where qi, rj, r j Z[X] and c = 0. We have two cases c > 0 and c < 0. If c > 0 we apply the Normal Form of NS (Lemma 5.5) and get

i [m] (ai q i)M(Ci) +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) ,

where the ais are positive and all the q is have positive coefficients. We then change sign to both sides of the equality and get

i [m] q i M(Ci) = X

i [m] ai M(Ci) +

j=1 rj(x2 j xj) +

j=1 r j(xj + xj 1) .

If c < 0 we first change sign to both sides of (10) to reduce to the previous case. Then we argue as in the previous lemma. To conclude, the only new small fact to notice is that each monomial in the sum P i [m] q i M(Ci), is a weakening of an initial axiom, once translated to a weighted clause.

Lemma 5.12. SA p-simulates w-Res.

Proof. We show now how to convert a w-Res refutation into a SA refutation. Let (L1, . . . , Lt) be a w-Res refutation of some multiset of clauses F. We construct algebraic expressions S1, . . . , St with the property that Si = P (C, w) Li w M(C) and they are valid SA derivations. Let S1 = P (C, w) L1 w M(C). By assumption, all the clauses C in L1 are clauses from F. Then suppose we constructed an algebraic expression Si = P (C, w) Li w M(C) having the form of a SA derivation. We want then to construct Si+1.

If Li Li+1 let Si+1 = Si.

If Li+1 is obtained from Li by a Symmetric-Cut rule (C x, w) (C x, w) (C, w) , then add to the algebraic expression Si the terms

w M(C) + w M(C x) + w M(C x) = w M(C)(x + x 1) .

That is Si+1 = Si + w M(C)(x + x 1).

Bonacina, Bonet, & Levy

If Li+1 is obtained from Li by a Split rule (C, w) (C x, w) (C x, w), then add to Si the terms w M(C) w M(C x) w M(C x) = w M(C)(x + x 1) .

That is Si+1 = Si w M(C)(x + x 1).

If Li+1 is obtained from Li by a Idempotency rule (C x x, w)

(C x, w) then add to Si the terms w M(C x) + w M(C x x) = w M(C)(x2 x) .

That is Si+1 = Si + w M(C)(x2 x).

If Li+1 is obtained from Li by an Idempotency rule (C x x, w)

(C x, w) then add to Si the terms

w M(C x) + w M(C x x) = w M(C)( x2 x)

= w M(C)(x2 x)

+ (w M(C) x w M(C)x)( x + x 1) .

That is Si+1 = Si + w M(C)(x2 x) + (w M(C) x w M(C)x)( x + x 1).

If Li+1 is obtained from Li by an Excluded Middle rule (x x, w) then add to Si the terms

w M(x x) = wx x

= wx(x + x 1) + w(x2 x) .

That is Si+1 = Si wx(x + x 1) + w(x2 x).

It is immediate to see that Si+1 constructed above is such that

(C, w) Li+1 w M(C) ,

and in particular St = P (C, w) Lt w M(C). Since we started with a w-Res refutation in Lt, we have the weighted clause ( , c) for some c > 0, and all the other clauses have positive coefficients; therefore, St = c q where q is a polynomial with positive coefficients. Therefore St + q = c is a SA refutation.

Lemma 5.13. NS p-simulates restricted w-Res.

Proof. If instead of a w-Res refutation we had a restricted w-Res refutation, the argument is the same as in the previous lemma, the only difference is that now q is a sum of multiples of initial axioms, therefore Ss + q = c is a NS refutation.

6. Examples

In the previous sections we saw some simple examples of SA/w-Res/c-Res derivations in the context of exemplifying the equivalences among the systems. In this section we see two families of contradictions provable in SA that are hard for Res: the graph pigeonhole principle and the Hex principle. Moreover, there are polynomial time algorithms to find their SA proofs.

Weighted, Circular and Semi-Algebraic Proofs

6.1 The Graph-Pigeonhole Principle

Let pij with i [m] and j [n] be the Boolean variables of the pigeonhole principle. With the usual intended meaning that pij is 1 if the pigeon i flies to the hole j and 0 otherwise. The pigeonhole principle PHPm n is the conjunction of the clauses:

(totality axioms) _

j [n] pij for all i [m] ,

(injectivity axioms) pij pi j for all i = i [m] and for all j [n] .

The encoding of the pigeonhole principle PHPm n as a set of polynomial inequalities is

j [n] xij 0 : i [m]} { xijxi j 0 : i = i [m], j [n]} .

We use Boolean variables xij for the algebraic encoding and pij for the propositional encoding just for clarity: xij = 1 if and only if pij = 1. The formula PHPm n is unsatisfiable whenever m > n. Given a bipartite graph G with bipartition (P, H), the graph pigeonhole principle PHP(G) is PHP|P| |H| once restricted by the assignment mapping pij = 0 for each (i, j) / E(G), and for the algebraic encoding xij = 0, xij = 1 for each (i, j) / E(G). It is well known that PHPn+1 n has polynomial-size SA refutations, but it requires linear degree (see for instance (Rhodes, 2007)) and it is hard for Resolution. The same is true for the bijective pigeonhole principle, which is hard for Resolution but easy for Sherali-Adams (G o os et al., 2022). For completeness, in Appendix A, we give a short proof of PHPm n in the language of SA. Other, seemingly different, proofs of PHPm n were given in the language of c-Res (Atserias & Lauria, 2019, Theorem 4) and in the language of Max SAT Resolution with Extension by Larrosa and Rollon (2020). It is not hard to see that all those proofs are essentially the same argument seen in different languages.

Proposition 6.1. Let G be a bipartite graph with bipartition ([m], [n]) and m > n. PHP(G) has polynomial-size unary SA refutations of degree at most the degree of the graph G.

A direct consequence of Proposition 6.1 is that such refutations of PHP(G) can be found in time n O(d), where d is the maximum degree of G. We know that SA/c-Res/w-Res are able to p-simulate Res and to prove PHP(G). What other combinatorial principles can be proved efficiently by these systems? Informally, Bonacina and Bonet (2022) show that SA/c-Res/w-Res are able to prove (additionally to what Res is able to prove) only principles reducible to a weighted version of PHP(G). Notice that not all combinatorial principles reducible to PHPm n are provable efficiently in SA. For instance, the bit-encoding of PHPm n requires exponential size refutations in SA/w-Res/c-Res (Dantchev, Ghani, & Martin, 2020).

We can have principles that are equivalent to PHP(G) and efficiently refutable in SA, but such that the equivalence is not at all obvious. One of those principles is Hex. Buss (2006)

Bonacina, Bonet, & Levy

show that a formalization Hex and PHP(G) are equivalent modulo bounded-depth Frege reductions but is was not clear that such reduction could be carried out in systems working on clauses such as Resolution or Sherali-Adams (seen as weighted Resolution). Consider a Hex board of size n n, i.e. a parallelogram of size n n tiled with hexagons and the tiles at the border have colors Blue (B), Cyan (C), Magenta (M), and Red (R). See Fig. 5 for an example of Hex board with n = 8.

C R R R R R R R

M M M M M M M

Figure 5: A 8 8 Hex board with borders filled in.

There are two players that take turns coloring the tiles of the board. Player I colors tiles with either Blue or Cyan and Player II colors tiles with either Magenta and Red. The goal of Player I is to create a path consisting only of Blue-Cyan tiles connecting opposite sides of the board. Similarly, the goal of Player II is to create a path consisting only of Magenta-Red tiles connecting opposite sides of the board. Every completely filled Hex board has a winner, i.e. a path either consisting only of Blue-Cyan tiles or Red-Magenta tiles connecting opposite sides of the board. Intuitively, the HEXn formula asserts that there is no winner by forbidding those type of paths, and therefore it is unsatisfiable. We use two pairs of similar colors to express this principle as clauses; the non existence of a path connecting opposite sides of the board is expressed saying that there are no adjacent Red-Magenta or Blue-Cyan tiles. For the description of the HEXn formula we follow (Buss, 2006). Given an hexagon in position (i, j), it is adjacent to the hexagons in positions (i, j 1), (i, j + 1), (i + 1, j 1), (i + 1, j), (i 1, j 1), (i 1, j + 1). For each hexagon h we have 4 variables Bh, Ch, Mh, Rh indicating its color (B for Blue, C for Cyan, M for Magenta, R for Red). The formula HEXn is then the conjunction of the following clauses:

1. Unit clauses expressing that the borders of the board are pre-colored as in Fig. 5: i.e. the clauses B1,1, . . . , B1,n 1, R1,n, . . . , Rn 1,n, Cn,2, . . . , Cn,n, and M2,1, . . . , Mn,1.

2. Clauses stating that each hexagon gets exactly one color, i.e. for each hexagon h we have the clauses Bh Ch Mh Rh together with the clauses Bh Ch, Bh Mh, Bh Rh, Ch Mh, Ch Rh, and Mh Rh.

3. Clauses stating that no adjacent hexagons can be colored red-magenta or blue-cyan, i.e. the clauses Rh Mh , Bh Ch for each adjacent hexagons h, h .

The clauses above in the context of SA derivations gets encoded as the following inequalities

1. B1,1 0, . . . , B1,n 1 0, R1,n 0, . . . , Rn 1,n 0, Cn,2 0, . . . , Cn,n 0, and M2,1 0, . . . , Mn,1 0.

Weighted, Circular and Semi-Algebraic Proofs

2. For each hexagon h we have the inequalities Bh Ch Mh Rh 0 together with the inequalities Bh Ch 0, Bh Mh 0, Bh Rh 0, Ch Mh 0, Ch Rh 0, and Mh Rh 0.

3. The inequalities Rh Mh 0, Bh Ch 0 for each adjacent hexagons h, h .

Notice that, the inequalities in item 2 are semantically equivalent to

Bh + Ch + Mh + Rh = 1 ,

and this has also short SA derivations from item 2.

Proposition 6.2. HEXn has polynomial-size SA/c-Res/w-Res refutations.

The HEXn principle looks very different from a pigeonhole principle but indeed it is a pigeonhole principle in disguise, see (Buss, 2006).

Proof. We construct a pigeonhole principle associated to HEXn. The set of pigeons P are all the vertices in the Hex n n board where exactly three tiles meet. The set of holes H are all the vertices in the same Hex board where exactly three tiles meet except the bottom-left vertex (where two Blue tiles and a Magenta tile meet). Each pigeon is only allowed to fly to the hole in the very same place where the pigeon is or to the (at most three) holes adjacent to it. Let G be this bipartite graph of degree at most 4 and let xij be the variables of PHP(G) in the polynomial encoding. For i P, let N(i) be the set of its neighbors in G. Notice that G has a loop in each vertex in P \H, in particular, for each i P \H, i N(i). By Proposition 6.1, we know there is a SA refutation of PHP(G) of the form

j N(i) xij X

i =i P j N(i) N(i )

pi,i ,jxijxi j

(qij(x2 ij xij) + q ij(xij + xij 1))

where ci s are positive constants, qij, q ij s are polynomials, and p, pi,i ,j s are polynomials with positive coefficients. Moreover, the size of the refutation is polynomial in |P| + |Q| = n O(1) and p has degree at most 4, the pi,i ,j s have degree at most 2, the qij s have degree at most 2 and the q ij s have degree at most 3. To get from this a small size refutation of HEXn we look at the variables xij not as indeterminates but as suitable polynomials in the variables of HEXn. In particular, the polynomials Q j N(i) xij, xijxi j, x2 ij xij, and xij + xij 1 are not axioms anymore but some polynomials we want to derive from the axioms of HEXn. For i P and j N(i), let l(i, j) be the hexagon on the left of the vector ij and r(i, j) be the hexagon on the right of the vector ij. We want the polynomial xij = 1 if l(i, j) has color Blue and r(i, j) has color Magenta, as in the following figure. In particular, the only vertex in P \ H (the one at the bottom

Bonacina, Bonet, & Levy

Figure 6: i and j are both pigeons and holes. The arrow shows pigeon i flying to hole j.

left of the Hex board) is mapped to its only neighbour in H. If no pair of tiles adjacent to i is colored Blue/Magenta, we set xii = 1. In other words, for i P and j N(i) \ {i}

xij = Bl(i,j)Mr(i,j) xij = 1 xij ,

j N(i)\{i} xij

j N(i)\{i} (1 Bl(i,j)Mr(i,j))

xii = 1 xii .

That is, by construction, the polynomials xij + xij 1 and xii + xii 1 are identically 0, and therefore derivable from the axioms of HEXn. First let s see what is the form of the polynomial p in eq. (11) now that it is a polynomial in the variables of HEXn. We use the following identity on the variables X1, . . . , Xk:

i [k] Xi = X

i [k] (Xi + Xi 1) Y

to encode the negated variables in low degree.

The polynomial p has degree at most 4 and positive coefficients. Monomials in p in the variables xij, xij, using the identity above, can be transformed into a sum of positive monomials in the variables of HEXn and multiples of Boolean axioms. Since the degree of p is constant this is just a polynomial increase in the size. For j N(i), the polynomial x2 ij xij has a simple derivation from the Boolean axioms of HEXn:

(Bl(i,j)Mr(i,j))2 Bl(i,j)Mr(i,j) = B2 l(i,j)(M2 r(i,j) Mr(i,j)) + Mr(i,j)(B2 l(i,j) Bl(i,j)) .

Similarly, it is not hard to see that x2 ii xii has a simple derivation from the Boolean axioms of HEXn. The polynomials Q j N(i) xij are also easy to derive from the Boolean axioms of HEXn since Y

j N(i) xij = xii(1 xii) .

Now consider the polynomials xij xi j of PHP(G). We have two cases.

Weighted, Circular and Semi-Algebraic Proofs

case 1: i, i , j are distinct vertices such that j N(i) N(i ), and the corresponding injectivity axiom xij xi j for PHP(G) is

xij xi j = Bl(i,j) Mr(i,j) Bl(i ,j) Mr(i ,j) .

Intuitively, this follows from HEXn since if the injectivity was violated then there would be a tile colored both Blue and Magenta, which is not allowed. More formally, either l(i, j) = r(i , j) or r(i, j) = l(i , j) and xij xi j is a multiple of an axiom of HEXn, an axiom stating that hexagons cannot be colored both Blue and Magenta.

case 2: i N(i) \ {i}, and the corresponding injectivity axiom xi i xii for PHP(G) is

xi i xii = Bl(i ,i) Mr(i ,i) Y

j N(i)\{i} (1 Bl(i,j)Mr(i,j))) .

Intuitively if the pigeon i flies to i, this means that the tile l(i , i) has color Blue and the tile r(i , i) has color Magenta. Then, the third tile incident to i, (1) must have some color, and (2) that color cannot be Cyan or Red. Therefore, its color must be Blue or Magenta and therefore i does not fly to i. Let l = l(i i), r = r(i , i) and h be the third hexagon adjacent to i. Then

xi i xii = Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml) .

We show this is derivable by a case analysis based on the color of h. The inequalities

Ch( Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml)) 0

Bh( Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml)) 0

Rh( Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml)) 0

Mh( Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml)) 0 ,

once expanded as sum of monomials, are all derivable from HEXn. Therefore, summing the previous derivations,

(Ch + Bh + Rh + Mh)( Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml)) 0

is also derivable from HEXn, and since Ch + Bh + Rh + Mh = 1, then

Bl Mr(1 Bl Mh)(1 Bh Mr)(1 Br Ml) 0

is also derivable.

A direct consequence of the proof of Proposition 6.2 and the degree-automatability of SA is that we can find SA refutations of HEXn in polynomial time in n using linear programming.

Acknowledgments

This work was supported by the Ministerio de Ciencia e Innovaci on/Agencia Estatal de Investigaci on MCIN/AEI/10.13039/501100011033, Spain [grant numbers PID2019-109137GBC21, PID2019-109137GB-C22, IJC2018-035334-I, PID2022-138506NB-C21].

Bonacina, Bonet, & Levy

Appendix A. Proof of the Pigeonhole Principle in SA

We prove Proposition 6.1. That is, given G be a bipartite graph with bipartition ([m], [n]) and m > n, PHP(G) has polynomial-size unary SA refutations of degree at most the degree of the graph G. First we consider PHPm n . Given j [n] and k [m] let Hkj = Q ℓ [k] xℓj and H0j := 1. Notice that Hk+1,j = xk+1,j Hkj. To improve readability, we highlight in yellow monomials with positive coefficients, in

blue Boolean axioms, in red injectivity axioms, and in green totality axioms. For j [n] we have the following equality by a telescopic sum

i [m] xij = Hm,j X

Hi 1,j( xij + xij 1 ) + xij xij Hi 1,j

where the underlined a polynomial has a simple SA derivation from PHPm n

xij xij Hi 1,j = X

xij Hℓ 1,j( xℓj + xℓj 1 ) Hℓ 1,j xijxℓj

That is, for each j [n] we have the following SA derivation of 1 P i [m] xij from PHPm n :

i [m] xij = Hm,j X

i [m] Hi 1,j( xij + xij 1 )

i [m] ℓ [i 1]

xij Hℓ 1,j( xℓj + xℓj 1 ) Hℓ 1,j xijxℓj

Let πj be the RHS of eq. (12). Similarly, for i [m] and k [n] let Pik = Q ℓ [k] xiℓ. Let Pi0 := 1. As before, Pi,k+1 = xi,k+1Pik and we have

j [n] xij 1 = Pi,n + X

Pi,j 1( xij + xij 1 ) + xij xij Pi,j 1

where the underlined polynomial has a simple SA derivation from PHPm n

xij xij Pi,j 1 = X

xij Pi,ℓ 1( xiℓ+ xiℓ 1 ) + Pi,ℓ 1xijxiℓ

That is, for each i [m] we have the following SA derivation of P j [n] xij 1 from PHPm n X

j [n] xij 1 = Pi,n + X

j [n] Pi,j 1( xij + xij 1 )

j [n] ℓ [j 1]

xij Pi,ℓ 1( xiℓ+ xiℓ 1 ) + Pi,ℓ 1xijxiℓ

Weighted, Circular and Semi-Algebraic Proofs

Let ρi be the RHS of eq. (13). We have that

j [n] πj + X

i [m] ρi = X

j [n] xij 1

= n m < 0 ,

and therefore P j [n] πj + P i [m] ρi = n m is a SA refutation of PHPm n . By inspecting the previous proof it is immediate to see that for PHP(G) the degree of the refutation is the maximum degree of the graph G, indeed PHP(G) is the result of restricting PHPm n mapping some variables xij to 0. Doing this same restriction to the proof above has the effect of shrinking its degree to the maximum degree of a vertex in G.

Ans otegui, C., & Levy, J. (2021). Reducing SAT to Max2SAT. In Proc. of the 30th International Joint Conference on Artificial Intelligence (IJCAI 21), pp. 1367 1373.

Atserias, A., & Hakoniemi, T. (2019). Size-degree trade-offs for sums-of-squares and positivstellensatz proofs. In Proc. of the 34th Computational Complexity Conference (CCC 19), Vol. 137, pp. 24:1 24:20.

Atserias, A., & Lauria, M. (2019). Circular (yet sound) proofs. In Proc. of the 22nd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 19), Vol. 11628, pp. 1 18.

Atserias, A., Lauria, M., & Nordstr om, J. (2016). Narrow proofs may be maximally long. ACM Trans. Comput. Logic, 17(3), 19:1 19:30.

Atserias, A., & M uller, M. (2019). Automating resolution is NP-hard. In Proc. of the 60th IEEE Annual Symp. on Foundations of Computer Science (FOCS 19), pp. 498 509.

Atserias, A., & M uller, M. (2020). Automating resolution is NP-hard. J. ACM, 67(5).

Atserias, A., & Ochremiak, J. (2018). Proof complexity meets algebra. ACM Trans. Comput. Logic, 20(1), 1 46.

Beame, P., Impagliazzo, R., Krajicek, J., Pitassi, T., & Pudlak, P. (1994). Lower bounds on Hilbert s Nullstellensatz and propositional proofs. In Proc. of the 35th Annual Symposium on Foundations of Computer Science (FOCS 94), pp. 794 806.

Beame, P., & Pitassi, T. (1996). Simplified and improved resolution lower bounds. In Proc. of the 37th Annual Symposium on Foundations of Computer Science (FOCS 96), pp. 274 282.

Bonacina, I., & Bonet, M. L. (2022). On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems. In Proc. of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 22), pp. 25:1 25:12.

Bonet, M. L., Buss, S., Ignatiev, A., Marques-Silva, J., & Morgado, A. (2018). Maxsat resolution with the dual rail encoding. In Proc. of the 32nd AAAI Conference on Artificial Intelligence (AAAI 18), pp. 6565 6572.

Bonet, M. L., Buss, S., Ignatiev, A., Morgado, A., & Marques-Silva, J. (2021). Propositional proof systems based on maximum satisfiability. Artificial Intelligence, 300, 103552.

Bonacina, Bonet, & Levy

Bonet, M. L., & Levy, J. (2020). Equivalence between systems stronger than resolution. In Proc. of the 23nd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 20), pp. 166 181.

Bonet, M. L., Levy, J., & Many a, F. (2006). A complete calculus for Max-SAT. In Proc. of the 9th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 06), pp. 240 251.

Bonet, M. L., Levy, J., & Many a, F. (2007). Resolution for Max-SAT. Artificial Intelligence, 171(8-9), 606 618.

Bonet, M. L., Pitassi, T., & Raz, R. (2000). On interpolation and automatization for Frege systems. SIAM J. Comput., 29(6), 1939 1967.

Bonet, M., Pitassi, T., & Raz, R. (1997). No feasible interpolation for TC0-Frege proofs. In Proc. of the 38th Annual Symposium on Foundations of Computer Science (FOCS 97), pp. 254 263.

Buss, S. R. (2006). Polynomial-size Frege and resolution proofs of st-connectivity and Hex tautologies. Theoretical Computer Science, 357(1), 35 52.

Cherif, M. S., Habet, D., & Py, M. (2022). From crossing-free resolution to max-sat resolution. In Solnon, C. (Ed.), 28th International Conference on Principles and Practice of Constraint Programming, CP 2022, July 31 to August 8, 2022, Haifa, Israel, Vol. 235 of LIPIcs, pp. 12:1 12:17. Schloss Dagstuhl - Leibniz-Zentrum f ur Informatik.

Cooper, M. C., de Givry, S., & Schiex, T. (2007). Optimal soft arc consistency. In Veloso, M. M. (Ed.), IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, pp. 68 73.

Dantchev, S., Martin, B., & Rhodes, M. (2009a). Tight rank lower bounds for the Sherali Adams proof system. Theoretical Computer Science, 410(21-23), 2054 2063.

Dantchev, S., Martin, B., & Rhodes, M. (2009b). Tight rank lower bounds for the Sherali Adams proof system. Theoretical Computer Science, 410(21), 2054 2063.

Dantchev, S. S. (2007). Rank complexity gap for lov asz-schrijver and sherali-adams proof systems. In Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing, STOC 07, p. 311 317, New York, NY, USA. Association for Computing Machinery.

Dantchev, S. S., Ghani, A., & Martin, B. (2020). Sherali-Adams and the binary encoding of combinatorial principles. In Proc. of the 14th Latin American Symposium (LATIN 20), Vol. 12118, pp. 336 347.

de Rezende, S. F., G o os, M., Nordstr om, J., Pitassi, T., Robere, R., & Sokolov, D. (2021a). Automating algebraic proof systems is NP-hard. In Proc. of the 53rd Annual ACM SIGACT Symposium on Theory of Computing (STOC), pp. 209 222. ACM.

de Rezende, S. F., Lauria, M., Nordstr om, J., & Sokolov, D. (2021b). The power of negative reasoning. In Proc. of the 36th Computational Complexity Conference (CCC 21), Vol. 200, pp. 40:1 40:24.

Weighted, Circular and Semi-Algebraic Proofs

Filmus, Y., Mahajan, M., Sood, G., & Vinyals, M. (2020). Max SAT resolution and subcube sums. In Proc. of the 23nd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 20), pp. 295 311.

Fleming, N., G o os, M., Grosser, S., & Robere, R. (2022). On semi-algebraic proofs and algorithms. In Proc. of the 13th Innovations in Theoretical Computer Science Conference (ITCS 22), Vol. 215, pp. 69:1 69:25.

Fleming, N., Kothari, P., & Pitassi, T. (2019). Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comput. Sci., 14(1-2), 1 221.

G o os, M., Hollender, A., Jain, S., Maystre, G., Pires, W., Robere, R., & Tao, R. (2022). Separations in proof complexity and TFNP. In Proc. of the 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS 22).

Haken, A. (1985). The intractability of resolution. Theoretical Computer Science, 39, 297 308.

Ignatiev, A., Morgado, A., & Marques-Silva, J. (2017). On tackling the limits of resolution in SAT solving. In Proc. of the 20th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 17), pp. 164 183.

Larrosa, J., & Heras, F. (2005). Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In Proc. of the 19th Int. Joint Conf. on Artificial Intelligence (IJCAI 05), pp. 193 198.

Larrosa, J., & Rollon, E. (2020). Towards a better understanding of (partial weighted) maxsat proof systems. In Proc. of the 23nd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 20), pp. 218 232.

Larrosa, J., & Roll on, E. (2020). Augmenting the power of (partial) Max SAT resolution with extension. In Proc. of the 34th Nat. Conf. on Artificial Intelligence (AAAI 20).

Loera, J. A., Lee, J., Margulies, S., & Onn, S. (2009). Expressing combinatorial problems by systems of polynomial equations and Hilbert s Nullstellensatz. Combinatorics, Probability and Computing, 18(4), 551 582.

Morgado, A., Ignatiev, A., Bonet, M. L., Marques-Silva, J., & Buss, S. (2019). DRMax SAT with Max HS: First contact. In Proc. of the 22nd Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 19), Vol. 11628, pp. 239 249.

Py, M., Cherif, M. S., & Habet, D. (2022). Proofs and certificates for max-sat. J. Artif. Intell. Res., 75, 1373 1400.

Rhodes, M. (2007). Rank lower bounds for the Sherali-Adams operator. In Cooper, S. B., L owe, B., & Sorbi, A. (Eds.), Computation and Logic in the Real World, pp. 648 659, Berlin, Heidelberg. Springer Berlin Heidelberg.

Rollon, E., & Larrosa, J. (2022). Proof complexity for the maximum satisfiability problem and its use in SAT refutations. J. Log. Comput., 32(7), 1401 1435.

Sherali, H. D., & Adams, W. P. (1990). A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM Journal on Discrete Mathematics, 3(3), 411 430.

Bonacina, Bonet, & Levy

Sherali, H. D., & Adams, W. P. (1994). A hierarchy of relaxations and convex hull characterizations for mixed-integer zero one programming problems. Discrete Applied Mathematics, 52(1), 83 106.