key: cord-0046689-g9kkx2b5
authors: Filmus, Yuval; Mahajan, Meena; Sood, Gaurav; Vinyals, Marc
title: MaxSAT Resolution and Subcube Sums
date: 2020-06-26
journal: Theory and Applications of Satisfiability Testing - SAT 2020
DOI: 10.1007/978-3-030-51825-7_21
sha: 813e93cefc7c32c33b5c4edf42500b444994c5dc
doc_id: 46689
cord_uid: g9kkx2b5

We study the 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 semialgebraic proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, is a special case of the 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.

The most well-studied propositional proof system is Resolution (Res), [5, 22] . It is a refutational line-based system that operates on clauses, successively inferring newer clauses until the empty clause is derived, indicating that the initial set of clauses is unsatisfiable. It has just one satisfiability-preserving rule: if clauses A ∨ x and B ∨ ¬x have been inferred, then the clause A ∨ B can be inferred. Sometimes it is convenient, though not necessary in terms of efficiency, to also allow a weakening rule: from clause A, a clause A ∨ x can be inferred. While there are several lower bounds known for this system, it is still very useful in practice and underlies many current SAT solvers.

While deciding satisfiability of a propositional formula is NP-complete, the MaxSAT question is an optimization question, and deciding whether its value is as given (i.e. deciding, given a formula and a number k, whether the maximum number of clauses simultaneously satisfiable is exactly k) is potentially harder since it is hard for both NP and coNP. A proof system for MaxSAT was proposed in [7, 14] . This system, denoted MaxSAT Resolution or more briefly MaxRes, operates on multi-sets of clauses. At each step, two clauses from the multi-set are resolved and removed. The resolvent, as well as certain "disjoint" weakenings of the two clauses, are added to the multiset. The invariant maintained is that for each assignment ρ, the number of clauses in the multi-set falsified by ρ remains unchanged. The process stops when the multi-set has a satisfiable instance along with k copies of the empty clause; k is exactly the minimum number of clauses of the initial multi-set that must be falsified by every assignment.

Since MaxRes maintains multi-sets of clauses and replaces used clauses, this suggests a "read-once"-like constraint. However, this is not the case; read-once resolution is not even complete [13] , whereas MaxRes is a complete system for certifying the MaxSAT value (and in particular, for certifying unsatisfiability). One could use the MaxRes system to certify unsatisfiability, by stopping the derivation as soon as one empty clause is produced. Such a proof of unsatisfiability, by the very definition of the system, can be p-simulated by Resolution. (The MaxRes proof is itself a proof with resolution and weakening, and weakening can be eliminated at no cost.) Thus, lower bounds for Resolution automatically apply to MaxRes and to MaxResW (the augmenting of MaxRes with an appropriate weakening rule) as well. However, since MaxRes needs to maintain a stronger invariant than merely satisfiability, it seems reasonable that for certifying unsatisfiability, MaxRes is weaker than Resolution. (This would explain why, in practice, MaxSAT solvers do not seem to use MaxRes -possibly with the exception of [20] , but they instead directly call SAT solvers, which use standard resolution.) Proving this would require a lower bound technique specific to MaxRes.

Associating with each clause the subcube (conjunction of literals) of assignments that falsify it, each MaxRes step manipulates and rearranges multi-sets of subcubes. This naturally leads us to the formulation of a static semi-algebraic proof system that we call the SubCubeSums proof system. This system, by its very definition, p-simulates MaxResW and is a special case of the Sherali-Adams proof system. Given this position in the ecosystem of simple proof systems, understanding its capabilities and limitations seems an interesting question.

1. We observe that for certifying unsatisfiability, the proof system MaxResW p-simulates the tree-like fragment of Res, TreeRes (Lemma 1). This simulation seems to make essential use of the weakening rule. On the other hand, we show that even MaxRes without weakening is not simulated by TreeRes (Theorem 1). We exhibit a formula, which is a variant of the pebbling contradiction [4] on a pyramid graph, with short refutations in MaxRes (Lemma 2), and show that it requires exponential size in TreeRes (Lemma 7). 2. We initiate a formal study of the newly-defined semialgebraic proof system SubCubeSums, which is a natural restriction of the Sherali-Adams proof system. We show that this system is not simulated by Res (Theorem 2).

3. We show that the Tseitin contradiction on an odd-charged expander graph is hard for SubCubeSums (Theorem 3) and hence also hard for MaxResW. While this already follows from the fact that these formulas are hard for Sherali-Adams [1] , our lower-bound technique is qualitatively different; it crucially uses the fact that a stricter invariant is maintained in MaxResW and SubCubeSums refutations. 4. Abstracting the ideas from the lower bound for Tseitin contradictions, we devise a lower-bound technique for SubCubeSums based on lifting (Theorem 4). Namely, we show that if every SubCubeSums refutation of a formula F must have at least one wide clause, then every SubCubeSums refutation of the formula F • ⊕ must have many cubes. We illustrate how the Tseitin contradiction lower bound can be recovered in this way.

The relations among these proof systems are summarized in the figure below, which also includes two proof systems discussed in Related Work. 

One reason why studying MaxRes is interesting is that it displays unexpected power after some preprocessing. As described in [12] (see also [18] ), the PHP formulas that are hard for Resolution can be encoded into MaxHornSAT, and then polynomially many MaxRes steps suffice to expose the contradiction. The underlying proof system, DRMaxSAT, has been studied further in [6] , where it is shown to p-simulate general Resolution. While DRMaxSAT gains power from the encoding, the basic steps are MaxRes steps. Thus, to understand how DRMaxSAT operates, a better understanding of MaxRes could be quite useful.

A very recent paper [15] studies a proof system MaxResE where MaxRes is augmented with an extension rule. The extension rule generalises a weighted version of MaxRes; as defined, it eliminates the non-negativity constraint inherent in MaxResW and SubCubeSums. This system happens to be equivalent to Circular Resolution [16] , which in turn is equivalent to Sherali-Adams [2] . It is also worth mentioning that MaxResW appears in [16] as MaxRes with a split rule, or ResS.

In the setting of communication complexity and of extension complexity of polytopes, non-negative rank is an important and useful measure. As discussed in [11] , the query-complexity analogue is conical juntas; these are non-negative combinations of subcubes. Our SubCubeSums refutations are a restriction of conical juntas to non-negative integral combinations. Not surprisingly, our lower bound for Tseitin contradictions is similar to the conical junta degree lower bound established in [10] .

We define the proof systems MaxRes, MaxResW, and SubCubeSums in Sect. 2 

For set X of variables, let X denote the set of all total assignments to variables in X. For a (multi-) set of F clauses, viol F : X → {0} ∪ N is the function mapping α to the number of clauses in F (counted with multiplicity) falsified by α. A (sub)cube is the set of assignments falsifying a clause, or equivalently, the set of assignments satisfying a conjunction of literals.

The proof system Res has the resolution rule inferring C ∨ D from C ∨ x and D ∨ x, and optionally the weakening rule inferring C ∨ x from C if x ∈ C. A refutation of a CNF formula F is a sequence of clauses C 1 , . . . , C t where each C i is either in F or is obtained from some j, k < i using resolution or weakening, and where C t is the empty clause. The underlying graph of such a refutation has the clauses as nodes, and directed edge from C to D if C is used in the step deriving D. The proof system TreeRes is the fragment of Res where only refutations in which the underlying graph is a tree are permitted. A proof system P simulates (p-simulates) another proof system P if proofs in P can be transformed into proofs in P with polynomial blow-up (in time polynomial in the size of the proof). See, for instance, [3] , for more details.

The MaxRes proof system operates on sets of clauses, and uses the MaxSAT resolution rule [7] , defined as follows:

The weakening rule for MaxSAT resolution replaces a clause A by the two clauses A∨x and A∨x. While applying either of these rules, the antecedents are removed from the multi-set and the non-tautologous consequents are added. If F is obtained from F by applying these rules, then viol F and viol F are the same function.

In the proof system MaxRes, a refutation of F is a sequence F = F 0 , F 1 , . . . , F s where each F i is a multi-set of clauses, each F i is obtained from F i−1 by an application of the MaxSAT resolution rule, and F s contains the empty clause . In the proof system MaxResW, F i may also be obtained from F i−1 by using the weakening rule. The size of the proof is the number of steps, s. In [7, 14] , MaxRes is shown to be complete for MaxSAT, hence also for unsatisfiability. Since the proof system MaxRes we consider here is a refutation system rather than a system for MaxSAT, we can stop as soon as a single is derived.

The SubCubeSums proof system is a static proof system. For an unsatisfiable CNF formula F , a SubCubeSums proof is a multi-set G of sub-cubes (or terms, or conjunctions of literals) satisfying viol F ≡ 1 + viol G .

We can view SubCubeSums as a subsystem of the semialgebraic Sherali-Adams proof system as follows. Let F be a CNF formula with m clauses in variables

; and a polynomial p 0 of the form

The degree or rank of the proof is the maximum degree of

. The polynomials f i corresponding to the clauses, as well as the terms in p 0 , are conjunctions of literals, thus special kinds of d-juntas (Boolean functions depending on at most d variables). So p 0 is a non-negative linear combination of non-negative juntas, that is, in the nomenclature of [11] , a conical junta.

The Sherali-Adams system is sound and complete, and verifiable in randomized polynomial time; see for instance [9] .

Consider the following restriction of Sherali-Adams:

This implies each q j must be 0, since the rest of the expression is multilinear. Hence, for some non-negative integral α A,B ,

f i This is exactly the SubCubeSums proof system: the terms in p 0 are subcubes, and the right-hand-side is viol F . For each disjoint pair A, B, the SubCubeSums proof has α A,B copies of the corresponding sub-cube. The degree of a SubCube-Sums proof is the maximum number of literals appearing in a conjunction. The size of a SubCubeSums proof is the number of subcubes, that is,

The constraint g i = 1 means that for bounded CNF formulas, the degree of a SubCubeSums proof is essentially the degree of p 0 , i.e. the degree of the juntas.

The following proposition shows why this restriction remains complete. In fact, SubCubeSums is also implicationally complete in the following sense. 

Since TreeRes allows reuse only of input clauses, while MaxRes does not allow any reuse of clauses but produces multiple clauses at each step, the relative power of these fragments of Res is intriguing. In this section, we show that MaxRes with the weakening rule, MaxResW, p-simulates TreeRes, is exponentially separated from it, and even MaxRes (without weakening) is not simulated by TreeRes.

Proof. Let T be a tree-like derivation of from F of size s. Without loss of generality, we may assume that T is regular; no variable is used as pivot twice on the same path.

Since a MaxSAT resolution step always adds the standard resolvent, each step in a tree-like resolution proof can be performed in MaxResW as well, provided the antecedents are available. However, a tree-like proof may use an axiom (a clause in F ) multiple times, whereas after it is used once in MaxResW it is no longer available, although some weakenings are available. So we need to work with weaker antecedents. We describe below how to obtain sufficient weakenings.

For each axiom A ∈ F , consider the subtree T A of T defined by retaining only the paths from leaves labeled A to the final empty clause. We will produce multiple disjoint weakenings of A, one for each leaf labelled A. Start with A at the final node (where T A has the empty clause) and walk up the tree T A towards the leaves. If we reach a branching node v with clause A , and the pivot at v is x, weaken A to A ∨ x and A ∨ x. Proceed along the edge contributing x with A ∨ x, and along the other edge with A ∨ x. Since T is regular, no tautologies are created in this process, which ends with multiple "disjoint" weakenings of A.

After doing this for each axiom, we have as many clauses as leaves in T . Now we simply perform all the steps in T .

Since each weakening step increases the number of clauses by one, and since we finally produce at most s clauses for the leaves, the number of weakening steps required is at most s.

We now show that even without weakening, MaxRes has short proofs of formulas exponentially hard for TreeRes. The formulas that exhibit the separation are composed formulas of the form F • g, where F is a CNF formula, g : {0, 1} → {0, 1} is a Boolean function, there are new variables x 1 , . . . , x for each original variable x of F , and there is a block of clauses C • g, a CNF expansion of the expression

We use the pebbling formulas on single-sink directed acyclic graphs: there is a variable for each node, variables at sources must be true, the variable at the sink must be false, and at each node v, if variables at origins of incoming edges are true, then the variable at v must also be true.

We denote by PebHint(G) the standard pebbling formula with additional hints u∨v for each pair of siblings (u, v)-that is, two incomparable vertices with a common predecessor-, and we prove the separation for PebHint(G) composed with the OR function. More formally, if G is a DAG with a single sink z, we define PebHint(G) • OR as follows. For each vertex v ∈ G there are variables v 1 and v 2 . The clauses are 

Note that the first three types of clauses are also present in standard composed pebbling formulas, while the last type are the hints.

We prove a MaxRes upper bound for the particular case of pyramid graphs. Let P h be a pyramid graph of height h and n = Θ(h 2 ) vertices.

Proof. We derive the clause s 1 ∨ s 2 for each vertex s ∈ P n in layered order, and left-to-right within one layer. If s is a source, then s 1 ∨ s 2 is readily available as an axiom. Otherwise assume that for a vertex s with predecessors u and v and siblings r and t -in this order -we have clauses u 1 ∨ u 2 ∨ s 1 ∨ s 2 and v 1 ∨ v 2 , and let us see how to derive s 1 ∨ s 2 . (Except at the boundary, we don't have the clause u 1 ∨ u 2 itself, since it has been used to obtain the sibling r and doesn't exist anymore.) We also make sure that the clause v 1 ∨ v 2 ∨ t 1 ∨ t 2 becomes available to be used in the next step.

In the following derivation we skip ∨ symbols, and we colour-code clauses so that green clauses are available by induction, axioms are blue, and red clauses, on the right side in steps with multiple consequents, are additional clauses that are obtained by the MaxRes rule but not with the usual resolution rule. The case where some of the siblings are missing is similar: if r is missing then we use the axiom u 1 ∨ u 2 instead of the clause u 1 ∨ u 2 ∨ s 1 ∨ s 2 that would be available by induction, and if t is missing then we skip the steps that use

Finally, once we derive the clause z 1 ∨z 2 for the sink, we resolve it with axiom clauses z 1 and z 2 to obtain a contradiction.

A constant number of steps suffice for each vertex, for a total of Θ(n).

We can prove a tree-like lower bound along the lines of [3] , but with some extra care to respect the hints. As in [3] we use the pebble game, a game where the single player starts with a DAG and a set of pebbles, the allowed moves are to place a pebble on a vertex if all its predecessors have pebbles or to remove a pebble at any time, and the goal is to place a pebble on the sink using the minimum number of pebbles. Denote by bpeb(P → w) the cost of placing a pebble on a vertex w assuming there are free pebbles on a set of vertices P ⊆ V -in other words, the number of pebbles used outside of P when the starting position has pebbles in P . For a DAG G with a single sink z, bpeb(G) denotes bpeb(∅ → z). For U ⊆ V and v ∈ V , the subgraph of v modulo U is the set of vertices u such that there exists a path from u to v avoiding U .

The canonical search problem of a formula F is the relation Search(F ) where inputs are variable assignments α ∈ {0, 1} n and the valid outputs for α are the clauses C ∈ F that α falsifies. Given a relation f , we denote by DT 1 (f ) the 1query complexity of f [17] , that is the minimum over all decision trees computing f of the maximum of 1-answers that the decision tree receives.

For all G we have DT 1 (Search(PebHint(G))) ≥ bpeb(G) − 1.

Proof. We give an adversarial strategy. Let R i be the set of variables that are assigned to 1 at round i. We initially set w 0 = z, and maintain the invariant that 1. there is a distinguished variable w i and a path π i from w i to the sink z such that a queried variable v is 0 iff v ∈ π i ; and 2. after each query the number of 1 answers so far is at least bpeb

Assume that a variable v is queried. If v is not in the subgraph of w i modulo R i then we answer 0 if v ∈ π i and 1 otherwise. Otherwise we consider p 0 = bpeb(R i → v) and p 1 = bpeb(R i ∪ {v} → w i ). By Lemma 4, bpeb(R i → w i ) ≤ max(p 0 , p 1 + 1). If p 0 ≥ p 1 then we answer 0, set w i+1 = v, and extend π i with a path from w i+1 to w i that does not contain any 1 variables (which exists by definition of subgraph modulo R i ). This preserves item 1 of the invariant, and since p 0 ≥ bpeb(R i → w i ), item 2 is also preserved. Otherwise we answer 1 and since p 1 ≥ bpeb(R i → w i ) − 1 the invariant is also preserved.

This strategy does not falsify any hint clause, because all 0 variables lie on a path, or the sink axiom, because the sink is assigned 0 if at all. Therefore the decision tree ends at a vertex w t that is set to 0 and all its predecessors are set to 1, hence bpeb(R t → w t ) = 1. By item 2 of the invariant the number of 1 answers is at least bpeb(G) − 1.

To complete the lower bound we use the Pudlák-Impagliazzo Prover-Delayer game [21] where Prover points to a variable, Delayer may answer 0, 1, or * , in which case Delayer obtains a point in exchange for letting Prover choose the answer, and the game ends when a clause is falsified. (Search(F ) ))) in tree-like resolution.

Proof. We use a strategy for the 1-query game of Search(F ) to ensure that Delayer gets DT 1 (F ) points in the Prover-Delayer game. If Prover queries a variable x i then -If x is already queried we answer accordingly. -Otherwise we query x. If the answer is 0 we answer 0, otherwise we answer * .

Our strategy ensures that if both x 1 and x 2 are assigned then x 1 ∨ x 2 = x. Therefore the game only finishes at a leaf of the decision tree, at which point Delayer earns as many points as 1s are present in the path leading to the leaf. The lemma follows by Lemma 6.

The formulas PebHint(P n ) • OR are easy to refute in MaxRes (Lemma 2), but from Lemmas 3,5, and 7, they are exponentially hard for TreeRes. Hence, Theorem 1. TreeRes does not simulate MaxResW and MaxRes.

In this section, we explore the power and limitations of the SubCubeSums proof system. On the one hand we show (Theorem 2) that it has short proofs of the subset cardinality formulas, known to be hard for resolution but easy for Sherali-Adams. On the other hand we show a lower bound for SubCubeSums for the Tseitin formulas on odd-charged expander graphs (Theorem 3). Finally, we establish a technique for obtaining lower bounds on SubCubeSums size: a degree lower bound in SubCubeSums for F translates to a size lower bound in SubCubeSums for F • ⊕ (Theorem 4).

We now show that Res does not simulate SubCubeSums.

There are formulas that have SubCubeSums proofs of size O(n) but require resolution length exp(Ω(n)).

The separation is achieved using subset cardinality formulas [19, 23, 25] . These are defined as follows: we have a bipartite graph G(U ∪ V, E), with |U | = |V | = n. The degree of G is 4, except for two vertices that have degree 5. There is one variable for each edge. For each left vertex u ∈ U we have a constraint e u x e ≥ d(u)/2 , while for each right vertex v ∈ V we have a constraint e v x e ≤ d(v)/2 , both expressed as a CNF. In other words, for each vertex u ∈ U we have the clauses i∈I x i for I ∈

The lower bound requires G to be an expander, and is proven in [19, Theorem 6] . The upper bound is the following lemma.

Proof. Our plan is to reconstruct each constraint independently, so that for each vertex we obtain the original constraints e u x e ≥ d(u)/2 and e v x e ≥ d(v)/2 , and then add all of these constraints together.

Formally, if F u is the set of polynomials that encode the constraint corresponding to vertex u, we want to write the equations

and

with c u,j , c v,j ≥ 0 and j c u,j = O(1), so that with c j = v∈U ∪V c v,j , we get

Hence we can write f ∈F f − 1 = j c j h j with j c j = O(n) and each c j ≥ 0. It remains to show how to derive Eqs. (1) and (2) . The easiest way is to appeal to the implicational completeness of SubCubeSums, Proposition 2. We continue deriving Eq. (1), assuming for simplicity a vertex of degree d and incident edges [d] . Let x I = i∈I x i , and let x I : I ∈

, or it falsifies it, in which case we have on the one hand g(x) = s > 0, and on the other hand

We proved that f ≥ g, therefore by Proposition 2 we can write f − g as a sum of subcubes of size at most 2 d = O(1).

Equation (2) can be derived analogously, completing the proof.

Fix any graph G with n nodes and m edges, and let I be the node-edge incidence matrix. Assign a variable x e for each edge e. Let b be a vector in {0, 1} n with i b i ≡ 1 mod 2. The Tseitin contradiction asserts that the system IX = b has a solution over F 2 . The CNF formulation has, for each vertex u in G, with degree d u , a set S u of 2 du−1 clauses expressing that the parity of the set of variables {x e | e is incident on u} equals b u .

These formulas are exponentially hard for Res [24] , and hence are also hard for MaxResW. We now show that they are also hard for SubCubeSums. By Theorem 2, this lower bound cannot be inferred from hardness for Res.

We will use some standard facts: For connected graph G, over F 2 , if i b i ≡ 1 mod 2, then the equations IX = b have no solution, and if i b i ≡ 0 mod 2, then IX = b has exactly 2 m−n+1 solutions. Furthermore, for any assignment a, and any vertex u, a falsifies at most one clause in S u .

A graph is a c-expander if for all 

For a cube C, define N i (C) = |C ∩ X i |. Then for all C ∈ C, N 1 (C) = 0, and so C is partitioned by X i , i ≥ 3. Let C be those cubes of C that have a non-empty part in X 3 . We will show that C is large. In fact, we will show that for a suitable S, the set C ⊆ C of cubes with |C ∩ X 5 | ≤ S|C ∩ X 3 | is large.

Defining the probability distribution μ on C as

,

We want to choose a good value for S so that A is very large, and B is Θ (1) . To see what will be a good value for S, we estimate the expected value of |C∩X5| |C∩X3| and then use Markov's inequality. For this, we should understand the sets X 3 , X 5 better. These set sizes are known precisely: for each odd i, |X i | = n i 2 m−n+1 . Now let us consider C ∩ X 3 and C ∩ X 5 for some C ∈ C . We rewrite the system IX = b as I X + I C X C = b, where X C are the variables fixed in cube C (to a C , say). So I X = b + I C a C . An assignment a is in C ∩ X r iff it is of the form a a C , and a falsifies exactly r equations in I X = b where b = b + I C a C . This is a system for the subgraph G C where the edges in X C have been deleted. This subgraph may not be connected, so we cannot use our size expressions directly. Consider the vertex sets V 1 , V 2 , . . . of the components of G C . The system I X = b can be broken up into independent systems; I (i)X (i) = b (i) for the ith connected component. Say a component is odd if j∈Vi b (i) j ≡ 1 mod 2, even otherwise. Let |V i | = n i and |E i | = m i . Any a falsifies an odd/even number of equations in an odd/even component.

For a ∈ C∩X 3 , it must falsify three equations overall, so G C must have either one or three odd components. If it has only one odd component, then there is another assignment in C falsifying just one equation (from this odd component), so C ∩ X 1 = ∅, a contradiction. Hence G C has exactly three odd components, with vertex sets V 1 , V 2 , V 3 , and overall k ≥ 3 components. An a ∈ C ∩ X 3 falsifies exactly one equation in I(1), I(2), I (3) . We thus arrive at the expression

Similarly, an a ∈ C ∩ X 5 must falsify five equations overall. One each must be from V 1 , V 2 , V 3 . The remaining 2 must be from the same component. Hence

We can deduce more by using the definition of μ, and the following fact: Since g = viol F − 1, an assignment in X 3 belongs to exactly two cubes in C, and by definition these cubes are in C . Similarly, an assignment in X 5 belongs to exactly four cubes in C, not all of which may be in C . Hence

Now we can estimate the average:

At S = n 2 /9, by Markov's inequality, B = Pr

Now we show that conditioned on |C∩X5| |C∩X3| ≤ S, the average value of 1 μ(C) is large.

So we must show that w(C) must be large. Each literal in C removes one edge from G while constructing G C . Counting the sizes of the cuts that isolate components of G C , we count each deleted edge twice. So

By the c-expansion property of G, Q1 ≥ cn i . If n i > n/2, it still cannot be too large because of the conditioning. Recall

So each n i ≤ 5n/6. Thus even when n i > n/2, we can conclude that n i /5 ≤ n/6 ≤ n − n i < n/2.

Choose c-expanders where c ensures w(C) + 1 − n = Ω(n). (Any constant c > 10.) Going back to our calculation of A from Eq. 3),

for suitable c > 10. Thus |C| ≥ |C | ≥ A · B ≥ 2 Ω(n) · (1/10) .

We describe a general technique to lift lower bounds on conical junta degree to size lower bounds for SubCubeSums. Before proving this theorem, we establish two lemmas. For a function h:

, 1} n and the ⊕ in α 1 ⊕ α 2 is taken bitwise.

Proof. Fix assignments α 1 , α 2 and let α = α 1 ⊕ α 2 . We claim that for each clause C ∈ F falsified by α there is exactly one clause D ∈ F • ⊕ that is falsified by α 1 α 2 . Indeed, by the definition of composed formula the assignment α 1 α 2 falsifies C • ⊕, hence the assignment falsifies some clause D ∈ C • ⊕. However, the clauses in the CNF expansion of C • ⊕ have disjoint subcubes, hence α 1 α 2 falsifies at most one clause from the same block. Observing that if α does not falsify C, then α 1 α 2 does not falsify any clause in C • ⊕ completes the proof. Proof. Let J be a conical junta of size s that computes f • ⊕ 2 . Let ρ be the following random restriction: for each variable x of f , pick i ∈ {0, 1} and b ∈ {0, 1} uniformly and set x i = b. Consider a term C of J of degree at least d > log 4/3 s. The probability that C is not zeroed out by ρ is at most (3/4) d < 1/s, hence the probability that the junta J ρ has degree larger than d is at most s · (3/4) d < 1. Hence there is a restriction ρ such that J ρ is a junta of degree at most d, although not one that computes f . Since for each original variable x, ρ sets exactly one of the variables x 0 , x 1 , flipping the appropriate surviving variables-those where x i is set to 1-gives a junta of degree at most d for f .

Proof (of Theorem 4). We prove the contrapositive. Assume F • ⊕ has a Sub-CubeSums proof of size s. Let H be the collection of s cubes in this proof. So viol F •⊕ − 1 = viol H . By Corollary 1, there is an integral conical junta for (viol F − 1) • ⊕ of size s. By Lemma 10 there is an integral conical junta for viol F − 1 of degree O(log s).

Recovering the Tseitin lower bound: This theorem, along with the Ω(n) conical junta degree lower bound of [10] , yields an exponential lower bound for the SubCubeSums and MaxResW refutation size for Tseitin contradictions.

A candidate for separating Res from SubCubeSums: We conjecture that the Sub-CubeSums degree of the pebbling contradiction on the pyramid graph, or on a minor modification of it (a stack of butterfly networks, say, at the base of a pyramid), is n Ω (1) . This, with Theorem 4, would imply that F •⊕ is hard for Sub-CubeSums, thereby separating it from Res. We have not yet been able to prove the desired degree lower bound. We do know that SubCubeSums degree is not exactly the same as Res width -for small examples, a brute-force computation has shown SubCubeSums degree to be strictly larger than Res width.

We placed MaxRes(W) in a propositional proof complexity frame and compared it to more standard proof systems, showing that MaxResW is between tree-like resolution (strictly) and resolution. With the goal of also separating MaxRes and resolution we devised a new lower bound technique, captured by SubCubeSums, and proved lower bounds for MaxRes without relying on Res lower bounds.

Perhaps the most conspicuous open problem is whether our conjecture that pebbling contradictions composed with XOR separate Res and SubCubeSums holds. It also remains open to show that MaxRes simulates TreeRes -or even MaxResW -or that they are incomparable instead.

Size-degree trade-offs for sums-of-squares and Positivstellensatz proofs

Circular (yet sound) proofs

Near optimal separation of treelike and general resolution

Short proofs are narrow-resolution made simple

Canonical expressions in boolean algebra

MaxSAT resolution with the dual rail encoding

Resolution for Max-SAT

An observation on time-storage trade off

Semialgebraic proofs and efficient algorithm design

Extension complexity of independent set polytopes

Rectangles are nonnegative juntas

On tackling the limits of resolution in SAT solving

Intractability of read-once resolution

A logical approach to efficient Max-SAT solving

Augmenting the power of (partial) MaxSAT resolution with extension

Towards a better understanding of (partial weighted) MaxSAT proof systems

Lifting theorems for equality

Horn maximum satisfiability: reductions, algorithms and applications

Long proofs of (seemingly) simple formulas

Maximum satisfiability using core-guided MaxSAT resolution

A lower bound for DLL algorithms for k-SAT (preliminary version)

A machine-oriented logic based on the resolution principle

sgen1: a generator of small but difficult satisfiability benchmarks

Hard examples for resolution

Zero-one designs produce small hard SAT instances