1.Introduction
The problem to decide whether a Boolean formula is satisfiable (SAT) is one of central problems in computer science, both theoretically and practically. From the theoretical side, SAT is the canonical NP-complete problem [19], making it intractable unless P = NP. From the practical side, the ‘SAT revolution’ [37] with the evolution of practical SAT solvers has turned SAT into a tractable problem for many industrial instances [8].
In this paper we consider the model counting problem (#SAT) which asks how many satisfying assignments a given Boolean formula has. While #SAT is obviously a generalization of SAT, it is presumably much harder. #SAT is the canonical complete problem for the function class #P. While FP = #P would imply P = NP, it is known that FP = #P is even equivalent to P = PP. The power of #SAT is also illustrated by Toda’s theorem [36] stating that any problem in the polynomial hierarchy can be solved in polynomial time with oracle access to #SAT.
Despite its higher complexity, #SAT solving has been actively pursued through the past two decades [26] and a number of #SAT solvers have been developed throughout the years. In fact, the past years have witnessed increased interest in #SAT solving with an annual model counting competition being organised since 2020 as part of the SAT conference [23]. #SAT solvers allow to tackle a large variety of real-world questions, including all kinds of problems in the areas probabilistic reasoning [2,31], risk analysis [22,40] and explainable artificial intelligence [3,34].
Unlike in SAT solving where conflict-driven clause learning (CDCL) [32] dominates the scene, there are a number of conceptually different approaches to #SAT solving, including the lifting of standard techniques from SAT-solving [35], employing knowledge compilation [30], and via dynamic programming [25]. While some approaches try to approximate the number of solutions, we will only consider exact model counting in the following.
There is a tight correspondence between practical SAT solving and propositional proof systems [14]. While we know that in principle every SAT solver implicitly defines a proof system, a seminal result of [1,33] established that CDCL (at least in its nondeterministic version) is equivalent to the resolution proof system. However, practical CDCL with e.g. the VSIDS heuristics corresponds to an exponentially weaker proof system than resolution [38]. In the same vein, there has recently been a line of research to understand the correspondence between solvers for quantified Boolean formulas (QBF) and QBF resolution proof systems [6,9,10]. This correspondence between solvers and proofs is not only of theoretical, but also of immense practical interest as it can be used for proof logging, i.e. for certifying the correctness of solvers on unsatisfiable SAT or QBF instances. Optimised proof systems have been devised in terms of RAT/DRAT for SAT [28,39] and QRAT for QBF [29] for this purpose. These proof systems aim to capture all modern solving techniques, including preprocessing and therefore tend to be very powerful [15,18]. In particular, in contrast to weak proof systems such as resolution, no lower bounds are known for RAT or QRAT.
In sharp contrast, far less is known about the correspondence of model counting solvers to proof systems. To our knowledge, there are currently three proof systems for #SAT. One is a static proof system based on decision DNNFs called kcps(#SAT) (the acronym stands for Knowledge Compilation based Proof System for #SAT) [16]. A very similar idea was used to modify current knowledge compilers such that they output certifiable decision DNNFs [17]. With the help of an implemented checker it can be verified in polynomial time that a given CNF is indeed equivalent to the resulting certifiable decision DNNF.
The second, a line based proof system called MICE [24] (the acronym stands for Model-counting Induction by Claim Extension), was introduced in 2022 [24]. Interestingly, the system MICE not only provides a theoretical proof system for #SAT, but also allows proof logging for a number of state-of-the-art solvers in model counting, including sharpSAT [35], DPDB [25] and D4 [30], as demonstrated in [24]. Hence MICE proofs can be used to verify the correctness of answers of these #SAT solvers.
A third proof system was introduced very recently [13] for certified proof checking of #SAT solvers. The system is similar in spirit to the general proof-checking formats RAT and DRAT [28,39] used for SAT solving and employs Partitioned-Operation Graphs (POGs).
1.1.Our Contributions
We perform a proof complexity analysis of the #SAT proof system MICE from [24]. Prior to this paper, no proof complexity results for MICE were known. Our results can be summarised as follows.
(a) A simplified proof system MICE’. We analyse the proof system MICE and define a somewhat simplified calculus MICE′. Lines in MICE are of the form ((F,V),A,c) where F is a propositional formula V is a set of variables, A is a partial assignment and c∈N. Semantically, these lines express that the formula F under the partial assignment A has precisely c models. The system MICE then employs four rules to derive new lines with the ultimate goal to derive a line ((F,vars(F)),∅,c). Thus in the ultimate line, c is the number of models of the formula F.
The four rules of the system include one axiom rule for satisfying total assignments and three rules to compose, join and extend existing lines. All the rules have a rather extensive set of side conditions to verify their applicability. For the composition rule this even includes an external resolution proof to check that the composition of claims in the rule indeed covers all models.
The variable set V does not feature in the semantical explanation above. While it might be tempting to choose V=vars(F) for all lines (as is done in the final claim), we show that this restriction is too strong and results in an exponentially weaker system. Nevertheless, we show that we can slightly adapt the rules of MICE (in particular the extension rule) and obtain a system MICE′ for which we can impose V=vars(F) for all lines without weakening the system. Lines in MICE′ therefore can take the form (F,A,c). This allows to eliminate and simplify some of the side conditions for the original rules of MICE when transferring to MICE′. Our simplified system MICE′ is as strong as MICE in terms of simulations (Propositions 4.8 and 4.9). Hence also MICE′ can be used for proof logging for the #SAT solvers mentioned above.
(b) Lower bounds for MICE and MICE’. We show an exponential lower bound for the proof size in MICE′ (and hence also for MICE) for a specific family of CNFs.
As mentioned above, the composition rule of MICE (and MICE′) incorporates resolution proofs. Exploiting this feature, it is not too hard to transfer resolution lower bounds to MICE′. In fact, we can show that on unsatisfiable formulas, resolution is polynomially equivalent to MICE′ (Theorem 5.1).
However, we would view such a transferred resolution lower bound not as a ‘genuine’ and interesting lower bound for MICE′. We therefore show a stronger bound for MICE′ for the number of proof steps (where we disregard the size of the attached resolution proofs). In our main result we show a lower bound of 2Ω(n) for the number of proof steps for a specific set of CNFs, termed XOR-PAIRSn, based on the parity function (Theorem 5.6). Technically, our lower bound is established by showing that in MICE′ proofs of XOR-PAIRSn, all applications of the join and extension rules preserve the model count.
(c) A connection between MICE and decision DNNFs. We show a tight connection between MICE′ and decision DNNFs. Specifically, we efficiently extract a decision DNNF from a MICE′ proof (Theorem 6.1). This provides an alternative way to obtain lower bounds for MICE′.
1.2.Organisation
The remainder of this article is organised as follows. After reviewing some standard notions from propositional logic and proof systems in Section 2, we revise the #SAT proof system MICE from [24] in Section 3 and show some properties of the system. This gives rise to a simplified proof system MICE′ which we define in Section 4. Section 5 contains our results on the exponential lower bound for MICE′ (and hence for MICE). In Section 6 we explain the connections to decision DNNFs, yielding additional MICE′ lower bounds. We conclude in Section 7 with relations to some open questions and future directions.
3.The Proof System MICE for #SAT
In this section we recall the MICE proof system for #SAT from [24] and show some basic properties of the system.
Definition 3.1
Definition 3.1([24]).
A claim is a triple ((F,V),A,c) where F is a propositional formula in CNF, V is a set of variables, A is an assignment with vars(A)⊆V and c∈N. For such a claim, let ModA(F,V):={α∈⟨V⟩∣α⊧F∪A}. The claim is correct if c=|ModA(F,V)|.
Claims will be the lines in our proof systems for model counting. Semantically, they describe that the formula F under the partial assignment A has exactly c models. The partial assignment A is sometimes also referred to as the assumption. What is perhaps a bit mysterious at this point is the role of the variable set V. We will get to this shortly.
The rules of MICE are Exactly One Model (1-Mod), Composition (Comp), Join (Join) and Extension (Ext). They are specified in Fig. 1. We give some intuition on the rules. The axiom rule (1-Mod) states that if a complete assignment A satisfies a formula F, then F has exactly one model under A.
Figure 1.
Inference rules for MICE [24].
![Inference rules for MICE [24].](https://content.iospress.com:443/media/sat/2024/15-1/sat-15-1-sat231507/sat-15-sat231507-g001.jpg)
With (Comp) we can sum up model counts of a formula F under different partial assignments A1,…,An in order to weaken the assumption to a partial assignment A. This is only sound if the solutions of F under assumptions A1,…,An form a disjoint partition of the full solution space of F under A. That this is indeed the case can be verified with an independent proof, e.g. in propositional resolution. This proof is called an absence of models statement. We want to emphasize that the rule (Comp) can be applied with n=0, i.e. we can derive any claim ((F,V),A,0) if A∪{C|V∣C∈F} is unsatisfiable. In particular, we can derive ((φ,vars(φ)),∅,0) for any unsatisfiable formula φ with a single application of (Comp).
The (Join) rule allows us to multiply the model counts of two formulas that are completely independent restricted to the assumptions. Finally, with (Ext), we can extend simultaneously all models, i.e. we enlarge the formula and assumption without changing the count.
We can now formally define MICE proofs.
Definition 3.2
Definition 3.2(Fichte, Hecher, Roland [24]).
A MICE trace is a sequence π=(I1,…,Ik) where for each i∈[k], either
Ii is a claim if Ii is derived by one of (1-Mod), (Join), (Ext) or
Ii=(I,ρ) if the claim I is derived by (Comp) and ρ is the resolution refutation for the respective absence of models statement.
A MICE proof of a formula φ is a MICE trace π=(I1,…,Ik) where Ik is (or contains in case of (Comp)) the claim ((φ,vars(φ)),∅,c) for some c∈N.
In [24] it is shown that MICE is a sound and complete proof system for #SAT.
For measuring the proof size, we use two natural options. s(π) notates the size of π which is the total number of claims plus the number of clauses in resolution proofs in the absence of models statements. c(π) counts only the number of claims a proof has which is exactly the number of inference steps that the proof needs.
In a correct claim ((F,V),A,c) the count c is uniquely determined by the formula F, set of variables V and assumption A. Therefore, we often omit c and refer to the claim as ((F,V),A). To ease notation we will usually just write a MICE proof as sequence of claims I1,…,Im and do not explicitly record the used absence of models statements. We just assume that whenever we use (Comp), the necessary resolution refutation is part of the MICE proof.
If a formula F is satisfied by the partial assignment A, we can set the remaining variables arbitrarily. Therefore, the component (F,vars(F)) has exactly 2|vars(F)|−|vars(A)| models under assumption A. The following construction shows that we can efficiently derive the corresponding claim in MICE.
Proposition 3.3.
If some assumption A satisfies an arbitrary formula F with vars(A)⊆vars(F), there is a MICE derivation of the claim I=((F,vars(F)),A,2|vars(F)∖vars(A)|) with s(π)=7⋅(|vars(F)∖vars(A)|) and c(π)=4⋅(|vars(F)∖vars(A)|).
Proof:
Let vars(F)∖vars(A)={x1,…,xn}. For every i∈[n] we derive Ii1=((∅,vars(A)∪{xi}),A∪{xi},1) and Ii0=((∅,vars(A)∪{xi}),A∪{x‾i},1) with (1-Mod). This is possible since every assignment satisfies the empty formula. With (Comp) we get Ii=((∅,vars(A)∪{xi}),A,2) using the absence of models statement ρi=((xi),(x‾i),□). We use (Join) of I1 and I2, then (Join) of the result and I3, and so on. The requirements (J-1), (J-2) and (J-3) are satisfied. In this way we get ((∅,vars(F)),A,2|vars(F)∖vars(A)|). We use (Ext) to obtain I=((F,vars(F)),A,2|vars(F)∖vars(A)|). It is easy to see that all requirements (E-1) to (E-5) are satisfied. For (E-4), we use that A satisfies F. In total we use 4n MICE steps to derive I and we have n absence of models statements with 3 clauses each. □
We investigate some properties that any claim in a MICE proof has to fulfill. We assume that any MICE proof has no redundant claims, i.e. in the corresponding proof dag, there is a path from any node to the final claim. We also observe that for all inference rules, the derived F and V never shrink. This leads to the following two observations:
Observation 3.4.
If ((F,V),A) is derived from ((F1,V1),A1) in a MICE trace (not necessarily in one step), then F1⊆F and V1⊆V.
Therefore, any claim ((F,V),A) in a MICE proof of φ fulfills F⊆φ and V⊆vars(φ).
From Definition 3.1 it is not obvious how F and V are related. Intuitively, one might be tempted to set V=vars(F) for any claim ((F,V),A). However, this would make the proof system exponentially weaker as we will see later. Lemma 3.6 will show that we can at least assume vars(F)⊆V for every claim. To show this we need the following lemma:
Lemma 3.5.
For any claim ((F,V),A) and any variable x, if x∈vars(F)∖V, then literals x and x‾ cannot both occur in F.
Proof:
Suppose there exists such an x. Since ((F,V),A) is not redundant, there is a path to the final claim. Thus, there have to be claims ((F1,V1),A1) and ((F2,V2),A2) directly adjacent in the path with F⊆F1⊆F2, V⊆V1⊆V2 and x∉V1, x∈V2. Now ((F2,V2),A2) is directly derived from ((F1,V1),A1) in one step. We argue that this is not possible:
It is impossible with (1-Mod), since this rule uses no previous claim.
It is impossible with (Comp), since V1≠V2.
It is impossible with (Join). Assume otherwise that ((F1,V1),A1) is joined with some ((F3,V3),A3). Because of x∈V2=V1∪V3 we have x∈V3. Then x∈vars(F1)∩(V3∖V1), contradicting condition (J-3).
It is impossible with (Ext). Otherwise x has to be in vars(A2) because of (E-2) and x∈V2∖V1 per construction. Then A2|V2∖V1 satisfies a clause in F1 since both literals x and x‾ occur in F1 (because F⊆F1). Thus condition (E-5) fails.
This leads to a contradiction. As a result, such an
x can not exist. □
Lemma 3.6.
Let a formula φ and a MICE proof π for φ be given. Then there is a MICE proof π′ satisfying vars(F)⊆V for any claim ((F,V),A)∈π′ such that s(π′)=O(s(π)3) and c(π′)=c(π).
Proof:
Let π=(I1,…,Im) with Ii=((Fi,Vi),Ai). Because of Lemma 3.5, for any i∈[m], we can assume that there is no variable x∈vars(Fi)∖Vi that occurs in both polarities in Fi. Let αi∈⟨vars(Fi)∖Vi⟩ be the assignment that does not satisfy any clause in Fi, i.e. if x is in Fi we assign αi(x)=0 and vice versa. For every claim Ii, αi exists and it is unique. We define
f(((Fi,Vi),Ai)):=((Fi,Vi∪vars(Fi)),Ai∪αi)
with the unique
αi defined above. Note that
Ai and
αi have no variables in common and are therefore consistent. The resulting claim on the right side satisfies the requirement we want to achieve.
We show by induction that (f(I1),…,f(Ik)) is a valid MICE trace for all k∈{0,…,m}. In the base case k=0 the empty trace is valid. For the induction step we assume that we have already derived f(I1),…,f(Ik−1). In particular, we have derived f(I) for every claim I we used to derive Ik. We consider the different rules from which Ik could be derived.
Exactly One Model. Ik=((Fk,Vk),Ak) is derived with (1-Mod). We can derive f(Ik)=((Fk,Vk∪vars(Fk)),Ak∪αk) with (1-Mod) as well.
(O-1). vars(Ak∪αk)=Vk∪vars(Fk) since vars(Ak)=Vk ((O-1) for Ik) and vars(αk)=vars(Fk)∖Vk.
(O-2). Ak∪αk satisfies Fk, since Ak satisfies Fk ((O-2) for Ik).
Composition. Ik=((Fk,Vk),Ak) is derived with (Comp) of claims Ii1,…,Iir with ij<k and Iij=((Fk,Vk),Aij) for j∈[r]. Let ρ be the absence of models statement ((C-3) for Ik) that refutes
{C|Vk∣C∈Fk}∪Ak∪{A‾ij∣j∈[r]}.
For
j∈[r] let
f(Iij)=((Fk,Vk∪vars(Fk)),Aij∪αk) with
αk=αij, since
αij does only depend on
Fk and
Vk and is therefore equal to
αk. To derive
f(Ik)=((Fk,Vk∪vars(Fk)),Ak∪αk) we can use (
Comp) of
f(Ii1),…,f(Iir):
(C-1). Aij∪αk assign the same variables and are pairwise inconsistent, since Aij assign the same variables and are pairwise inconsistent ((C-1) for Ik).
(C-2). For every j∈[r] we have Ak⊆Aij ((C-2) for Ik) and in particular Ak∪αk⊆Aij∪αk.
(C-3). We need an absence of models statement that refutes
{C|Vk∪vars(Fk)∣C∈Fk}∪(Ak∪αk)∪{Aij∪αk‾∣j∈[r]}=Fk∪Ak∪αk∪{(A‾ij∨α‾k)∣j∈[r]}
For this we do at most (|Fk|+r)⋅|αk|=O(|π|2) resolution steps to remove all αk literals from Fk and (A‾ij∨α‾k). Note that this is possible, since for any x∈lits(αk), only x‾ can appear in lits(Fk) per construction of αk. It remains exactly the formula that is refuted by ρ as all variables from αk are removed.
Join. Ik=((Fk,Vk),Ak)=((Fi∪Fj,Vi∪Vj),Ai∪Aj) is derived using (Join) of claims Ii=((Fi,Vi),Ai) and Ij=((Fj,Vj),Aj) with i,j<k. First, we show
vars(Fi)∖(Vi∪Vj)=vars(Fi)∖Vi.
The inclusion ⊆ follows directly. To show the other direction ⊇, assume x∈vars(Fi) and x∉Vi. Because of (J-3) for Ik is x∉vars(Fi)∩(Vj∖Vi). Thus, x∉Vj and therefore, x∈vars(Fi)∖(Vi∪Vj).
Using this we can prove
αk=αi∪αj.
For that it is sufficient to show that both sides assign the same variables and that they are consistent.
We show that vars(αk)=vars(αi)∪vars(αj). With the definitions of α and Fk we get vars(αk)=vars(Fk)∖Vk=vars(Fi∪Fj)∖(Vi∪Vj). Applying simple set operations and the equation from above, this is equal to (vars(Fi)∖(Vi∪Vj))∪(vars(Fj)∖(Vi∪Vj))=(vars(Fi)∖Vi)∪(vars(Fj)∖Vj). This is exactly vars(αi)∪vars(αj) per definition.
To show consistency of αi, αj and αk, we show that every pair is consistent. αi and αj are consistent: Otherwise suppose x∈lits(αi) and x‾∈lits(αj) for some literal x. Per construction is x‾∈lits(Fi), x∈lits(Fj) and therefore, x∈lits(Fk), x‾∈lits(Fk). Furthermore, var(x)∉(Vi∪Vj)=Vk. As a result, var(x)∈vars(Fk)∖Vk and x occurs in both polarities in Fk leading to a contradiction to Lemma 3.5. αk and αi are consistent: Assume x∈vars(αk) and x∈vars(αi) for some variable x. W.l.o.g. let x∈lits(αk). Then, x‾∈lits(Fk)=lits(Fi∪Fj) leading to x‾∈lits(Fi) and x∈lits(αi). Analogously we get that αk and αj are consistent.
To derive
f(Ik)=((Fk,Vk∪vars(Fk)),Ak∪αk)=((Fi∪Fj,Vi∪Vj∪vars(Fi)∪vars(Fj)),Ai∪Aj∪αi∪αj)
we can use (
Join) of
f(Ii)=((Fi,Vi∪vars(Fi)),Ai∪αi) and
f(Ij)=((Fj,Vj∪vars(Fj)),Aj∪αj):
(J-1). Ai and Aj are consistent because of (J-1) for Ik. We showed already that αi and αj are consistent. Ai and αj are consistent, because they have no variables in common. Otherwise let x be a variable with x∈vars(Ai) and x∈vars(αj). Per construction is x∈Vi, x∈vars(Fj) and x∉Vj and thus, x∈vars(Fj)∩(Vi∖Vj). This contradicts (J-3) for Ik. The same argument shows that Aj and αi are consistent.
As a result, Ai∪αi and Aj∪αj are consistent.
(J-2). First we show
Vi∩vars(αj)=∅andVj∩vars(αi)=∅.
For the sake of contradiction, assume there is a variable x with x∈Vi and x∈vars(αj). Per construction is x∈vars(Fj) and x∉Vj and thus x∈vars(Fj)∩(Vi∖Vj) which contradicts (J-3) for Ik. Analogously we get Vj∩vars(αi)=∅. Furthermore, (Vi∩Vj)⊆vars(Ar) for r∈{i,j} because of (J-2) for Ik. Using this, we get
(Vi∪vars(αi))∩(Vj∪vars(αj))=(Vi∩Vj)∪(vars(αi)∩vars(αj))∪(Vi∩vars(αj))∪(Vj∩vars(αi))=(Vi∩Vj)∪(vars(αi)∩vars(αj))⊆vars(Ar)∪(vars(αi)∩vars(αj))⊆vars(Ar)∪vars(αr)
for r∈{i,j}.(J-3). The requirement vars(Fi)∩((Vi∪Vj)∖Vi)=∅ is always fulfilled if the two joined claims satisfy vars(Fi)⊆Vi.
Extension. Ik=((Fk,Vk),Ak) is derived using (Ext) of Ii=((Fi,Vi),Ai) with i<k. Then we can also derive f(Ik)=((Fk,Vk∪vars(Fk)),Ak∪αk) from f(Ii)=((Fi,Vi∪vars(Fi)),Ai∪αi) with (Ext):
(E-1). Fi⊆Fk, Vi∪vars(Fi)⊆Vk∪vars(Fk) is fulfilled, since Fi⊆Fk and Vi⊆Vk because of (E-1) for Ik.
(E-2). We have to show (Vk∪vars(Fk))∖(Vi∪vars(Fi))⊆vars(Ak∪αk). For this, let x be an arbitrary variable with x∈(Vk∪vars(Fk))∖(Vi∪vars(Fi)). If x∈Vk, then x∈Vk∖Vi⊆vars(Ak) because of (E-2) for Ik. Otherwise if x∉Vk, x∈vars(Fk) and thus x∈vars(αk) per construction of αk.
(E-3). We have to show that (Ak∪αk)|Vi∪vars(Fi)=Ai∪αi. For this we use
Ak|Vi=Ai
which follows from (E-3) for Ik. Furthermore, by using Vi⊆Vk and vars(α)∩Vk=∅, we receive
αk|Vi=αk|Vk∩Vi=(αk|Vk)|Vi=∅.
Next, we prove
(Ak∪αk)|vars(Fi)∖Vi=αi.
For this we show that both assign the same variables and then that every variable is assigned equally.To show that both sides assign the same variables, the direction ⊆ follows with vars((Ak∪αk)|vars(Fi)∖Vi)⊆vars(Fi)∖Vi=vars(αi). For the other direction ⊇, let x∈vars(αi) implying x∈vars(Fi)∖Vi. Thus, we have to show that x∈vars(Ak∪αk). If x∈Vk, then x∈Vk∖Vi and thus, x∈vars(Ak) because of (E-2) for Ik. If x∉Vk, then x∈αk, since x∈vars(Fi)⊆vars(Fk).
In order to show that αk and αi are consistent, assume x∈vars(αk)∩vars(αi) and let x∈lits(αi). Then we have x‾∈lits(Fi)⊆lits(Fk) leading to x∈lits(αk). Ak, αi are consistent: Assume x∈vars(Ak)∩vars(αi) and let x∈lits(αi). Then x‾∈lits(Fi), x∉Vi, x∈Vk. Because of (E-5) for Ik, Ak|Vk∖Vi and in particular Ak|{x} does not satisfy any C∈Fi. Since there is a clause in Fi that contains literal x‾, x∈lits(Ak).
Using those three properties from above we get
(Ak∪αk)|Vi∪vars(Fi)=Ak|Vi∪αk|Vi∪(Ak∪αk)|vars(Fi)∖Vi=Ai∪αi.
(E-4). (Ak∪αk) satisfies Fk∖Fi, since Ak satisfies Fk∖Fi (E-4) for Ik.
(E-5). (Ak∪αk)|(Vk∪vars(Fk))∖(Vi∪vars(Fi)) does not satisfy C for any C∈Fi as the restricted assignment has no variables in vars(Fi).
This completes the induction. Since Im=((φ,vars(φ)),∅)=f(Im), π′=(f(I1),…,f(Im)) is a valid proof for φ with the claimed property. The number of claims does not change. The number of clauses in the refutation does only increase in the (Comp) case and at most by a factor of O(s(π)2). □
In the following we always assume vars(F)⊆V for any claim ((F,V),A). With this requirement, the conditions of the inference rules can be simplified.
Corollary 3.7.
If we require vars(F)⊆V for every claim ((F,V),A), the following simplifications for the MICE rules apply:
We can simplify the absence of models statement in the requirement (C-3) to be a refutation of F∪A∪{Ai‾∣i∈[n]}.
We can remove condition (J-3) for (Join).
We can remove condition (E-5) for (Ext).
However, imposing the stronger condition vars(F)=V for every claim ((F,V),A) would make the proof system exponentially weaker as we illustrate with the next proposition.
Lemma 3.8.
There is a family of formulas (Tn)n∈N such that for both measures s(⋅) and c(⋅) holds:
Tn has polynomial-size MICE proofs and
if vars(F)=V is required for all claims ((F,V),A), the shortest MICE proof of Tn has exponential size.
Proof:
Consider the family of formulas (Tn)n∈N that only have one clause
(x1∨x2∨⋯∨xn).
First we show that
Tn has a
MICE proof of size
O(n2) for every
n. With the construction of Proposition
3.3 we derive
I1=((Tn,vars(Tn)),{x1=1},2n−1),I2=((Tn,vars(Tn)),{x1=0,x2=1},2n−2),⋮In=((Tn,vars(Tn)),{x1=0,x2=0,…,xn−1=0,xn=1},1).
We apply (
Comp) to the one claim
In which results in
Jn=((Tn,vars(Tn)),{x1=0,x2=0,…,xn−1=0},1).
Then, we use (
Comp) of
Jn and
In−1 which results in
Jn−1=((Tn,vars(Tn)),{x1=0,x2=0,…,xn−2=0},3).
Similarly we apply (
Comp) to every pair of claims
Ii and
Ji+1 and finally get
J1=((Tn,vars(Tn)),∅,2n−1).
In total we need
O(n2) steps to derive all
Ii and
n applications of (
Comp) to combine these claims.
Next, we show that any MICE proof with the additional requirement vars(F)=V has size 2Ω(n). Note that the construction from Proposition 3.3 does not work under this additional requirement.
We show that the claim I∅=((∅,∅),∅,1) does not help for the proof. If we use (Join) on I∅ together with any claim I, the result is I. Similarly, if we derive I with (Ext) from I∅, we can derive I with (1-Mod) without I∅. If we apply (Comp) on claim I∅ together with some other claims, (C-1) implies that all used claims have to be I∅. Thus, (Comp) would result in I∅. Therefore, we can assume I∅ is not in the proof at all.
Thus, the only component we can use is C=({x1∨…∨xn},{x1,…,xn}). Assume I is derived with (Join) from I1=(C,A1) and I2=(C,A2). Condition (J-2) implies vars(A1)=vars(A2)={x1,…,xn} and in particular A1=A2 because of (J-1). Therefore, I=I1=I2 and the usage of (Join) is redundant. Let I=(C,A) be derived from I1=(C,A1) with (Ext). Because of (E-3) we have A=A1 and hence I=I1. Hence, the rules (Join) and (Ext) achieve nothing and we can assume that they do not appear in the proof.
As a result, the proof can only use rules (1-Mod) and (Comp). Such a proof needs 2n−1 applications of (1-Mod) as Tn has 2n−1 models. □
4.A Simplified Proof System MICE’ for #SAT
We now adapt MICE to a new proof system MICE′ that is as strong as MICE and only uses claims ((F,V),A) with components satisfying V=vars(F). Therefore, we can drop the explicit mentioning of the variable set V and only need to specify the formula F. This makes the resulting proof system more intuitive and easier to investigate for lower bounds.
The rules of MICE′ are Axiom (Ax), Composition (Comp’), Join (Join’) and Extension (Ext’). They are specified in Fig. 2.
Figure 2.
Inference rules for MICE′.
The intuition for the rules (Comp’) and (Join’) are very similar to (Comp) and (Join) from MICE. The (Ax) rule enables us to derive the claim (∅,∅,1) which is trivially true. (Ext’) is also similar to (Ext) with one important difference: If we use (Ext) in MICE, the assumption has to assign all variables that are added to the claim. As a result, we extend one model of the original claim to one new model. In (Ext’) however, this is not necessarily the case. As long as the new assumption satisfies all added clauses, we are allowed to leave new introduced variables unassigned in the assumption. Like this we extend every model of the original claim to a set of new models, one for every possible assignment of these unassigned variables.
Definition 4.1
Definition 4.1(Adapted Proof System MICE′).
A claim is a triple (F,A,c) with vars(A)⊆vars(F). For such a claim, let ModA(F):={α∈⟨vars(F)⟩∣α⊧F∪A}. The claim is correct if c=|ModA(F)|. The rules of MICE′ are (Ax), (Comp’), (Join’) and (Ext’). The notions of MICE′ traces and MICE′ proofs are defined analogously as for MICE. Furthermore, we use the same two measures for the proof size s(⋅) and c(⋅).
As in the MICE proof system we often omit the count c of claims and assume that no redundant claims exist in MICE′ proofs, i.e. all claims are connected to the final claim.
We prove that all four derivation rules are sound, i.e. for every derived claim (F,A,c) holds c=|ModA(F)|. In doing so, we will also provide some intuition on the semantic meaning of the rules.
Lemma 4.2.
The inference rules of MICE′ are sound.
Proof:
To prove the soundness of every MICE′ rule, we associate every claim (F,A,c) with the set ModA(F). With this interpretation, we can specify how every rule modifies these models. This way, we can show that the resulting model count is indeed correct for every MICE′ rule.
The soundness of (Ax) is obvious, since |Mod∅(∅)|=|{∅}|=1.
To show soundness of (Comp’), let (F,A,∑i∈[n]ci) be derived with (Comp’) from correct claims (F,A1,c1),…,(F,An,cn). Then we have
ModA(F)={α∈⟨vars(F)⟩∣α⊧F∪A}=⊎i∈[n]{α∈⟨vars(F)⟩∣α⊧F∪Ai}⊎{α∈⟨vars(F)⟩∣α⊧F∪A∪{A‾i∣i∈[n]}}
where
⊎ denotes the disjoint union. This split of
A into those
Ai is possible since
A⊆Ai (C-2). The sets on the right side of the equation are pairwise disjoint because of (C-1). The last set is empty, otherwise there would not exist an absence of models statement (C-3). Thus,
ModA(F)=⊎i∈[n]ModAi(F).
Using the correctness of all used claims we get
|ModA(F)|=∑i∈[n]|ModAi(F)|=∑i∈[n]ci.
Next, we show soundness of (
Join’). For this, let
(F1∪F2,A1∪A2,c1⋅c2) be derived with (
Join’) from correct claims
(F1,A1,c1) and
(F2,A2,c2). We show that
ModA1∪A2(F1∪F2)={α1∪α2∣α1∈ModA1(F1),α2∈ModA2(F2)}.
We will prove both subset relations separately in the following.
For ⊆, let α∈ModA1∪A2(F1∪F2) be given. Per definition, α satisfies F1∪F2∪A1∪A2 and in particular α|vars(F1)∪vars(A1) has to satisfy F1∪A1. Because of vars(A1)⊆vars(F1), α|vars(F1) has to satisfy F1∪A1 and therefore, α|vars(F1)∈ModA1(F1). Analogously, we get α|vars(F2)∈ModA2(F2). Since α=α|vars(F1)∪α|vars(F2), we can choose α1=α|vars(F1) and α2=α|vars(F2) to see the relation.
For the other direction ⊇, we first have to show that any fixed α1∈ModA1(F1) and α2∈ModA2(F2) are consistent. Because of (J-2) ensuring vars(F1)∩vars(F2)⊆vars(Ai) for both i∈{1,2}, we know that they could only be inconsistent in variables in Ai. With (J-1) which states that A1 and A2 are consistent, we can conclude that α1 and α2 are consistent. We know that αi satisfies Fi∪Ai per construction. As a result, α1∪α2 satisfies F1∪F2∪A1∪A2 and is therefore in ModA1∪A2(F1∪F2).
The model count for the derived claim follows directly with the correctness of both used claims,
|ModA1∪A2(F1∪F2)|=|ModA1(F1)|⋅|ModA2(F2)|=c1⋅c2.
Finally we have to show that (
Ext’) is sound. Assume
(F,A,c) is derived with (
Ext’) from the correct claim
(F1,A1,c1). We show
ModA(F)={α∪(A∖A1)∪β∣α∈ModA1(F1),β∈⟨vars(F)∖(vars(F1)∪vars(A))⟩}.
Similarly to the previous case, we prove both inclusions separately.
For ⊆, let γ∈ModA(F) be given. Per definition, γ satisfies F∪A=F1∪(F∖F1)∪A1∪(A∖A1). This split is possible because of (E-1) and (E-2). We can define α=γ|vars(F1), β=γ|vars(F)∖(vars(F1)∪vars(A)). Then we have γ=α∪(A∖A1)∪β and get the inclusion.
For ⊇, we fix some α∈ModA1(F1), β∈⟨vars(F)∖(vars(F1)∪vars(A))⟩ and define γ=α∪(A∖A1). As α has to contain the assignment according to A1, we have that γ satisfies A. With (E-3) follows that γ satisfies F∖F1. Since A1 is a model of F1, γ satisfies F1 as well. As a result, γ satisfies F∪A and is therefore in ModA(F).
The corresponding model count follows immediately with the correctness of (F1,A1,c1),
|ModA(F)|=|ModA1(F1)|⋅|ModA(F∖F1)|=c1⋅2|vars(F)∖(vars(F1)∪vars(A))|.
As we have shown with the easy semantic arguments above, all rules of
MICE′ are sound. □
Corollary 4.3.
Let claim I=(F,A) and a model α∈ModA(F) be given.
If I is derived with (Comp’) using claims (F,A1),…,(F,An), then there exists exactly one i∈[n] such that α∈ModAi(Fi).
If I is derived with (Join’) using claims (F1,A1) and (F2,A2), then for both i∈[2] we have α|vars(Fi)∈ModAi(Fi).
If I is derived with (Ext’) using claim (F1,A1), then α|vars(F1)∈ModA1(F1).
We introduce an additional rule (SA) which is similar to the construction in Proposition 3.3.
Definition 4.4
Definition 4.4(Satisfying Assumption Rule).
Under the condition (S-1): A satisfies F, we allow to derive
(F,A,2|vars(F)∖vars(A)|)(SA).
This rule is sound and does not make MICE′ proofs much shorter. Therefore, when constructing MICE′ proofs, we sometimes use this additional rule as it makes proofs more intuitive and easier to understand.
Lemma 4.5.
(SA) is sound. Further, if formula φ has a MICE′ proof π that can use the additional rule (SA), then there exists a MICE′ proof π′ of φ with s(π′)=s(π)+1 and c(π′)=c(π)+1.
Proof:
Assume that we applied (SA) in π to derive claim I=(F,A,2|vars(F)∖vars(A)|). Then we can derive I without (SA) with two MICE′ steps in the following way. We use (Ax) to get (∅,∅,1) and then (Ext’) to derive I. It is easy to see that conditions (E-1) and (E-2) are fulfilled. (E-3) follows directly from (S-1). The resulting counts are the same since 1⋅2|vars(F)∖(vars(F1))∪vars(A))|=2|vars(F)∖vars(A)|. Since we can simulate (SA) with the other sound MICE′ rules, (SA) is sound as well. If we replace all applications of (SA) like this, then the proof size increases at most by one, as we need (Ax) only once in the proof. □
To justify our definition of MICE′ we have to show that it is indeed a proof system for #SAT.
Theorem 4.6.
MICE′ is a sound and complete proof system for #SAT.
Proof:
The soundness of MICE′ follows directly from the soundness of the inference rules as shown in Lemma 4.2.
Next, we show that MICE′ is complete. For this, let an arbitrary formula φ be given. We can derive Iα=(φ,α,1) for every α∈Mod(φ) with (SA). For all these models together there is an absence of models statement. Therefore, we can derive (φ,∅,|Mod(φ)|) with (Comp’) from all claims Iα. Note that for unsatisfiable formulas we can derive the final claim with a single application of (Comp’).
In proof systems, it is also necessary that proofs can be verified in polynomial time. This is possible in MICE′ since all conditions (C-1), (C-2), (C-3), (J-1), (J-2), (E-1), (E-2) and (E-3) are easy to check in polynomial time. □
Next, we show some basic properties of MICE′.
Lemma 4.7.
Let claim (F1,A1) be used to derive (F,A) (not necessarily in one step). Then
Proof:
Because every MICE′ rule does not decrease the formula F, the first property is obvious.
Let ((F1,A1),…,(Fn,An)=(F,A)) be a path in this derivation. It is easy to check that for all four inference rules of MICE′ we have Ai+1|vars(Fi)⊆Ai for i∈[n−1]. We can restrict both sides and get
(Ai+1|vars(Fi))|vars(F1)=Ai+1|vars(Fi)∩vars(F1)=Ai+1|vars(F1)⊆Ai|vars(F1).
Therefore,
A|vars(F1)=An|vars(F1)⊆An−1|vars(F1)⊆⋯⊆A1|vars(F1)=A1.
From
A|vars(F1)⊆A1 the second property follows. □
Using these properties, we can show that the new proof system MICE′ is polynomially equivalent to MICE. Note that this result is true for both measures of proof size s(⋅) and c(⋅). To prove this equivalence, we show both simulations separately.
First we show that MICE′ is at least as strong as MICE. This simulation is the more important one for this paper as it implies that lower bounds for MICE′ do also apply for MICE.
Proposition 4.8.
MICE′ p-simulates MICE.
Proof:
Let π=(I1,…,Im) be a MICE proof of a given formula φ. We assume that vars(F)⊆V for all claims ((F,V),A) in π which is justified by Lemma 3.6. We will show that for f(((F,V),A)):=(F,A|vars(F)) the sequence π′=(f(I1),…,f(Im)) is a correct MICE′ proof of φ.
For this we first prove by induction that (f(I1),…,f(Ik)) is a MICE′ proof trace for every k∈{0,…,m}. In the base case k=0 the empty trace is valid. For the induction step we assume we have already derived f(I1),…,f(Ik−1) and in particular f(I) for all claims I we used to derive Ik. We distinguish how Ik is derived.
Exactly One Model. Ik=((F,V),A) is derived with (1-Mod). Then we can derive f(Ik)=(F,A|vars(F)) with (SA) since A satisfies F ((O-2) for Ik) and in particular, A|vars(F) satisfies F.
Composition. Ik=((F,V),A) is derived with (Comp) using absence of models statement ρ and claims Ii1,…,Iir for ij<k with Iij=((F,V),Aij) and f(Iij)=(F,Aij|vars(F)). Note that some f(Iij) might be duplicates. We can derive f(Ik)=(F,A|vars(F)) with (Comp’) of claims f(Iij) after removing all duplicates:
(C-1). Aij|vars(F) assign the same variables, since Aij assign the same variables ((C-1) for Ik). The new assumptions are pairwise inconsistent as we removed all duplicates.
(C-2). A|vars(F)⊆Aij|vars(F) follows from A⊆Aij ((C-2) for Ik).
(C-3). There is an absence of models statement ρ ((C-3) for Ik) which is a refutation of
A∪F∪{A‾ij∣j∈[r]}
where we used our assumption vars(F)⊆V. ρ can be adapted to a refutation of
A|vars(F)∪F∪{A‾ij|vars(F)∣j∈[r]},
since we can just remove the variables that are not in vars(F) from every clause in ρ and get a valid resolution proof where some resolutions might get weakening steps.
Join. Ik=((Fi∪Fj,Vi∪Vj),Ai∪Aj) is derived with (Join) using claims Ii and Ij, with i,j<k. For r∈{i,j} let Ir=((Fr,Vr),Ar) and f(Ir)=(Fr,Ar|vars(Fr)). We can apply (Join’) to f(Ii) and f(Ij):
(J-1). Ai|vars(Fi) and Aj|vars(Fj) are consistent since Ai and Aj are consistent ((J-1) for Ik).
(J-2). From requirement vars(F)⊆V for every claim follows vars(Fi)∩vars(Fj)⊆Vi∩Vj. Furthermore, for r∈{i,j} is Vi∩Vj⊆vars(Ar) ((J-2) for Ik). Thus, also vars(Fi)∩vars(Fj)⊆vars(Ar|vars(Fr)).
The resulting claim is
(Fi∪Fj,Ai|vars(Fi)∪Aj|vars(Fj)). We will show that
Ai|vars(Fi)∪Aj|vars(Fj)=Ai|vars(Fi)∪vars(Fj)∪Aj|vars(Fi)∪vars(Fj).
The direction ⊆ follows directly. For the other direction ⊇ we assume that
x is in the right set and show that
x is in the left set as well. W.l.o.g. let
x∈Ai|vars(Fi)∪vars(Fj). If
x∈vars(Fi), then
x∈Ai|vars(Fi). So assume
x∉vars(Fi), then is
x∈vars(Fj). Our requirement
vars(Fj)⊆Vj implies
x∈Vj. Per definition of a claim,
vars(Ai)⊆Vi and therefore,
x∈Vi. Using (J-2) we get
x∈Vi∩Vj⊆vars(Aj). Since
Ai and
Aj are consistent ((J-1) for
Ik), we have
x∈Aj|vars(Fj).
Therefore, the (Join’) application results in the claim
(Fi∪Fj,Ai|vars(Fi)∪vars(Fj)∪Aj|vars(Fi)∪vars(Fj))=(Fi∪Fj,(Ai∪Aj)|vars(Fi)∪vars(Fj))=f(Ik).
Extension. Ik=((F,V),A) is derived with (Ext) from claim Ij=((Fj,Vj),Aj) with j<k and f(Ij)=(Fj,Aj|vars(Fj)). We can derive f(Ik)=(F,A|vars(F)) with (Ext’) of f(Ij):
(E-1). Fj⊆F follows from (E-1) for Ik.
(E-2). (A|vars(F))|vars(Fj)=A|vars(F)∩vars(Fj)=A|vars(Fj) since Fj⊆F. Using vars(Fj)⊆Vj this is equal to A|Vj∩vars(Fj) which we can transform to (A|Vj)|vars(Fj). Finally we can use A|Vj=Aj ((E-3) for Ik) and get (Aj)|vars(Fj).
(E-3). A|vars(F) satisfies F∖Fj since A satisfies F∖Fj ((E-4) for Ik).
This completes the induction. Therefore, π′ is a valid MICE′ trace. Since the final claim is f(Im)=f(((φ,vars(φ)),∅))=(φ,∅) we have that π′ is a MICE′ proof of φ. Per construction, c(π′)⩽c(π)+1 and s(π′)⩽s(π)+1. The additional 1 is needed in order to use the (SA) rule to simulate (1-Mod). Apart from that, the number of claims and the number of clauses in the resolution refutations do not increase. □
Next we show that MICE′ is not stronger than MICE. Although this result is not needed for the lower bounds, it is nice to know how our new proof system MICE′ relates to MICE exactly.
Proposition 4.9.
MICE p-simulates MICE′.
Proof:
Let π=(I1,…,In) with Ii=(Fi,Ai) be a MICE′ proof of a given formula φ. We define Ii′=((Fi,vars(Fi)),Ai) and show that we can derive Ik′ using I1′,…Ik−1′ with O(|vars(φ)|) MICE steps. We distinguish how Ik is derived.
Axiom. Ik=(∅,∅) is derived with (Ax). Then we can derive Ik′=((∅,∅),∅) with (1-Mod).
(O-1) and (O-2) are fulfilled since vars(∅)=∅ and the empty assignment satisfies ∅.
Composition. Ik=(Fk,Ak) is derived with (Comp’) using absence of models statement ρ and claims Ii1,…,Iir with Iij=(Fk,Aij) for ij<k. Then we can derive Ik′ with (Comp’) from Ii1′,…,Iir′.
(C-1) and (C-2) follow directly from (C-1) and (C-2) for Ik as we do not modify the assumptions. For (C-3) we can simply use the absence of models statement ρ since it refutes
(Ak)|vars(Fk)∪Fk∪{A‾ij|vars(Fk)∣j∈[r]}=Ak∪Fk∪{A‾ij∣j∈[r]}.
Join. Ik=(Fi∪Fj,Ai∪Aj) is derived with (Join’) applied to Ii=(Fi,Ai) and Ij=(Fj,Aj) with i,j<k. Then we can derive Ik′ with (Join’) using Ii′ and Ij′.
(J-1) follows directly from (J-1) for Ik, as we do not modify the assumptions. (J-2) stating vars(F1)∩vars(F2)⊆vars(Ak) follows from (J-2) for Ik.
Extension. Ik=(Fk,Ak) is derived with (Ext’) from Ii=(Fi,Ai) with i<k.
We derive
I=((∅,vars(Fk)∖(vars(Fi)∪vars(Ak))),∅)
with the construction of Proposition
3.3. We can apply (
Join) to
I and
Ii′.
(J-1). The empty assumption ∅ and Ai are consistent.
(J-2). (vars(Fk)∖(vars(Fi)∪vars(Ak)))∩vars(Fi)=∅⊆vars(Aj).
(J-3). This follows from Corollary 3.7.
With this (
Join’) we receive
I′=((Fi,vars(Fi)∪vars(Fk)∖(vars(Fi)∪vars(Ak))),Ai)=((Fi,vars(Fi)∪vars(Fk)∖vars(Ak)),Ai).
Next, we can apply (
Ext) to get
((Fk,vars(Fk)),Ak)=Ik′.
(E-1). Fi⊆Fk follows from (E-1) for Ik. Therefore, we also have vars(Fi)∪vars(Fk)∖vars(Ak)⊆vars(Fk).
(E-2). We apply some basic set operations to get vars(Fk)∖(vars(Fi)∪(vars(Fk)∖vars(Ak)))⊆vars(Fk)∖(vars(Fk)∖vars(Ak))⊆vars(Fk)∩vars(Ak)=vars(Ak). For the last equation we used that (Fk,Ak) is a MICE′ claim and therefore vars(Ak)⊆vars(Fk).
(E-3). We have that Ak|vars(Fi)∪vars(Fk)∖vars(Ak)=Ak|vars(Fi) is equal to Ai because of (E-2) for Ik.
(E-4). Ak satisfies Fk∖Fi follows from (E-3) for Ik.
(E-5). This follows from Corollary 3.7.
As a result, we can derive Ik′ from I1′,…Ik−1′ with a single MICE step if Ik is derived with (Ax), (Comp’) or (Join’). In particular, the resolution proof size of the absence of models statement in case of (Comp’) does not change. If Ik′ is derived with (Ext’), we need one application of the construction of Proposition 3.3, one (Join) and one (Ext) and therefore in total O(|vars(φ)|) MICE steps.
Since In′=((φ,vars(φ)),∅), there is a MICE proof π′ of φ that has sizes s(π′)=s(π)⋅O(vars(φ)) and c(π′)=c(π)⋅O(vars(φ)). □
5.Lower Bounds for MICE and MICE’
In this section we investigate the proof complexity of MICE′. Because of the equivalence of MICE and MICE′ (Proposition 4.8 and Proposition 4.9), all of the proof complexity results for MICE′ below also apply to MICE. For the analysis we use the two different measures of proof size.
First, we consider the proof size s(⋅). For that, we can easily lift known lower bounds from propositional resolution and get families of formulas that require MICE′ proofs of exponential size.
However, one could argue, that this is not the kind of hardness we are interested in. In the second part we get a stronger result by showing a lower bound for the number of inference steps c(⋅), i.e. we ignore the sizes of the absence of models statements.
5.1.Lower Bounds for the Proof Size
In this subsection we only consider the proof size s(⋅) that counts the number of claims plus the length of all resolution refutations. If we use MICE′ on unsatisfiable formulas, we have to prove that the formula has zero models. Hence, we can use MICE′ as proof system for the language UNSAT as well. We show that MICE′ is precisely as strong as resolution for unsatisfiable formulas.
Theorem 5.1.
MICE′ is polynomially equivalent to Res for unsatisfiable formulas.
Proof:
Let φ be an arbitrary unsatisfiable formula.
We first show that Res is simulated by MICE′. Suppose πRes is a resolution refutation of φ, then we can use πRes as an absence of models statement and derive the final claim (φ,∅,0) with a single application of (Comp’) of zero claims.
Next, we show that MICE′ is simulated by Res. Let a MICE′ refutation π=(I1,…,Im) for φ be given with Ii=(Fi,Ai,ci). We define πRes=(φ,X1,X2,…,Xm) with
Xi=∅if ci≠0{A‾i}if Ii is derived by (Join’) or (Ext’){C∪A‾i∣C∈ρ}if Ii is derived by (Comp’) and absence of modelsstatement ρ.
We show that
πRes is a valid resolution trace (with weakening steps). For this we use induction on
m. In the base case for
m=0 the trace only contains the clauses of φ and is therefore valid. For the induction step let
(φ,X1,…,Xk−1) be a valid resolution trace. If
ck≠0, there is nothing to show. Therefore, we can assume that
ck=0. In particular,
Ik is not derived with (
Ax). We distinguish how
Ik is derived.
Ik is derived with (Comp’) from claims Ii1,…,Iir with ij<k using the absence of models statement ρ which is a resolution derivation
Fk∪Ak∪{A‾ij∣j∈[r]}⊢□.
In this derivation we can weaken every clause by A‾k. Thus Xk is a resolution derivation of
Fk∪{A‾ij∣j∈[r]}⊢A‾k.
All clauses of Fk⊆φ (Observation 3.4) are already in πRes. All clauses A‾ij are in πRes as well by induction hypothesis, since cij=0 for all used claims Ii1,…,Iir to get the sum ck=0. Thus, the resolution derivation is correct.Ik is derived by (Join’) from claims Ii and Ij with i,j<k. Since ck=0=ci⋅cj, w.l.o.g. ci=0. Therefore, we have already derived A‾i by induction hypothesis. Thus A‾k=Ai∪Aj‾=(A‾i∨A‾j) can be derived with a single weakening step.
Ik is derived by (Ext’) from Ii with i<k. Since ck=ci⋅2|vars(Fk)∖(vars(Fi)∪vars(Ak))|=0 we have ci=0. Thus A‾i has already been derived. We can derive A‾k from A‾i by weakening since Ai⊆Ak (E-3).
Since
cm=0, the last claim
Im is derived with (
Comp’), (
Join’) or (
Ext’). Thus,
Xm contains the clause
A‾m=□. As a result,
πRes is a resolution refutation of φ since it is a valid derivation of □. Furthermore, we see that
|πRes|=O(s(π)). It is known that any refutation with resolution and weakening can be transformed into a refutation without weakening efficiently which proves the claim. □
Many hard families of formulas for resolution are known. One famous example is the pigeonhole formula family PHP for which an exponential lower bound for resolution was first shown in [27]. With Theorem 5.1 we can conclude that these hard formulas for resolution are also hard for MICE′.
Corollary 5.2.
Any MICE′ proof π of PHPn has size s(π)=2Ω(n).
We note that it is also quite straightforward to obtain exponential proof size lower bounds for satisfiable formulas in MICE′ by forcing the system to refute some exponentially hard CNFs in absence of models statements.
5.2.Lower Bounds for the Number of Inference Steps
One could argue that unsatisfiable formulas such as PHP are not particularly interesting for model counting. We also note that they have very simple MICE′ proofs of just one step (as in the simulation of resolution by MICE′ in Theorem 5.1) and that their hardness for MICE′ stems solely from the fact that they are hard for resolution (and such resolution proofs need to be included as an absence of models statement). However, we would argue that this does not tell us much on the complexity of MICE′ proofs.
We therefore now tighten our complexity measure and consider the proof size measure c(⋅) that only counts the number of MICE′ inference steps which is exactly the number of claims a proof π has. This measure disregards the size of the accompanying resolution refutations and hence formulas such as PHP become easy.
In our main result we present a family of formulas that is exponentially hard with respect to this sharper measure of counting inference steps. Such hard formulas need to have many models as the following upper bound shows.
Observation 5.3.
Every formula φ has a MICE′ proof π with c(π)=|Mod(φ)|+2.
Proof:
The MICE′ proof that we used to show the completeness in Theorem 4.6 needs one (Ax) step, |Mod(φ)| applications of (Ext’), and one application of (Comp’). □
Therefore, to show exponential lower bounds to the number of steps we will need formulas with 2Ω(n) models. Next, we show that MICE′ proofs for such formulas do not require claims with c=0. In particular, we can assume that there are no such claims in the proofs.
Lemma 5.4.
Let φ∈SAT and π be a MICE′ proof of φ. Then there is a MICE′ proof π′ of φ that has no claim with count c=0 such that s(π′)=O(s(π)2) and c(π′)⩽c(π).
Proof:
Assume that in π some claim I=(F,A) is derived with (Comp’) from claims I1,…,In with Ii=(F,Ai,ci) and cn=0 using some absence of models statement ρ. Because of Theorem 5.1 we can construct a resolution refutation ρn of F∪An that has size O(|π|). Therefore, we can derive I with (Comp’) from I1,…,In−1 as well: (C-1) and (C-2) are still satisfied. For (C-3) we need an absence of models statement that refutes F∪A∪{A‾i∣i∈[n−1]}. For this we can first derive A‾n from F with ρn and then apply ρ. Like this, we can remove claim In. We repeat this for every claim with c=0 that is used for (Comp’). Afterwards, we remove all claims that became redundant. Let π′ be the resulting proof.
Per construction, π′ is a valid MICE′ proof for φ. We will show that π′ has no claims with c=0. Assume otherwise claim I with c=0 is in π′. Since I is not redundant, there is a path to the final claim with c>0. In this path there have to be claims I1 with c1=0 and I2 with c2>0 such that I2 is directly derived from I1 with one of the four MICE′ rules.
Obviously this is not possible with (Ax).
Per construction, it is impossible with (Comp’), because otherwise I1 would not be in π′.
It is not possible with (Join’) nor (Ext’) as c2 would be a product with one factor c1=0 leading to c2=0.
Hence,
π′ has no claim with
c=0. Furthermore,
c(π′)⩽c(π) since we only removed claims. For every claim with
c=0 that was used for (
Comp’), we have to add a resolution proof of size
O(s(π)) leading to
s(π′)=O(s(π)2). □
Next, we introduce the family of formulas (XOR-PAIRSn)n∈N. They consist of variables xi and zij for i,j∈[n] and are satisfied exactly if (zij=xi⊕xj) for every pair i,j∈[n].
Definition 5.5.
The formula XOR-PAIRSn consists of the clauses
Cij1=(xi∨xj∨z‾ij),Cij2=(x‾i∨xj∨zij),Cij3=(xi∨x‾j∨zij),Cij4=(x‾i∨x‾j∨z‾ij)
for
i,j∈[n].
Theorem 5.6.
Any MICE′ proof π of XOR-PAIRSn requires size c(π)=2Ω(n).
We start with some observations and lemmas and prove the lower bound at the end of this section.
The idea of the proof is the following: The final claim has a large count. In order to get a large count with a small number of MICE′ steps, we have to use (Ext’) or (Join’) such that the previous counts get multiplied. However, we show that one factor of any such multiplication is always 1. As a result, the only way to increase the count is with (Comp’). We start with applications of (Ax) with count 1 and can only sum up those counts with (Comp’). As a result, we need an exponential number of summands.
Observation 5.7.
XOR-PAIRSn has 2n models.
Proof:
We can set xi arbitrarily for all i∈[n] and have a unique assignment for the remaining z variables to satisfy XOR-PAIRSn. □
For the following arguments we will only consider MICE′ proofs of XOR-PAIRSn without redundant claims (i.e. all claims are connected to the final claim) and without claims with c=0 (this is possible by Lemma 5.4). Our next lemma states that if we have some clause Cij in a claim, then all missing clauses Cij have to be satisfied by the assumption.
Lemma 5.8.
Let (F,A) be an arbitrary claim in a MICE′ proof of XOR-PAIRSn. If there are i,j∈[n] such that {xi,xj,zij}⊆vars(F), then A has to satisfy every clause Cijk for k∈[4] that is not in F.
Proof:
We fix variables i,j∈[n] such that {xi,xj,zij}⊆vars(F) and a clause C=Cijk∉F for some k∈[4]. We consider only the path from (F,A) to (XOR-PAIRSn,∅) which has to exist, because otherwise (F,A) is redundant. There have to be claims I1=(F1,A1) and I2=(F2,A2) directly adjacent in this path with F⊆F1⊆F2⊆φ, C∉F1, C∈F2, i.e. I1 is the last claim in the path that does not contain C. I2 is directly derived from I1 with one of the four MICE′ steps.
I2 is obviously not derived with (Ax) nor (Comp’), since F1≠F2.
Assume I2 is derived with (Join’) of I1 and some I3=(F3,A3). Since C∉F1 and C∈F2=F1∪F3 is C∈F3. In particular {xi,xj,zij}⊆vars(F3). Together with {xi,xj,zij}⊆vars(F)⊆vars(F1) we get {xi,xj,zij}⊆vars(F1)∩vars(F3)⊆vars(A1) and {xi,xj,zij}⊆vars(A3) where we used (J-2). Since A1 and A3 are consistent (J-1), xi, xj, zij have to be assigned in the same way in A1 and A3. Because of Lemma 4.7 those variables have to be set in A as well and in particular with the same polarities.
Assume A does not satisfy C. Then, A3 does not satisfy C either, since all variables of C are set as in A. Hence, (F3,A3) has no models leading to c3=0 which contradicts our assumption that there are no claims with count zero for satisfiable formulas (Lemma 5.4). Therefore, A has to satisfy C.
Assume, I2 is derived with (Ext’) from I1. Then A2 has to satisfy C∈F2∖F1 by condition (E-3). Because of Lemma 4.7, A has to assign xi, xj, zij in the same way as A2. Hence A satisfies C as well.
Therefore,
I2 can only be derived if
A satisfies
C leading to the lemma. □
The following lemma is similar in spirit. It shows that if all clauses Cij are missing in a claim, then xi and xj have to be set in the assumption.
Lemma 5.9.
Let a MICE′ proof of XOR-PAIRSn be given and let (F,A) be an arbitrary claim in the proof. If there are i,j∈[n] such that {xi,xj}⊆vars(F) and zij∉vars(F), then {xi,xj}⊆vars(A).
Proof:
We fix indices i,j∈[n] such that {xi,xj}⊆vars(F) and zij∉vars(F). Since zij∉vars(F) we have Cijk∉F for all k∈[4]. We consider only the path from (F,A) to (XOR-PAIRSn,∅) which has to exist, because otherwise (F,A) is redundant. There have to be claims I1=(F1,A1) and I2=(F2,A2) directly adjacent in this path with Cijk∉F1 for all k∈[4] and Cijs∈F2 for at least one s∈[4]. That means, I1 is the last claim in this path which contains none of the four clauses Cij. Towards a contradiction, let us assume xi∉vars(A) (the argument for xj is analogous). By Lemma 4.7, also xi∉vars(A1) and xi∉vars(A2). The claim I2 is directly derived from I1 by one of the four MICE′ rules.
I2 is not derived with (Ax) nor (Comp’), since F1≠F2.
I2 is not derived with (Join’). Assume otherwise, then I2 is the result of (Join’) of I1 with some other claim I3=(F3,A3). Since Cijs∉F1 and Cijs∈F2=F1∪F3 we have Cijs∈F3 and in particular xi∈vars(F3). Together with xi∈vars(F)⊆vars(F1) we get a contradiction with (J-2) because xi∈vars(F1)∩vars(F3)⊆vars(A1), but xi∉vars(A1).
I2 is not derived with (Ext’) from I1. Otherwise, A2 has to satisfy F2∖F1 by condition (E-3). Since F1 does not contain any clause Cij, A2 has to satisfy all clauses Cij that are in F2. By Lemma 5.8, A2 has to satisfy all clauses Cij that are not in F2 as well. In order to satisfy all four clauses of Cij, all three variables xi, xj and zij have to be set in A2, in particular xi∈vars(A2) which is a contradiction.
As a result,
I2 cannot be derived from
I1 which implies that our assumption
xi∉vars(A) was false. □
Using the previous two lemmas, we show that the two inference rules that multiply counts, i.e. (Join’) and (Ext’), do not affect the count at all for the XOR-PAIRS formulas.
Lemma 5.10.
Let a MICE′ proof of XOR-PAIRSn be given. If the proof contains a (Join’) of two claims (F1,A1,c1) and (F2,A2,c2), then min(c1,c2)=1.
Proof:
Suppose otherwise, c1⩾2 and c2⩾2.
Assume that all x variables occurring in vars(F1) are assigned in A1. Since c1⩾2, vars(F1)∖vars(A1)≠∅. In particular, there has to be a zij∈vars(F1)∖vars(A1) such that there is at least one model of F1 and A1 with zij=0 and one with zij=1. Then we have {xi,xj}⊆vars(F1) and {xi,xj}⊆vars(A1). As a result, A1 has to satisfy all clauses Cijk that are in F1. Because of Lemma 5.8, A1 has to satisfy the clauses Cijk that are not in F1 as well. Thus, A1 has to satisfy all four clauses Cijk, which is only possible if zij∈vars(A1). This contradicts the choice of zij. Similarly, we also see that there is at least one x variable in vars(F2)∖vars(A2).
Hence, we can fix xi∈vars(F1)∖vars(A1) and xj∈vars(F2)∖vars(A2). Condition (J-2) implies xi∉vars(F2), xj∉vars(F1) and in particular i≠j. Because of vars(A1)⊆vars(F1) and xj∉vars(F1) we get xj∉vars(A1) and therefore also xj∉vars(A1∪A2). The joined claim is (F,A)=(F1∪F2,A1∪A2) with {xi,xj}⊆vars(F) and Cijk∉F for all k, implying zij∉vars(F). With Lemma 5.9 we get the contradiction xj∈vars(A)=vars(A1∪A2).
Therefore, our assumption c1⩾2 and c2⩾2 was false. □
Using this lemma we can show, that w.l.o.g. any MICE′ proof of XOR-PAIRSn does not use (Join’).
Lemma 5.11.
Let π be a MICE′ proof of XOR-PAIRSn. Then there is a MICE′ proof π′ that does not use (Join’) with c(π′)⩽2⋅c(π).
Proof:
Using π we construct a MICE′ proof π′ that does not use (Join’).
For this suppose that in π, the claim I=(F1∪F2,A1∪A2) is derived with (Join’) of (F1,A1,c1) and (F2,A2,c2). Because of Lemma 5.10 we can assume that c2=1. Thus, there is a unique assignment α such that vars(A2)∩vars(α)=∅, vars(A2∪α)=vars(F2) and A2∪α satisfies F2. Then, we can apply (Ext’) to (F1,A1) resulting in (F1∪F2,A1∪A2∪α). We check the conditions to apply (Ext’).
(E-1). F1⊆F1∪F2 holds.
(E-2). We see that (A1∪A2∪α)|vars(F1)=A1|vars(F1)∪A2|vars(F1)∪α|vars(F1)=A1. In the last equation we used three facts:
A1|vars(F1)=A1 is a direct consequence of vars(A1)⊆vars(F1).
A2|vars(F1)⊆A1 follows from vars(A2|vars(F1))⊆vars(F2)∩vars(F1)⊆vars(A1) by (J-2) and the fact that A1 and A2 are consistent by (J-1).
α|vars(F1)=∅. Assume otherwise that x∈vars(α)∩vars(F1). Then x∈vars(α)∩vars(F1)⊆vars(F2)∩vars(F1)⊆vars(A2) by (J-2). Thus, x∈vars(A2)∩vars(α) contradicting the construction of α.
(E-3). A1∪A2∪α satisfies (F1∪F2)∖F1⊆F2 as A2∪α satisfies F2 by construction.
Applying (Comp’) on the claim (F1∪F2,A1∪A2∪α) we get (F1∪F2,A1∪A2). In this way we can remove every (Join’) application with one application of each (Ext’) and (Comp’). Let π′ be the resulting MICE′ proof of XOR-PAIRSn that does not use (Join’). The number of claims in the proof increases at most by a factor of two. □
Lemma 5.12.
Let a MICE′ proof of XOR-PAIRSn be given. Any claim (F,A,c) in the proof that is derived with (Ext’) from (F1,A1,c1) satisfies c=c1.
Proof:
Suppose c≠c1. Since c=c1⋅2|vars(F)∖(vars(F1)∪vars(A))| there is a variable v∈vars(F) with v∉vars(F1)∪vars(A). Variable v occurs in some clause Cijk∈F∖F1. Therefore, {xi,xj,zij}⊆vars(F). A has to satisfy all clauses of Cij that occur in F∖F1 because of (E-3). Furthermore, A has to satisfy all clauses of Cij that do not occur in F as well due to Lemma 5.8. Since, v∉vars(F1), there is no Cij∈F1. Therefore, A has to satisfy all four clauses Cij. For this, xi, xj and zij have to be set in A. Since v occurs in Cij, we have v∈vars(A) which contradicts the choice of v. □
Now we have all ingredients to finally prove that the XOR-PAIRS formulas require proofs with an exponential number of MICE′ steps.
Proof of Theorem 5.6:
Note that with Observation 5.7, Lemma 5.10 and Lemma 5.12 we can infer immediately that any tree-like MICE′ proof of XOR-PAIRSn, i.e. any proof that uses every claim except the axiom at most one time, has at least size 2n+2. However, in general (dag-like) MICE′ proofs, any claim can be used multiple times. General dag-like MICE′ might be exponentially stronger than the tree-like version. Therefore, the lower bound is not shown yet.
To prove the lower bound in the general case, let π be an arbitrary MICE′ proof of XOR-PAIRSn. Let π′ be a MICE′ proof of XOR-PAIRSn that does not use (Join’) with c(π′)⩽2⋅c(π) which has to exist because of Lemma 5.11.
We consider an arbitrary fixed path κ in π′ from the axiom to the final claim. Since π′ does not use (Join’), we can only enlarge the formula with (Ext’). Because of Lemma 5.12, we have to assign all newly introduced variables when we use (Ext’), i.e. every variable is in at least one assumption in κ. The only rule that can remove variables from the assumption is (Comp’).
Since the final claim has the empty assumption, we have to remove all variables from the assumption in κ. Therefore, in κ there has to be at least one application of (Comp’) where we remove a variable xi from the assumption for some i∈[n]. Let I1κ=(F1κ,A1κ) be the claim that was used for the first such (Comp’) in κ to derive I2κ=(F2κ,A2κ).
Let X be the set of all x variables: X:={x1,…,xn}. We show
X⊆vars(F1κ).
Let
xi be a variable that is removed from the assumption by applying (
Comp’) to
I1κ, i.e.
xi∉vars(A2κ). Suppose, there is a
j∈[n] such that
xj∉vars(F1κ) and in particular
Cijs∉F1κ for all
s∈[4], implying
zij∉vars(F1κ). Let
Irκ=(Frκ,Arκ) be the first claim in κ with
zij∈vars(Frκ) and therefore
{xi,xj,zij}⊆vars(Frκ).
Irκ has to be derived with (
Ext’). Because of condition (E-3),
Arκ has to satisfy all clauses
Cijs in
Frκ. Furthermore,
Arκ has to satisfy all clauses
Cijs that are not in
Frκ because of Lemma
5.8. Hence,
Arκ has to satisfy
Cijs for all
s∈[4]. To do so, we have to assign all three variables
xi,
xj and
zij in
Arκ. In particular, we have
xi∈vars(Arκ). Since
xi∉vars(A2κ), Lemma
4.7 states
xi∉vars(Arκ). With this contradiction we see that such an
xj with
xj∉vars(F1κ) cannot exist.
Since X⊆vars(F1κ), all variables in X were introduced and assigned in the assumption with (Ext’) in I1κ or previously in κ. Per construction there are no other (Comp’) applications before I1κ in κ that remove variables in X. Therefore, we have
X⊆vars(A1κ).
We show that for every α∈Mod(XOR-PAIRSn) there is a path κ in π′ with α|X=A1κ|X. Assume that for some fixed model α there is no such path. Since π′ does not use (Join’) and α∈Mod∅(XOR-PAIRSn), Corollary 4.3 implies that there is a path κ from axiom to the final claim, such that every claim (F,A) in κ fulfills α|vars(F)∈ModA(F). In particular,
α|vars(F1κ)∈ModA1κ(F1κ).
If we restrict both sides on the variables in
X and use
X⊆vars(F1κ), we get
α|X∈{β|X∣β∈ModA1κ(F1κ)}.
Since
X⊆vars(A1κ), all models
β∈ModA1κ(F1κ) have
β|X=(A1κ)|X. Therefore, the right set has only one element which is
(A1κ)|X, leading to
α|X=(A1κ)|X. Hence, κ is a path with the claimed property for α.
Since XOR-PAIRSn has 2n models, there are (at least) 2n paths in π′ and in particular 2n claims I1κ. Because every model of XOR-PAIRSn assigns the x variables differently, all these claims I1κ are pairwise different. Therefore, π′ has at least 2n claims.
Finally, we see that the arbitrarily chosen MICE′ proof π has size c(π)⩾12⋅c(π′)⩾2n−1 leading to the lower bound. □
6.Connection Between MICE’ and Decision DNNFs
In this section we show that there is a tight connection between MICE′ proofs and decision DNNFs. That is, we show in Section 6.1. that we can extract a decision DNNF for some formula φ efficiently from a MICE′ proof of φ. By exploiting this connection we immediately get further lower bounds for MICE′. Finally, in Section 6.2. we use this connection in order to provide an alternative proof that XOR-PAIRS requires MICE′ proofs of exponential size.
Let us first review the concept of DNNFs (Decomposable Negation Normal Form) and focus on the special case of decision DNNFs [21] which are widely used in knowledge compilation. Formally, a decision DNNF D with variables V is a directed acyclic graph with the following conditions. It has exactly one node with in-degree 0 which is called source. The nodes with outdegree 0 are labelled with 0 or 1 and are called sinks. All other nodes have out-degree 2 and are either decision nodes or And nodes. A decision node is labelled with a variable x∈V. One outgoing edge is labelled with 0 and the other with 1. On any path in D the variable x can be decided at most once. An And node is labelled with ∧ and has to satisfy the decomposability property. That is, the sets of variables that occur in the subcircuits of the two children have to be disjoint.
Let N be any node in D, then DN denotes the subcircuit of D with root N. Under a given assignment α∈⟨V⟩, D evaluates to D(α) which is defined recursively as follows.
Let N be a sink of D with label 0, then DN(α)=0. If its label is 1, then DN(α)=1.
Let N be a decision node deciding variable x∈V and let N0 be the child node for x=0, N1 for x=1. Then,
DN(α)=DN0(α),if x is assigned to false in αDN1(α),if x is assigned to true in α.
Let N be an And node with children N0 and N1. Then, DN(α)=DN0(α)∧DN1(α).
A decision DNNF represents some formula φ if
D evaluates to 1 for exactly the models of φ. The size of a decision DNNF is the number of its nodes.
6.1.Efficient Extraction of a Decision DNNF from a MICE’ Proof
We will show, that we can extract decision DNNFs from MICE′ proofs efficiently, i.e. the size of the resulting decision DNNF is not much larger than the number of MICE′ steps.
Theorem 6.1.
Let φ be a formula with MICE′ proof π with n steps. Then there exists a decision DNNF of size at most n⋅(1+|vars(φ)|)+1 representing φ.
Proof:
Let π=I1,…,In be a MICE′ proof with Ik=(Fk,Ak) for every k∈[n]. Our goal is to construct from π a decision DNNF for φ. W.l.o.g. the first claim of π is (∅,∅,1) derived with (Ax) and all other claims are not derived with (Ax). We use the notation Modφ(F):={α∈⟨vars(φ)⟩∣α⊧F}. Inductively, we construct a decision DNNF Ck for every k∈[n] such that:
For the base case k=1, I1=(∅,∅,1) is derived with (Ax). Therefore, we set C1 to a circuit that only contains one sink labelled with 1.
For the induction step we distinguish how Ik is derived.
Join. Ik is derived with (Join) of claims Ii and Ij. Per induction hypothesis, we have already derived decision DNNFs Ci and Cj representing Modφ(Fi[Ai]) and Modφ(Fj[Aj]). We define Ck to be an And gate with the two children Ci and Cj. Because of (J-2) we have vars(Fi)∩vars(Fj)⊆vars(Ai)∩vars(Aj). Together with (IH2) we get vars(Ci)∩vars(Cj)⊆vars(Fi[Ai])∩vars(Fj[Aj])=∅. Therefore, the And is indeed decomposable. Furthermore, (IH1) and (IH2) are satisfied:
Modφ(Fk[Ak])=Modφ((Fi∪Fj)[Ai∪Aj])=Modφ(Fi[Ai∪Aj]∪Fj[Ai∪Aj])=Modφ(Fi[Ai]∪Fj[Aj])=Modφ(Fi[Ai])∩Modφ(Fj[Aj])
and
vars(Ck)=vars(Ci)∪vars(Cj)⊆vars(Fi[Ai])∪vars(Fj[Aj])⊆vars((Fi∪Fj)[Ai∪Aj])=vars(Fk[Ak])
where we used that
Ai,
Aj are consistent (J-1). Further, in the third step, we use that if there is some variable
v∈vars(Fi)∩vars(Aj), then also
v∈vars(Fi)∩vars(Fj)⊆vars(Ai) (J-2).
Composition. Ik is derived with (Comp) from claims Ii1,…,Iir. If r=0, then Ck only contains one node labelled with 0 and the induction hypothesis is fulfilled. Otherwise, let V=vars(Ai1)∖vars(Ak). (Remember, that all assumptions Aij have the same set of variables because of (C-1)). We build a complete binary decision tree T with variables in V. For every claim Iij for j∈[r] there is exactly one leaf in T that is consistent with the assumption of Iij. We replace this leaf with the corresponding decision DNNF Cij. Afterwards, we replace all remaining leaves with the 0 sink. Furthermore, we remove every decision gate where both decisions lead to the 0 sink node as long as such nodes exist. We set Ck to be the resulting circuit. Note, that Ck has at most n paths from the root to some claim and every such path has at most |vars(φ)| decision nodes.
Per construction, Ck contains exactly the models of Fk[Ak] and Ck contains only variables from Fk[Ak].
Extension. Ik is derived with (Ext) from Ii. Then we can set Ck=Ci. To see this, we use that Ak satisfies Fk∖Fi by (E-3) and Ak|vars(Fi)=Ai by (E-2):
Fk[Ak]=Fi[Ak]=Fi[Ak|vars(Fi)]=Fi[Ai].
Therefore,
Modφ(Fk[Ak])=Modφ(Fi[Ai]).
This completes the induction. Since In=(φ,∅), Cn computes Modφ(φ). Thus, Cn represents φ and is a decision DNNF by construction.
To estimate the size, we observe that every claim becomes a node in Cn. Further, there are at most |vars(φ)|⋅n additional decision nodes for the (Comp’) constructions. We may also need one additional sink labelled with 0. In total, we get |Cn|⩽n⋅(1+|vars(φ)|)+1. □
As a direct consequence of Theorem 6.1, lower bounds for decision DNNFs also apply for MICE′.
Corollary 6.2.
If formula φ requires a decision DNNF of size d, then any MICE′ proof for φ has size at least (d−1)⋅(|vars(φ)|+1)−1.
However, the resulting lower bounds are only of interest if the formulas admit short CNF representations. Therefore, in order to obtain relevant lower bounds for MICE′, we need formulas that separate CNF from decision DNNFs. In fact, a few such formulas are known in the literature [4,5,11,12], which by Corollary 6.2 yield additional MICE′ lower bounds.
6.2.An Alternative Proof of the Lower Bound
Here, we provide an alternative proof to our direct MICE′ lower bound for XOR-PAIRS (Theorem 5.6). By Corollary 6.2, to show the lower bound it suffices to show that XOR-PAIRS require decision DNNFs of exponential size. In fact, we show the even stronger result, that all DNNFs for XOR-PAIRS have exponential size.
For the DNNF size lower bound we use a technique from communication complexity similar to [12]. To do so, we have to introduce some notions from communication complexity. Let V be a set of variables. A (combinatorial) rectangle over V is a set R⊆⟨V⟩ such that there exists a partition V=V1⊎V2 and two sets of assignments r1⊆⟨V1⟩, r2⊆⟨V2⟩ satisfying R={α1∪α2∣α1∈r1,α2∈r2}. A rectangle is called balanced if its underlying partition is balanced, i.e. |V|3⩽|V1|⩽2⋅|V|3. A finite set of balanced rectangles {Ri} over variables vars(φ) is called rectangle cover of φ if ⋃iRi=Modφ.
The following result provides a powerful technique to prove lower bounds for DNNF size (and thus also for MICE′ proof size).
Theorem 6.3
Theorem 6.3([12]).
Let C be a DNNF computing a function φ. Then, φ has a balanced rectangle cover of size at most |C|.
Therefore, we only have to prove that any rectangle cover of XOR-PAIRS has exponential size. For that, we show that any rectangle in such a cover cannot be too large.
Lemma 6.4.
Any balanced rectangle for XOR-PAIRSn has size at most 27374⋅n for large enough n.
Proof:
Let n be large enough and R be a balanced rectangle from some arbitrary rectangle cover for XOR-PAIRSn. Let V=V1⊎V2 be the underlying balanced partition. We say that a pair (i,j) is split if xi, xj and zi,j do not all occur in the same set V1 or V2. Further, two pairs (i,j) and (k,l) intersect if {i,j}∩{k,l}≠∅.
First, we show that R contains at least n237 pairs that are split. For that we distinguish two cases.
Case 1. Assume that both sets V1 and V2 contain at least n6 different xi variables each. Then (i,j) is split, if xi∈V1 and xj∈V2. Thus, R has at least (n6)2=n236 split pairs.
Case 2. Otherwise we assume that V2 has w.l.o.g. at most n6 different xi variables. Since V1 has at least 5⋅n6 different xi variables, there are (5⋅n6)2=25⋅n236 different zij variables that would need to be in V1 such that V1 does not contain a split pair. However, as R is balanced, we have |V1|⩽23⋅|V|=23⋅(n2+n). Therefore, these zij variables do not all fit in V1 and for every such variable zij that is put in V2 instead, we obtain a split pair (i,j). In this way, by making V1 as large as allowed, we still get 25⋅n236−23⋅(n2+n)=n236−2⋅n3⩾n237 (for n large enough) split pairs.
Next, we have a closer look at these n237 split pairs. Since every pair (i,j) only intersects with at most 2⋅n other pairs, R has to contain at least n2∕372⋅n=n74 split pairs that are pairwise-disjoint.
Let (i,j) be one of these pairwise disjoint pairs. For the two variables xi and xj there are four possibilities to assign them. We can show that at most two of these assignments lie in our rectangle R. For that we distinguish two cases.
Case 1. xi and xj are in two different sets of V1 and V2. W.l.o.g. we assume that xi∈V1, xj∈V2 and zij∈V2. Then, the value of xi has to be fixed in R. Otherwise, R would contain two assignments that assign xj and zij in the same way but xi differently. As R contains only assignments that satisfy XOR-PAIRSn this is impossible because it contradicts zij=xi⊕xj.
Case 2. xi and xj are in the same set. W.l.o.g. we assume that xi∈V1 and xj∈V1. Since (i,j) is split, we have zij∈V2. With the same argument used in case 1, we see that the value of xi⊕xj has to be constant in R. So there are at most two of the four assignments for x1 and x2 in R.
Now, we can finally argue about the maximum size R can have. As XOR-PAIRSn has 2n models, it cannot be larger than that. However, for every pairwise-disjoint pair in R, the rectangle can only contain two of the four possible assignments. Therefore, |R|⩽2n−n74=27374⋅n. □
For XOR-PAIRSn we have to cover all 2n models with rectangles which cannot be larger than 27374⋅n. Therefore, any cover has at least size 2n74. With Theorem 6.3, we obtain the DNNF size lower bound.
Corollary 6.5.
Any DNNF computing XOR-PAIRSn has size at least 2n74 for large enough n.
Finally, by applying Theorem 6.1, we get the MICE′ lower bound as well.
Corollary 6.6.
Any MICE′ proof of XOR-PAIRSn has size 2Ω(n).
