We first show that if a formula has a short RES refutation, then the corresponding proof trace extension has a short CL proof. Intuitively, the new trace variables allow us to simulate every resolution step of the original proof individually, without worrying about extra branches left over after learning a derived clause.
Proof. Suppose contains a derived clause Ci whose strict subclause Ci' can be derived by resolving two previously occurring clauses. We can replace Ci with Ci', do trivial simplifications on further derivations that used Ci and obtain a simpler proof of F. Doing this repeatedly will remove all such redundant clauses and leave us with a simplified proof no larger in size. Hence we will assume without loss of generality that has no such clause.
Viewing as a sequence of clauses, its last two elements must be a literal, say v, and . Let S = (F {v,}). Let (C1, C2,..., Ck) be the subsequence of that has precisely the clauses in S. Note that Ci v for some i, 1ik. We claim that the branching sequence = (tC1, tC2,..., tCk) induces a CL proof of F of size k using the FirstNewCut scheme. To prove this, we show by induction that after i branching steps, the clause learning procedure branching according to has learned clauses C1, C2,..., Ci, has trace variables tC1, tC2,..., tCi set to TRUE, and is at decision level i.
The base case for induction, i = 0, is trivial. The clause learning procedure is at decision level zero and no clauses have been learned. Suppose the inductive claim holds after branching step i - 1. Let Ci = (x1 x2 ... xl). Ci must have been derived in by resolving two clauses (A y) and (B y) coming from F {C1, C2,..., Ci-1}, where Ci = (A B). The ith branching step sets tCi = FALSE. Unit propagation using trace clauses (xj tCi), 1jl, sets each xj to FALSE, thereby falsifying all literals of A and B. Further unit propagation using (A y) and (B y) implies y as well as y, leading to a conflict. The cut in the conflict graph containing y and y on the conflict side and everything else on the reason side yields Ci as the FirstNewCut clause, which is learned from this conflict. The process now backtracks and flips the branch on tCi by setting it to TRUE. At this stage, the clause learning procedure has learned clauses C1, C2,..., Ci, has trace variables tC1, tC2,..., tCi set to TRUE, and is at decision level i. This completes the inductive step.
The inductive proof above shows that when the clause learning
procedure has finished branching on all k literals in , it
will have learned all clauses in S. Adding to this the initial
clauses F that are already known, the procedure will have as known
clauses v as well as the two unit or binary clauses used to derive
v in . These immediately generate in the residual
formula by unit propagation using variable v, leading to a conflict at decision level
k. Since this conflict does not use any decision variable, fast
backtracking retracts all k branches. The conflict, however, still
exists at decision level zero, thereby concluding the clause learning
procedure and finishing the CL proof.
Proof. Let the restriction that sets every trace variable of F'n
to TRUE. We claim that
S(F'n)S(F'n|) = S(Fn)f (n) . (Fn) > f (n) . (F'n). The first inequality
holds because S is a natural proof system. The following
equality holds because keeps the original clauses of Fn
intact and trivially satisfies all trace clauses, thereby reducing the
initial clauses of F'n to precisely Fn. The next inequality
holds because S is an f (n)-proper refinement of RES. The final
inequality follows from Lemma
1.
This gives our first main result and its corollary using Proposition 2:
Remark. As clause learning yields resolution proofs of unsatisfiable formulas, CL is a refinement of RES. However, it is not necessarily a natural proof system. If it were shown to be natural, Theorem 1, by a contradiction argument, would imply that CL using the FirstNewCut scheme and no restarts is as powerful as RES itself.