# A Unified Framework for DPLL(T) + Certificates

Authors: Min Zhou; Fei He; Bow-Yaw Wang; Ming Gu; Jiaguang Sun
Journal: Journal of Applied Mathematics
 (2013)

---

## Abstract

Satisfiability Modulo Theories (SMT) techniques are widely used nowadays. SMT solvers are typically used as verification backends. When an SMT solver is invoked, it is quite important to ensure the correctness of its results. To address this problem, we propose a unified certificate framework based on DPLL(T), including a uniform certificate format, a unified certificate generation procedure, and a unified certificate checking procedure. The certificate format is shown to be simple, clean, and extensible to different background theories. The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. The soundness and completeness for DPLL(T) + certificates were established. The certificate checking procedure is straightforward and efficient. Experimental results show that the overhead for certificates generation is only 10%, which outperforms other methods, and the certificate checking procedure is quite time saving.


---

## Body

## 1. Introduction

### 1.1. Background and Motivation

Satisfiability Modulo Theories (SMT) techniques are getting increasingly popular in many verification applications. An SMT solver takes as input an arbitrary formula given in a specific fragment of first order logic with interpreted symbols. It returns a judgment telling whether the formula is satisfiable. By satisfiable, it means that there exists at least one interpretation under which the formula evaluates to true.SMT solvers are typically used as verification backends. During a verification process, SMT solver may be invoked many times. Each time the SMT solver is given a complex logical formula and is expected to give a correct judgment. However, SMT solvers employ many sophisticated data structures and tricky algorithms, which make their implementations prone to error. For instance, there are some solvers disqualified in SMT-COMP due to their incorrect judgments [1]. We therefore strongly believe that SMT solvers should be supported with a formal assessment of their correctness.Ensuring the correctness of an SMT solver is never easy. Generally, there are two approaches: to verify the SMT solver or to certify their judgments. For the former approach, it proves directly that the solver is correct. So, its judgements are naturally correct. Though rigor in logic, this method is not generally practical because verifying an SMT solver requires great workload. Not only the algorithm but also the implementation should be verified in a formal way. To the best of our knowledge, no state-of-the-art SMT solver has been completely verified. More importantly, this approach is solver dependent. Even if a solver is completely verified, the whole verification has to be done again when the solver is modified.The rationale of the latter approach is as follows: instead of proving the correctness of the solver, we prove its judgment. For this purpose, the solver is required to return a piece of evidence to support its judgment. This evidence is calledcertificate in this paper. Then, the correctness for the judgment is ensured by the certificate. If so, a rigorous and detailed proof can be constructed by referring to the certificate. Obviously, checking a certificate is much easier than verifying a solver. If the certificates are presented in a proper format, its checking algorithm could have low complexity. For instance, linear time is required to check certain certificates for unsatisfiable SAT problems. The certificate approach is solver independent. We need not to look into the solvers; the only requirement for solvers is to generate certificates. If the certificate format is unified, the certificate checking can be a uniform procedure. This benefit is vital since we need not to develop a certificate checker for each SMT solver.There are some SMT solvers that support certificate generation, such as CVC3 [2] and Z3 [3]. However, their certificate formats are quite different. As a result, the generation and checking procedures are tool specific. Although SMT solvers differ in the algorithms, we believe that their formats of certificates could be unified. The basic idea comes from SAT. In an SAT community, people consider to generate certificates along with the DPLL framework, and the certificates (for unsatisfiability instances) are unified as chains of linear regular resolutions which can lead from the initial clauses to an empty clause [4, 5]. With this uniform format, the generation and checking procedures for certificates can also be unified.This paper considers the DPLL(T) framework, which is extended from DPLL and has been widely used in state-of-the-art SMT solvers. A uniform format of SMT certificate is defined in this paper. The road map of our approach is shown in Figure 1. Note that the size of certificate can be exponential or even larger with respect to the input problem [6]. To reduce storage space, the certificate format is defined carefully in a concise way. Upon this format, a unified procedure for certificates generation is proposed. This procedure can be easily integrated into DPLL(T)-based SMT solvers. Moreover, a certificate checking procedure is also proposed in this paper. The checking procedure is easy, fast, and memory saving. To make it extensible, theory lemmas are checked by individual lemma checkers. Experimental results show that the average overhead for the certificates generation is about 10%.Figure 1
The road map of our approach.


### 1.2. Related Work

Propositional satisfiability problem (SAT) is a well-known decision problem. It was proven to be NP-complete by Cook [7] in 1971. All known algorithms for SAT have exponential complexity. State-of-the-art SAT solvers are based on DPLL [8] algorithm. The basic idea is to explore all valuations by depth-first search in a branch and bound manner. To reduce unnecessary search efforts, an optimization called clause learning is used, which learns a clause whenever it recovers from a conflict. This optimization significantly increases the performance and makes SAT algorithms practical. During the clause learning process, each learned clause is a resolvent of linear regular resolution from existing clauses [4].SMT is an extension of SAT. As the name implies, the input formula may contain theory-specific predicates and functions. For instance, while only boolean variables are allowed in SAT,x≥y∧y≥f(a)+x∨x<0 is a well-formed SMT formula. The background theory T of SMT is usually a composed theory from several individual theories. In this paper, we focus on quantifier-free SMT problems, for which the popular algorithm is DPLL(T) [9]. The DPLL(T) algorithm is extended from DPLL. Since the DPLL(T) algorithm is described as a transition system, solving an SMT problem is actually seeking a path to the success or fail state while respecting the guard conditions on transitions. Although there are other heuristics and optimizations, currently it is almost standard to develop SMT solvers based on DPLL(T).Certificates are, informally, a set of evidence that can be used to construct a rigorous proof for the judgment. For satisfiable cases, the certificate could be a model. What is more interesting is the certificates for unsatisfiable cases. Deduction steps from the input problem to a conflict should be reproducible by referring to the certificate. In this paper, when saying certificates, we refer to those for unsatisfiable cases.Many of the state-of-the-art SAT solvers can generate certificates, but their logical formats are very distinct from each other. For example, the certificate generated by zChaff [10] and MiniSat [11] are quite different. PicoSAT [12] generates concise and well-defined certificates. A tool called TraceCheck can do certificate checking [12]. In PicoSAT's certificates, there are initial clauses and resolvents. Resolvents are obtained from linear regular resolution. If all the clauses form a directional acyclic graph and the empty clause is derived, then it implies that the initial clause set is unsatisfiable. As shown in [4, 5], clause learning in DPLL corresponds to a linear regular resolution. So, this certificate format is also adoptable by other DPLL-based solvers.For general SMT problems, quantifiers may be used. Furthermore, theory-specific inference rules should be considered when deciding their satisfiability. Various logical frameworks are developed to provide flexible languages to write their proof, such reference could be found in [13–16]. If we focus on quantifier-free problems, the proof format and proof checking could be simplified. In practice, solvers such as CVC3 and Z3 can generate certificates, but their formats are also quite different because they use different proof rules. Proof rules are a set of inference rules with respect to the background theory T. To be better suited for certificate generation and checking, the certificate format should not depend heavily on theory-specific proof rules.The overhead for generating certificates should be as small as possible. An approach with 30% overhead is presented in [17], which uses the Edinburgh Logical Framework with Side Condition (LFSC). In our approach, we focus on quantifier-free problems so that the overhead is further reduced. Certificate generation is related to unsatisfiable core computation. In [18], a simple and flexible way of computing small unsatisfiable core in SMT was proposed. They compute by the propositional abstraction of SMT problem and invoke an existing unsatisfiable core extractor for SAT. Although the idea might be similar, unsatisfiable core computation concerns which clauses lead to unsatisfiability, whereas certificate generation concerns how. It is convenient to generate unsatisfiable core from certificates, but not vice versa.To check certificates, people can either check the certificate directly, just as in the SAT case, or translate them into inputs for some theorem provers such as HOL Light [19] or Isabelle/HOL [20]. There is also research in checking certificates using simple term rewriting [21]. A known fact is that if certificates are checked by translating them to proof items for theorem provers, it could take much longer time than certificate finding [20].


### 1.3. Contribution

In this paper, we present a certificate framework for quantifier-free formulas. Compared to other works, our approach has the following advantages.(i)
The certificate format is simple, clean, and extensible to different underlying theories.(ii)
The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. We also implement it in our solver.(iii)
On average, the certificate generation induces about 10% overhead which is much less than other approaches.(iv)
The certificate checking procedure is simplified. It has better performance.The rest of this paper is organized as follows. In Section2, we recall the original  DPLL(T) algorithm. The certificate format is defined in Section 3. The framework of  DPLL(T) + certificate is described in Section 4, where the formal rules are defined in Section 4.1, necessary implementation issues are discussed in Section 4.2, the properties are discussed in Section 4.3, and a couple of examples are shown in Section 4.4. Section 5 discusses the certificate checking matters. Experiments’ results are shown in Section 6. Finally, Section 7 concludes the paper.


## 1.1. Background and Motivation

Satisfiability Modulo Theories (SMT) techniques are getting increasingly popular in many verification applications. An SMT solver takes as input an arbitrary formula given in a specific fragment of first order logic with interpreted symbols. It returns a judgment telling whether the formula is satisfiable. By satisfiable, it means that there exists at least one interpretation under which the formula evaluates to true.SMT solvers are typically used as verification backends. During a verification process, SMT solver may be invoked many times. Each time the SMT solver is given a complex logical formula and is expected to give a correct judgment. However, SMT solvers employ many sophisticated data structures and tricky algorithms, which make their implementations prone to error. For instance, there are some solvers disqualified in SMT-COMP due to their incorrect judgments [1]. We therefore strongly believe that SMT solvers should be supported with a formal assessment of their correctness.Ensuring the correctness of an SMT solver is never easy. Generally, there are two approaches: to verify the SMT solver or to certify their judgments. For the former approach, it proves directly that the solver is correct. So, its judgements are naturally correct. Though rigor in logic, this method is not generally practical because verifying an SMT solver requires great workload. Not only the algorithm but also the implementation should be verified in a formal way. To the best of our knowledge, no state-of-the-art SMT solver has been completely verified. More importantly, this approach is solver dependent. Even if a solver is completely verified, the whole verification has to be done again when the solver is modified.The rationale of the latter approach is as follows: instead of proving the correctness of the solver, we prove its judgment. For this purpose, the solver is required to return a piece of evidence to support its judgment. This evidence is calledcertificate in this paper. Then, the correctness for the judgment is ensured by the certificate. If so, a rigorous and detailed proof can be constructed by referring to the certificate. Obviously, checking a certificate is much easier than verifying a solver. If the certificates are presented in a proper format, its checking algorithm could have low complexity. For instance, linear time is required to check certain certificates for unsatisfiable SAT problems. The certificate approach is solver independent. We need not to look into the solvers; the only requirement for solvers is to generate certificates. If the certificate format is unified, the certificate checking can be a uniform procedure. This benefit is vital since we need not to develop a certificate checker for each SMT solver.There are some SMT solvers that support certificate generation, such as CVC3 [2] and Z3 [3]. However, their certificate formats are quite different. As a result, the generation and checking procedures are tool specific. Although SMT solvers differ in the algorithms, we believe that their formats of certificates could be unified. The basic idea comes from SAT. In an SAT community, people consider to generate certificates along with the DPLL framework, and the certificates (for unsatisfiability instances) are unified as chains of linear regular resolutions which can lead from the initial clauses to an empty clause [4, 5]. With this uniform format, the generation and checking procedures for certificates can also be unified.This paper considers the DPLL(T) framework, which is extended from DPLL and has been widely used in state-of-the-art SMT solvers. A uniform format of SMT certificate is defined in this paper. The road map of our approach is shown in Figure 1. Note that the size of certificate can be exponential or even larger with respect to the input problem [6]. To reduce storage space, the certificate format is defined carefully in a concise way. Upon this format, a unified procedure for certificates generation is proposed. This procedure can be easily integrated into DPLL(T)-based SMT solvers. Moreover, a certificate checking procedure is also proposed in this paper. The checking procedure is easy, fast, and memory saving. To make it extensible, theory lemmas are checked by individual lemma checkers. Experimental results show that the average overhead for the certificates generation is about 10%.Figure 1
The road map of our approach.


## 1.2. Related Work

Propositional satisfiability problem (SAT) is a well-known decision problem. It was proven to be NP-complete by Cook [7] in 1971. All known algorithms for SAT have exponential complexity. State-of-the-art SAT solvers are based on DPLL [8] algorithm. The basic idea is to explore all valuations by depth-first search in a branch and bound manner. To reduce unnecessary search efforts, an optimization called clause learning is used, which learns a clause whenever it recovers from a conflict. This optimization significantly increases the performance and makes SAT algorithms practical. During the clause learning process, each learned clause is a resolvent of linear regular resolution from existing clauses [4].SMT is an extension of SAT. As the name implies, the input formula may contain theory-specific predicates and functions. For instance, while only boolean variables are allowed in SAT,x≥y∧y≥f(a)+x∨x<0 is a well-formed SMT formula. The background theory T of SMT is usually a composed theory from several individual theories. In this paper, we focus on quantifier-free SMT problems, for which the popular algorithm is DPLL(T) [9]. The DPLL(T) algorithm is extended from DPLL. Since the DPLL(T) algorithm is described as a transition system, solving an SMT problem is actually seeking a path to the success or fail state while respecting the guard conditions on transitions. Although there are other heuristics and optimizations, currently it is almost standard to develop SMT solvers based on DPLL(T).Certificates are, informally, a set of evidence that can be used to construct a rigorous proof for the judgment. For satisfiable cases, the certificate could be a model. What is more interesting is the certificates for unsatisfiable cases. Deduction steps from the input problem to a conflict should be reproducible by referring to the certificate. In this paper, when saying certificates, we refer to those for unsatisfiable cases.Many of the state-of-the-art SAT solvers can generate certificates, but their logical formats are very distinct from each other. For example, the certificate generated by zChaff [10] and MiniSat [11] are quite different. PicoSAT [12] generates concise and well-defined certificates. A tool called TraceCheck can do certificate checking [12]. In PicoSAT's certificates, there are initial clauses and resolvents. Resolvents are obtained from linear regular resolution. If all the clauses form a directional acyclic graph and the empty clause is derived, then it implies that the initial clause set is unsatisfiable. As shown in [4, 5], clause learning in DPLL corresponds to a linear regular resolution. So, this certificate format is also adoptable by other DPLL-based solvers.For general SMT problems, quantifiers may be used. Furthermore, theory-specific inference rules should be considered when deciding their satisfiability. Various logical frameworks are developed to provide flexible languages to write their proof, such reference could be found in [13–16]. If we focus on quantifier-free problems, the proof format and proof checking could be simplified. In practice, solvers such as CVC3 and Z3 can generate certificates, but their formats are also quite different because they use different proof rules. Proof rules are a set of inference rules with respect to the background theory T. To be better suited for certificate generation and checking, the certificate format should not depend heavily on theory-specific proof rules.The overhead for generating certificates should be as small as possible. An approach with 30% overhead is presented in [17], which uses the Edinburgh Logical Framework with Side Condition (LFSC). In our approach, we focus on quantifier-free problems so that the overhead is further reduced. Certificate generation is related to unsatisfiable core computation. In [18], a simple and flexible way of computing small unsatisfiable core in SMT was proposed. They compute by the propositional abstraction of SMT problem and invoke an existing unsatisfiable core extractor for SAT. Although the idea might be similar, unsatisfiable core computation concerns which clauses lead to unsatisfiability, whereas certificate generation concerns how. It is convenient to generate unsatisfiable core from certificates, but not vice versa.To check certificates, people can either check the certificate directly, just as in the SAT case, or translate them into inputs for some theorem provers such as HOL Light [19] or Isabelle/HOL [20]. There is also research in checking certificates using simple term rewriting [21]. A known fact is that if certificates are checked by translating them to proof items for theorem provers, it could take much longer time than certificate finding [20].


## 1.3. Contribution

In this paper, we present a certificate framework for quantifier-free formulas. Compared to other works, our approach has the following advantages.(i)
The certificate format is simple, clean, and extensible to different underlying theories.(ii)
The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. We also implement it in our solver.(iii)
On average, the certificate generation induces about 10% overhead which is much less than other approaches.(iv)
The certificate checking procedure is simplified. It has better performance.The rest of this paper is organized as follows. In Section2, we recall the original  DPLL(T) algorithm. The certificate format is defined in Section 3. The framework of  DPLL(T) + certificate is described in Section 4, where the formal rules are defined in Section 4.1, necessary implementation issues are discussed in Section 4.2, the properties are discussed in Section 4.3, and a couple of examples are shown in Section 4.4. Section 5 discusses the certificate checking matters. Experiments’ results are shown in Section 6. Finally, Section 7 concludes the paper.


## 2. The DPLL(T) Algorithm

The DPLL(T) algorithm was proposed in [9]. The input is a quantifier-free first order formula in conjunctive normal form (CNF) from the background theory T. DPLL(T) was given as a transition system. Most features and optimizations of SMT algorithms can be formalized in that way.In first order logic, any CNF formula can be viewed as a set of clauses. Each clause is disjunction of literals, and each literal is a positive or negative form of an atom. A formula is satisfiable if there exists an interpretation under which the formula evaluates to true.In DPLL(T), formula satisfiability is considered in some background theory T (all interpreted symbols should be from T). We use “⊨T” to denote theory entailment in T. Given sets of formulas Σ and Γ, if any interpretation that satisfies all formulas in Σ also satisfies all formulas Γ, we write Σ⊨TΓ. Similarly, “⊨” denotes propositional entailment which consider each atomic formula syntactically as a propositional literal.Each state is a 2-tuple “M∥F” where M is a stack of the currently asserted literals and F the set of clauses to be satisfied. The transition relations are given by the following rules.(i)Decide:Precondition
(1)
l or ¬l occurs in a clause of F;
(2)
l is undefined in M,
(1)M∥F↦Mld∥F.(ii)UnitPropagate:Precondition
(1)
M
⊨
¬
C;
(2)
l is undefined in M,
(2)M∥F,C∨l↦Ml∥F,C∨l.(iii)TheoryPropagate:Precondition
(1)
M
⊨
T
l;
(2)
l or ¬l occurs in F;
(3)
l is undefined in M,
(3)M∥F↦Ml∥F.(iv)T-Backjump:Precondition
(1)
M
l
d
N
⊨
¬
C;
(2)
there is some clauseC′∨l′ such that:
(a)
F
,
C
⊨
T
C
′
∨
l
′ and M⊨¬C′;
(b)
l
′ is undefined in M;
(c)
l
′ or ¬l′ occurs in F or in MldN,
(4)MldN∥F,C↦Ml′∥F,C.(v)T-Learn:Precondition
(1)
each atom ofC occurs in F or in M;
(2)
F
⊨
T
C,
(5)M∥F↦M∥F,C.(vi)T-Forget:Precondition
F
⊨
T
C,
(6)M∥F,C↦M∥F.(vii)Restart:Precondition
T
(7)
M
∥
F
↦
∅
∥
F
.(viii)Fail:Precondition
(1)
M
⊨
¬
C;
(2)
M contains no decision literals,
(8)M∥F,C↦〈Fail〉.In DPLL(T) algorithm, there is an assumption that there exists a T-solver that can check the consistency of conjunctions of literals given in T. This algorithm will terminate under weak assumption and is proven sound and complete [9].


## 3. The Certificate Format

If a formula is satisfiable, the certificate is simply an interpretation under which the formula evaluates to true. On the other hand, if it is unsatisfiable, the certificate could be much more complicated. It should be proven that “all attempts to find a model failed.” More precisely, each branch of the search tree must be tried. Technically speaking, thisclosed search tree can be presented as a refutation procedure which contains sequences of resolution procedures that produce the empty clause [12]. It is imaginable that if the search tree is quite large so is the set of refutation clauses.Remember that in first order logic (FOL), constants are considered as nullary functions. Then, a term is either a variable or a function with arguments which are also terms. For example,x, f(x,y) and ϕ(s,ψ(t)) are valid terms. An atom (or atomic formula) is a predicate with arguments being terms. Note that nullary predicates are actually propositional variables.Definition 1 (T-atom, T-literal).
Given a background theoryT, a T-atom is an atom whose functions and predicates are in the signature of T. A T-literal is the positive or negative form of a T-atom.For example, givenT the theory of Equality with Uninterpreted Functions, if p is a propositional variable, then p, x=f(y) are T-atoms and p, ¬p, x=f(y) and x≠f(y) are T-literals.A proof rule is an inference rule which has severalT-literals as premises and one T-literal as the conclusion. For proof rules whose conclusion is conjunction of n  T-literals, we can split it to n proof rules and one for each.) For example, x=y implies that f(x)=f(y) is a proof rule (the monotonicity of equality). This rule holds for all T-terms x,y and all function f. Each proof rule can be instantiated to a theory lemma. For instance, if s,t are two specific T-terms and g is a specific function, then (s=t)→(g(s)=g(t)) is a theory lemma.Definition 2 (clause item).
A clause item is one of the following three forms.(i)
Init  l1∨⋯∨ln: an initial clause l1∨⋯∨ln, where all li are T-literals.(ii)
Res  {C1,…,Cn}: a clause obtained from a linear resolution of C1,…,Cn, where all Ci are clauses items.(iii)
Lemma  l1∧⋯∧ln→l′: a theory lemma where all li and l′ are T-literals. The defined clause is ¬l1∨⋯∨¬ln∨l′.A resolution chainC1,C2,…,Cn is called a linear regular resolution chain if there exists a sequence of clauses D1,D2,…,Dn-1 such that: (1) D1 is the resolvent of C1 and C2; (2) for 2≤i<n, Di is the resolvent of Di-1 and Ci+1; (3) all resolutions are applied on different T-atoms.A clause item gives the syntax form for a clause. For each clause itemC, if it is well defined; the concrete form of C (given as disjunction of T-literals) can be calculated. It is called a concrete clause, denoted by ⟦C⟧. We do not distinguish C and ⟦C⟧ when no ambiguity is caused.Definition 3 (certificate item).
A certificate item is either of the following:(i)
Define ClauseItem,(ii)
Forget ClauseItem.Definition 4 (certificate).
A certificateP with respect to an SMT instance is a sequence of certificate items. The size of P, denoted by |P|, is the number of certificate items contained in P. P[i] is the ith element in P, for i=1,2,…,|P|.Definition 5 (context).
Given a certificateP and a number 0≤i≤|P|, the context with respect to i, denoted by ⌊P⌋, is a set of clause items such that:
(9)⌊P⌋i={∅ifi=0⌊P⌋i-1∪{C}ifi>0andP[i-1]isDefineC⌊P⌋i-1∖{C}ifi>0andP[i-1]isForgetC.Specially, denote⌊P⌋|P| by ⌊P⌋.Example 6.
Assume thatl1:x=y, l2:f(x)=f(y) and C1:¬l1∨¬l2, C2:l1. A certificate for the unsatisfiability of the clause set {C1,C2} is presented in Table 1. In this example, {C1,C2} is intuitively unsatisfiable. Note that C2 entails l1 which implies l2 in  TEUF, while C1,C2⊨¬l2.Table 1
A certificate example.
Clause item
⟦
C
⟧
Lemma
C
1
Define
Init
¬
l
1
∨
¬
l
2
¬
l
1
∨
¬
l
2
C
2
Define
Init
l
1
l
1
C
3
Define
Lemma
l
1
→
l
2
¬
l
1
∨
l
2
The property of “=”
C
4
Define
Res
C
1
,
C
3
,
C
2
□
The empty clauseDefinition 7 (well-formed certificate).
A certificateP is well formed if for all 1≤i≤|P|:  (i)
ifP[i]is aDefineitem then one of the following conditions hold:
(a)
it is ofInit type;(b)
it is ofRes{C1,…,Cn} type where Ck∈⌊P⌋i-1 for all 1≤k≤n, and there should be a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to P[i];(c)
it is ofLemma type and the concrete clause is valid in theory T, that is, ⊨T⟦P[i]⟧;(ii)
otherwiseP[i]is a Forget item and the referred clause must be defined in⌊P⌋i-1.


## 4. Certificate Generation with DPLL(T)

The certificate generation algorithm is described in this section. We first describe the abstract rule and implementation issues, then prove some important properties, and finally give a couple of examples.


### 4.1. The CDPLL(T) Algorithm

We describe here a certificate generation procedure that can be well adapted to the  DPLL(T) algorithm. The extension of DPLL(T) with certificate generation is called  CDPLL(T).Definition 8 (certificate refinement).
The certificate obtained by appending a certificate itemC to the end of the certificate P is denoted by P⊲C.We use a transition system to model the CDPLL(T) algorithm. Each state is represented as a 3-tuple “M∥F⊕P,” where M is the literal stack, F the clause set to be satisfied, and P the current certificate. The transition rules in CDPLL(T) are follows.(i)Decide:Precondition
(1)
l or ¬l occurs in a clause of F;
(2)
l is undefined in M,
(10)M∥F⊕P↦Mld∥F⊕P.(ii)UnitPropagate:Precondition
(1)
M
⊨
¬
C;
(2)
l is undefined in M,
(11)M∥F,C∨l⊕P↦Ml∥F,C∨l⊕P.(iii)TheoryPropagate:Precondition
(1)
M
⊨
T
l;
(2)
l or ¬l occurs in F;
(3)
l is undefined in M,
(12)M∥F⊕P↦Ml∥F⊕P.(iv)T-Backjump:Precondition
(1)
M
l
d
N
⊨
¬
C;
(2)
there exists a clauseC′∨l′ such that: (a) F,C⊨TC′∨l′ and M⊨¬C′, (b) l′ is undefined in M, and (c) l′ or ¬l′ occurs in F or in MldN;
(3)
R
=
{
C
1
,
C
2
,
…
,
C
n
} is a set of clause items such that: Ci∈⌊P⌋ for all i, and there exists a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to C′∨l′,
(13)MldN∥F,C⊕P↦Ml′∥F,C⊕(P⊲Res(R)).(v)T-Learn(I): this rule models the clause learning procedure.Precondition
(1)
Each atom ofC occurs in F or in M;
(2)
F
⊨
C;
(3)
R
=
{
C
1
,
C
2
,
…
,
C
n
} is a set of clause items such that: Ci∈⌊P⌋ for all i, and there exists a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to C,
(14)M∥F⊕P↦M∥F,C⊕(P⊲Res(R)).(vi)T-Learn(II): this rule models the learning of theory lemma.Precondition
(1)
Each atom ofC occurs in F or in M;
(2)
⊨
T
C,
(15)M∥F⊕P↦M∥F,C⊕(P⊲Lemma(C)).(vii)T-Forget:Precondition
F
⊨
T
C,
(16)M∥F,C⊕P↦M∥F⊕(P⊲Forget(C)).(viii)Restart:Precondition
T
(17)
M
∥
F
⊕
P
↦
∅
∥
F
⊕
P
.(ix)Fail:Precondition
(1)
M
⊨
¬
C;
(2)
M contains no decision literals;
(3)
R
=
{
C
1
,
C
2
,
…
,
C
n
} is a set of clause items such that: Ci∈⌊P⌋ for all i, and there exists a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to □,
(18)M∥F,C⊕P↦〈Fail〉⊕(P⊲Res(R)).The initial state isM∥F⊕P0 where P0 is the certificate that defines all initial clauses. When a final state 〈Fail〉⊕P is reached, P is the obtained certificate for the unsatisfiability judgment.The major differences between CDPLL(T) and DPLL(T) are as follows. (1) Certificate generation is added. Notice the modifications to rules T-Backjump, T-Learn, T-Forget, and T-Fail. (2) In order to generate well-formed certificates, the original T-Learn rule is split into 2 cases, one for the learning of resolvents (corresponds to clause learning) and the other for the learning of theory lemmas (corresponds to deductions in T). The first three rules are unchanged except the certificate part.


### 4.2. Implementation of CDPLL(T)

In a real implementation of CDPLL(T), additional information need to be collected to construct the certificate items. In this section, we discuss these details.Lemma 9.
For any reachable stateM∥F⊕P in CDPLL(T) and any clause C∈F, there exists a clause item D∈⌊P⌋ such that ⟦D⟧=C.Proof.
We prove that by induction. Initially, this property holds because all clauses inF0 are initial clauses and P0 consists of all initial clause items (by definition). At each valid transition step, the clause set F and the certificate P may be modified. However, each rule ensures that whenever a clause C is added to F, there is always a clause item D such that ⟦D⟧=C added to P, for example, in the rule T-Learn(I). Furthermore, whenever a clause item is removed from P, the corresponding clause is removed in F, for example, in the rule T-Forget. Thus, the property holds on all valid trace of CDPLL(T).


#### 4.2.1. Record Reasons

For any literall in M, it is either added by the Decide rule or forced by a clause or theory lemma. For the latter case, we need to record a clause item which is a deduction of the lemma and from which the literal l can be enforced. We call this item the reason for literal l being in M.Only rulesUnitPropagate, TheoryPropagate, and T-Backjump can enforce new literal to M. We discuss in the following the reasons recorded by these three rules. (i)
UnitPropagate: the reason is a certificate item D such that ⟦D⟧=C∨l∈F. By Lemma 9, such item always exists.(ii)
TheoryPropagate: assume that M=l1∧l2∧⋯∧lm and M⊨Tl; then, the reason is a certificate item D such that ⟦D⟧=¬l1∨¬l2∨¬⋯∨¬lm∨l.(iii)
T-Backjump: the reason for l′ is a certificate item D such that ⟦D⟧=C′∨l′. We will show in the following that such certificate item always exists when T-Backjump is applicable.For convenience, a subscript is used to denote the reason, for example, l(D) denotes the literal l asserted by the reason ⟦D⟧.


#### 4.2.2. Learn Clauses

In rulesT-Backjump and Fail, once there is a conflict, a backjump clause needs be learned. Furthermore, if there are some branches that have not been explored, T-Backjump is applied; otherwise, Fail is applied. Each clause learning procedure introduces some new certificate items.We use implication graph to analyze the clause learning process. Remember that in DPLL all literals are propositional atoms, the implication graph is simply a direct acyclic graph (DAG) where each edge corresponds to a deduction step. In CDPLL(T), the implication graph has two kinds of deductions: propositional deduction (which is similar to DPLL) and theory deduction. Each deduction step in the implication graph is labelled with a reason C. This graph can be viewed as a generalized implication graph. Without causing ambiguity, we still call it an implication graph.In the implication graph of DPLL, each cut containing the conflict literals corresponds to a learned clause (by resolving all the associated clauses of edges in this cut) [4]. No matter which criteria (e.g., 1-UIP) is used, the rule for clause learning is applicable. For CDPLL(T), when considering the generalized implication graphs, the clause learning rule is also applicable.There are two situations whereT-Backjump can be applied. Given a state M∥F⊕P, the first situation is that there exists a clause C∈F which is falsified by M, that is, ⊭M,C. Then, C is called the conflict clause. As in the rule, some backjump clause C′∨l′ should be learned by analyzing the conflict. Usually, C′∨l′ is a resolvent of a linear resolution. A certificate item with resolution type will be learned.The other situation is thatM itself becomes T-inconsistent. Then, a subset {l1,l2,…,lm} of M is unsatisfiable, that is, ⊨T¬l1∨¬l2∨⋯∨¬lm. This is also a conflict clause. It may not belong to F, but it can definitely be learned from F along with some theory lemmas. The fact that l1,…,lm leads to conflict is represented in the generalized implication graph. Furthermore, the clause C′∨l′ that is required by the rule T-Backjump can also be learned by generalized conflict clause analysis.In both situations, the backjump clauses are learned by clause learning. The certificate for unsatisfiability is actually a well-organized collection of these clause items. IfFail is applicable, no literal in M is decision variable; then, the learnt clause is the empty clause which shows F⊨T□.Example 10.
A generalized implication graph is shown in Figure2, where the literals are as follows: l0:x=y, l1:f(x)=f(y), and p is a propositional literal. Clauses are as follows:
(19)C0:¬l0∨¬l1:=¬(x=y)∨(f(x)=f(y)),C1:l0∨p:=x=y∨p,C2:l0∨¬p:=x=y∨¬p.Figure 2
Example of a generalized implication graph.Assume the current assignmentM=p,l0,¬l1. Then, there is a conflict between ¬l1 and l1. In all, there are 3 deductions in the implication graph: p→l0 forced by C2, l0→¬l1 by C0 and l0→l1 by the theory lemma C3. Among those reasons, solid lines correspond to existing clauses in F, while dashed lines correspond to theory lemmas. C3 is actually a theory lemma l0→l1(x=y→f(x)=f(y)).In the clause learning procedure, we start from the conflict(¬(l1∧¬l1)=¬l1∨l1) and trace back (apply a sequence of resolutions). If the 1st UIP schema [4] is used, it is possible to learn ¬p or ¬l0 (corresponds to cut1 and cut2, resp.). The resolution steps for learning ¬p are shown in Figure 3. Actually, ¬p is the resolvent of {C3,C0,C2} which are exactly the reasons labeled on the edges from the conflict to the cut. Among those, C0,C2 are normal clauses, and C3 is a theory lemma.Figure 3
Resolution steps for learning¬p.Based on the above discussions, the related rules can be interpreted more precisely as follows.(i)TheoryPropagate:
(20)M∥F⊕P↦Ml(C)∥F⊕P.
The precondition requires that M⊨Tl. Let M′ be a subset of M which entails l (possibly M′=M). Let C=¬M′∨l, then ⊨TC. Furthermore, M,C⊨Tl, which means C is a unit clause under the assignment M. Thus, C is the reason of l.(ii)UnitPropagate:
(21)M∥F,C∨l⊕P↦Ml(C∨l)∥F,C∨l⊕P.
The precondition requires that M⊨¬C; thus, C∨l is a unit clause under M. So, the reason of l is C∨l.(iii)T-Backjump:
(22)MldN∥F,C⊕P↦Ml′(C′∨l′)∥F,C⊕(P⊲Res(R)).
The precondition requires that there exits some clause C′∨l′ such that F,C⊨TC′∨l′ and M⊨¬C′. The clause C′∨l′ is then used as the reason for l′. As the clause learning is always applicable [9], this clause always exists. If the assignment MldN is T-consistent, then there must be some conflict clause C∈F. As explained above, the clause learning will then be applied, and the learned clause will be C′∨l′. On the other hand, when MldN is T-inconsistent, clause learning is also applicable in the generalized implication graph and generates a candidate C′∨l′. In both cases, C′∨l′ can be learned by applying linear regular resolutions on a clause set R [4]. Moreover, such R is the union of a subset of reasons in MldN and a group of theory lemmas.(iv)Fail:
(23)M∥F,C⊕P↦〈Fail〉⊕(P⊲Res(R)).
The Fail rule is similar to T-Backjump except that the learned clause is the empty clause.


### 4.3. Properties of CDPLL(T)

The soundness and completeness of CDPLL(T) are proven in this subsection.Lemma 11.
A well-formed certificate modified byT-Backjump, T-Learn(I), T-Learn(II), Fail, or T-Forget is still well formed.Proof.
Each of the 4 rules appends a new item to the certificate. Assume that the certificateP is modified to P′=P⊲I where I is the appended certificate item. The well-formed property of P′ is checked by case studying the rules applied.(i)
ForT-Backjump: a certificate item of resolution type is appended. According to the precondition, the certificate items referred by I are already defined in ⌊P⌋. So, P′ is still well formed.(ii)
ForT-Learn(I): similar to the previous case. The dependency of appended certificate item is satisfied.(iii)
ForT-Learn(II): a theory lemma item C is appended. It is required that ⊨TC. Thus, P′ is still well formed.(iv)
ForFail: similar to the T-Backjump case.(v)
ForT-Forget: the rule requires that the forgotten clause is in the clause set. By Lemma 9, we know that there is a certificate item in P which defines C. Thus, the well formedness is ensured.With the help of this lemma, it can be proven that CDPLL(T) procedure always generates well-formed certificates.Lemma 12.
Given any reachable stateM∥F⊕P in any CDPLL(T) procedure, P is a well-formed certificate.Proof.
First of all, the initial certificateP0 is well formed because it only contains initial items. Secondly, the certificate is only modified in T-Backjump, T-Learn(I), T-Learn(II), Fail, and T-Forget. By Lemma 11, these rules will preserve well formedness. So, following any path of CDPLL(T) will always generate a well-formed certificate. That completes the proof.Theorem 13 (soundness).
Given a clause setF0, for any certificate P, if Mx∥Fx⊕Px is reachable in a CDPLL(T)  procedure, then Mx∥Fx is also reachable in a DPLL(T) procedure. Specially, if 〈Fail〉  ⊕P is reachable in CDPLL(T), then 〈Fail〉 is also reachable in DPLL(T).Proof.
For each transition step in CDPLL(T):
(24)M∥F⊕P⟶CDPLL(T)M′∥F′⊕P′,
it holds that
(25)M∥F⟶DPLL(T)M′∥F′.
So, given a CDPLL(T) trace, a trace in DPLL(T) can be obtained by removing the certificate part. If Mx∥Fx⊕Px is reachable in CDPLL(T) so is Mx∥Fx in DPLL(T).Theorem 14 (completeness).
Given a clause setF0, if the state Mx∥Fx is reachable in a DPLL(T) procedure, then there must be a certificate Px such that Mx∥Fx⊕Px is reachable in a DPLL(T) procedure. Furthermore, if 〈Fail〉 is reachable in a DPLL(T) procedure, then 〈Fail〉  ⊕Px is reachable in a CDPLL(T) and □∈⌊Px⌋.Proof.
For rulesDecide, TheoryPropagate, UnitPropagate, T-Learn(II), T-Forget, and Restart, the preconditions are equal to those in CDPLL(T). So, if there is a transition in DPLL(T)  labelled with one of these rules, there could also be the same transition in CDPLL(T).
For other rules,T-Backjump, T-Learn(I), and Fail, we need to prove that: if Mx∥Fx is reachable, then there is some certificate Px such that Mx∥Fx⊕Px is reachable. We prove that by induction. Initially, this condition holds because the initial state M0∥F0 corresponds to M0∥F0⊕P0. Inductively, if
(26)M∥F⟶DPLL(T)M′∥F′
is a possible transition in DPLL(T), and there is some P such that M∥F⊕P is reachable in CDPLL(T).  (i)
If it is labelled withT-Learn(I), because the learned clause is from clause learning, and clause learning corresponds to linear regular resolution. It is always possible that necessary theory lemmas in the implication graph are learned at first by Learn(II) and get to a state M∥F⊕P′′, on which the preconditions of Learn(I) are satisfied. Then, M′∥F′⊕P′ is reached.(ii)
If it is labelled withT-Backjump or Fail, the situation is similar.Our approach can be well adapted to any DPLL(T)-based SMT solver. It is sound and complete regardless of the theory learning scheme used or the order of the decision procedure. It works well as long as clause learning is based on the generalized implication graph.


### 4.4. Examples

A couple of examples are discussed in this subsection. The first example is given as a CNF formula on propositional variables. In this case, the SMT problem reduces to an SAT problem. No theory deduction is involved in this example; so, we can get a general idea of the structure of certificates.Example  1. Consider the following clause set:
(27)C1=¬l1∨¬l2∨¬l3,C2=¬l1∨¬l2∨l3,C3=¬l1∨l2,C4=l1∨¬l2,C5=l1∨l2.LetF0={C1,C2,C3,C4,C5}; assume that P0 defines everything in F0 as initial clause; then, a possible CDPLL(T) procedure is shown in Table 2, where “~” means this field is the same as that in the previous row.Table 2
The  CDPLL(T)  procedure for Example  1.
No.
M
∥
F
⊕
P
Reason
Explanation
1
∅
∥
F
0
⊕
P
0
∅
Initial state
2
l
1
d
∥
~
⊕~
∅
Decide
3
l
1
d
,
l
2
∥
~
⊕~
l
2
↦
C
3
UnitPropagate
4
l
1
d
,
l
2
,
¬
l
3
∥
~
⊕~
{
l
2
↦
C
3
¬
l
3
↦
C
1
UnitPropagate now C2 is falsified
5
¬
l
1
∥
{
F
0
C
6
=
¬
l
1
⊕
[
P
0
⊲
R
e
s
{
C
1
,
C
2
,
C
3
}
=
C
6
]
¬
l
1
↦
C
6
C
6
=
¬
l
1 is learned
T-Backjump
6
¬
l
1
,
¬
l
2
∥
~
⊕~
{
¬
l
1
↦
C
6
¬
l
2
↦
C
4
UnitPropagate
7
〈
Fail
〉
∥
~
⊕
[
P
0
⊲
R
e
s
{
C
1
,
C
2
,
C
3
}
=
C
6
R
e
s
{
C
4
,
C
5
,
C
6
}
=
□
]
∅
FailIn step 4,C2=¬l1∨¬l2∨l3 is falsified. By analysing the implication graph, a clause is learned from C1,C2,C3. Among the referred clauses, C2 is a falsified clause, and C1,C3 are in the reasons. In step 7, C4 is falsified, but there is no decision variable. By analysing the implication graph, we can find a resolution from C4,C5,C6 to the empty clause. Among the referred clauses, C4 is a falsified clause, and C5,C6 are in the reasons.Example  2. Consider the background theory TEUF and a clause set F containing the following:
(28)(C1)a=b∨g(a)≠g(b),(C2)h(a)≠h(c)∨p,(C3)g(a)=g(b)∨¬p,(C4)h(a)=h(c)∨a=c,(C5)f(a)≠f(b),(C6)b=c.
Its boolean structure is
(29)C1=l1∨¬l5,C2=¬l6∨p,C3=l5∨¬p,C4=l6∨l2,C5=¬l4,C6=l3,
where
(30)l1:a=b,l2:a=c,l3:b=c,l4:f(a)=f(b),l5:g(a)=g(b),l6:h(a)=h(c).A possible CDPLL(T) procedure is shown in Table 3, where the referred certificates are as follows:
(31)P1=[P0⊲Lemma(¬l1∨l4)=C7],P2=[P0⊲Lemma(¬l1∨l4)=C7Lemma(l2∧l3⟶l1)=C8],P3=[P0⊲Lemma(¬l1∨l4)=C7Lemma(l2∧l3⟶l1)=C8Res{C8,C7,C4,C6,C2,C3,C1}=□].Table 3
A possible  CDPLL(T)  procedure.
No.
M
∥
F
⊕
P
Reason
Explanation
1
∅
∥
F
0
⊕
P
0
∅
Initial state
2
¬
l
4
∥
~
⊕
~
¬
l
4
↦
C
5
UnitPropagation
3
¬
l
4
,
l
3
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
UnitPropagation
4
¬
l
4
,
l
3
,
l
1
d
∥
~
⊕~
~
Decide  M becomes T-inconsistent
5
~
∥
F
0
∪
{
C
7
}
⊕
P
1
~
T-Learn(II), C7 is learned
6
¬
l
4
,
l
3
,
¬
l
1
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
T-Backjump
7
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
UnitPropagation
8
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
,
¬
p
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
¬
p
↦
C
3
UnitPropagation
9
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
,
¬
p
,
¬
l
6
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
¬
p
↦
C
3
¬
l
6
↦
C
2
UnitPropagation
10
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
,
¬
p
,
¬
l
6
,
l
2
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
¬
p
↦
C
3
¬
l
6
↦
C
2
l
2
↦
C
4
UnitPropagation  M becomes T-inconsistent
11
~
∥
F
0
∪
{
C
7
,
C
8
}
⊕
P
2
~
T-Learn(II), C8 is learned
12
~
∥
F
0
∪
{
C
7
,
C
8
}
⊕
P
3
~
Fail, □ derivedIn step 4,M becomes T-inconsistent. The generalized implication graph is shown in Figure 4. A theory lemma C7=¬l1∨l4 is learned (instantiated the monotonicity property of the equality) firstly, then the backjump rule is applicable. In steps 11 and 12, M becomes T-inconsistent again. A theory lemma C8=l2∧l3→l1 is then learned (transitivity of equality), and then clause learning is performed which learns the empty clause. The implication graph is shown in Figure 5.Figure 4
The implication graph in step 4.Figure 5
The implication graph in steps 11 and 12.


## 4.1. The CDPLL(T) Algorithm

We describe here a certificate generation procedure that can be well adapted to the  DPLL(T) algorithm. The extension of DPLL(T) with certificate generation is called  CDPLL(T).Definition 8 (certificate refinement).
The certificate obtained by appending a certificate itemC to the end of the certificate P is denoted by P⊲C.We use a transition system to model the CDPLL(T) algorithm. Each state is represented as a 3-tuple “M∥F⊕P,” where M is the literal stack, F the clause set to be satisfied, and P the current certificate. The transition rules in CDPLL(T) are follows.(i)Decide:Precondition
(1)
l or ¬l occurs in a clause of F;
(2)
l is undefined in M,
(10)M∥F⊕P↦Mld∥F⊕P.(ii)UnitPropagate:Precondition
(1)
M
⊨
¬
C;
(2)
l is undefined in M,
(11)M∥F,C∨l⊕P↦Ml∥F,C∨l⊕P.(iii)TheoryPropagate:Precondition
(1)
M
⊨
T
l;
(2)
l or ¬l occurs in F;
(3)
l is undefined in M,
(12)M∥F⊕P↦Ml∥F⊕P.(iv)T-Backjump:Precondition
(1)
M
l
d
N
⊨
¬
C;
(2)
there exists a clauseC′∨l′ such that: (a) F,C⊨TC′∨l′ and M⊨¬C′, (b) l′ is undefined in M, and (c) l′ or ¬l′ occurs in F or in MldN;
(3)
R
=
{
C
1
,
C
2
,
…
,
C
n
} is a set of clause items such that: Ci∈⌊P⌋ for all i, and there exists a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to C′∨l′,
(13)MldN∥F,C⊕P↦Ml′∥F,C⊕(P⊲Res(R)).(v)T-Learn(I): this rule models the clause learning procedure.Precondition
(1)
Each atom ofC occurs in F or in M;
(2)
F
⊨
C;
(3)
R
=
{
C
1
,
C
2
,
…
,
C
n
} is a set of clause items such that: Ci∈⌊P⌋ for all i, and there exists a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to C,
(14)M∥F⊕P↦M∥F,C⊕(P⊲Res(R)).(vi)T-Learn(II): this rule models the learning of theory lemma.Precondition
(1)
Each atom ofC occurs in F or in M;
(2)
⊨
T
C,
(15)M∥F⊕P↦M∥F,C⊕(P⊲Lemma(C)).(vii)T-Forget:Precondition
F
⊨
T
C,
(16)M∥F,C⊕P↦M∥F⊕(P⊲Forget(C)).(viii)Restart:Precondition
T
(17)
M
∥
F
⊕
P
↦
∅
∥
F
⊕
P
.(ix)Fail:Precondition
(1)
M
⊨
¬
C;
(2)
M contains no decision literals;
(3)
R
=
{
C
1
,
C
2
,
…
,
C
n
} is a set of clause items such that: Ci∈⌊P⌋ for all i, and there exists a linear regular resolution from {⟦C1⟧,⟦C2⟧,…,⟦Cn⟧} to □,
(18)M∥F,C⊕P↦〈Fail〉⊕(P⊲Res(R)).The initial state isM∥F⊕P0 where P0 is the certificate that defines all initial clauses. When a final state 〈Fail〉⊕P is reached, P is the obtained certificate for the unsatisfiability judgment.The major differences between CDPLL(T) and DPLL(T) are as follows. (1) Certificate generation is added. Notice the modifications to rules T-Backjump, T-Learn, T-Forget, and T-Fail. (2) In order to generate well-formed certificates, the original T-Learn rule is split into 2 cases, one for the learning of resolvents (corresponds to clause learning) and the other for the learning of theory lemmas (corresponds to deductions in T). The first three rules are unchanged except the certificate part.


## 4.2. Implementation of CDPLL(T)

In a real implementation of CDPLL(T), additional information need to be collected to construct the certificate items. In this section, we discuss these details.Lemma 9.
For any reachable stateM∥F⊕P in CDPLL(T) and any clause C∈F, there exists a clause item D∈⌊P⌋ such that ⟦D⟧=C.Proof.
We prove that by induction. Initially, this property holds because all clauses inF0 are initial clauses and P0 consists of all initial clause items (by definition). At each valid transition step, the clause set F and the certificate P may be modified. However, each rule ensures that whenever a clause C is added to F, there is always a clause item D such that ⟦D⟧=C added to P, for example, in the rule T-Learn(I). Furthermore, whenever a clause item is removed from P, the corresponding clause is removed in F, for example, in the rule T-Forget. Thus, the property holds on all valid trace of CDPLL(T).


### 4.2.1. Record Reasons

For any literall in M, it is either added by the Decide rule or forced by a clause or theory lemma. For the latter case, we need to record a clause item which is a deduction of the lemma and from which the literal l can be enforced. We call this item the reason for literal l being in M.Only rulesUnitPropagate, TheoryPropagate, and T-Backjump can enforce new literal to M. We discuss in the following the reasons recorded by these three rules. (i)
UnitPropagate: the reason is a certificate item D such that ⟦D⟧=C∨l∈F. By Lemma 9, such item always exists.(ii)
TheoryPropagate: assume that M=l1∧l2∧⋯∧lm and M⊨Tl; then, the reason is a certificate item D such that ⟦D⟧=¬l1∨¬l2∨¬⋯∨¬lm∨l.(iii)
T-Backjump: the reason for l′ is a certificate item D such that ⟦D⟧=C′∨l′. We will show in the following that such certificate item always exists when T-Backjump is applicable.For convenience, a subscript is used to denote the reason, for example, l(D) denotes the literal l asserted by the reason ⟦D⟧.


### 4.2.2. Learn Clauses

In rulesT-Backjump and Fail, once there is a conflict, a backjump clause needs be learned. Furthermore, if there are some branches that have not been explored, T-Backjump is applied; otherwise, Fail is applied. Each clause learning procedure introduces some new certificate items.We use implication graph to analyze the clause learning process. Remember that in DPLL all literals are propositional atoms, the implication graph is simply a direct acyclic graph (DAG) where each edge corresponds to a deduction step. In CDPLL(T), the implication graph has two kinds of deductions: propositional deduction (which is similar to DPLL) and theory deduction. Each deduction step in the implication graph is labelled with a reason C. This graph can be viewed as a generalized implication graph. Without causing ambiguity, we still call it an implication graph.In the implication graph of DPLL, each cut containing the conflict literals corresponds to a learned clause (by resolving all the associated clauses of edges in this cut) [4]. No matter which criteria (e.g., 1-UIP) is used, the rule for clause learning is applicable. For CDPLL(T), when considering the generalized implication graphs, the clause learning rule is also applicable.There are two situations whereT-Backjump can be applied. Given a state M∥F⊕P, the first situation is that there exists a clause C∈F which is falsified by M, that is, ⊭M,C. Then, C is called the conflict clause. As in the rule, some backjump clause C′∨l′ should be learned by analyzing the conflict. Usually, C′∨l′ is a resolvent of a linear resolution. A certificate item with resolution type will be learned.The other situation is thatM itself becomes T-inconsistent. Then, a subset {l1,l2,…,lm} of M is unsatisfiable, that is, ⊨T¬l1∨¬l2∨⋯∨¬lm. This is also a conflict clause. It may not belong to F, but it can definitely be learned from F along with some theory lemmas. The fact that l1,…,lm leads to conflict is represented in the generalized implication graph. Furthermore, the clause C′∨l′ that is required by the rule T-Backjump can also be learned by generalized conflict clause analysis.In both situations, the backjump clauses are learned by clause learning. The certificate for unsatisfiability is actually a well-organized collection of these clause items. IfFail is applicable, no literal in M is decision variable; then, the learnt clause is the empty clause which shows F⊨T□.Example 10.
A generalized implication graph is shown in Figure2, where the literals are as follows: l0:x=y, l1:f(x)=f(y), and p is a propositional literal. Clauses are as follows:
(19)C0:¬l0∨¬l1:=¬(x=y)∨(f(x)=f(y)),C1:l0∨p:=x=y∨p,C2:l0∨¬p:=x=y∨¬p.Figure 2
Example of a generalized implication graph.Assume the current assignmentM=p,l0,¬l1. Then, there is a conflict between ¬l1 and l1. In all, there are 3 deductions in the implication graph: p→l0 forced by C2, l0→¬l1 by C0 and l0→l1 by the theory lemma C3. Among those reasons, solid lines correspond to existing clauses in F, while dashed lines correspond to theory lemmas. C3 is actually a theory lemma l0→l1(x=y→f(x)=f(y)).In the clause learning procedure, we start from the conflict(¬(l1∧¬l1)=¬l1∨l1) and trace back (apply a sequence of resolutions). If the 1st UIP schema [4] is used, it is possible to learn ¬p or ¬l0 (corresponds to cut1 and cut2, resp.). The resolution steps for learning ¬p are shown in Figure 3. Actually, ¬p is the resolvent of {C3,C0,C2} which are exactly the reasons labeled on the edges from the conflict to the cut. Among those, C0,C2 are normal clauses, and C3 is a theory lemma.Figure 3
Resolution steps for learning¬p.Based on the above discussions, the related rules can be interpreted more precisely as follows.(i)TheoryPropagate:
(20)M∥F⊕P↦Ml(C)∥F⊕P.
The precondition requires that M⊨Tl. Let M′ be a subset of M which entails l (possibly M′=M). Let C=¬M′∨l, then ⊨TC. Furthermore, M,C⊨Tl, which means C is a unit clause under the assignment M. Thus, C is the reason of l.(ii)UnitPropagate:
(21)M∥F,C∨l⊕P↦Ml(C∨l)∥F,C∨l⊕P.
The precondition requires that M⊨¬C; thus, C∨l is a unit clause under M. So, the reason of l is C∨l.(iii)T-Backjump:
(22)MldN∥F,C⊕P↦Ml′(C′∨l′)∥F,C⊕(P⊲Res(R)).
The precondition requires that there exits some clause C′∨l′ such that F,C⊨TC′∨l′ and M⊨¬C′. The clause C′∨l′ is then used as the reason for l′. As the clause learning is always applicable [9], this clause always exists. If the assignment MldN is T-consistent, then there must be some conflict clause C∈F. As explained above, the clause learning will then be applied, and the learned clause will be C′∨l′. On the other hand, when MldN is T-inconsistent, clause learning is also applicable in the generalized implication graph and generates a candidate C′∨l′. In both cases, C′∨l′ can be learned by applying linear regular resolutions on a clause set R [4]. Moreover, such R is the union of a subset of reasons in MldN and a group of theory lemmas.(iv)Fail:
(23)M∥F,C⊕P↦〈Fail〉⊕(P⊲Res(R)).
The Fail rule is similar to T-Backjump except that the learned clause is the empty clause.


## 4.2.1. Record Reasons

For any literall in M, it is either added by the Decide rule or forced by a clause or theory lemma. For the latter case, we need to record a clause item which is a deduction of the lemma and from which the literal l can be enforced. We call this item the reason for literal l being in M.Only rulesUnitPropagate, TheoryPropagate, and T-Backjump can enforce new literal to M. We discuss in the following the reasons recorded by these three rules. (i)
UnitPropagate: the reason is a certificate item D such that ⟦D⟧=C∨l∈F. By Lemma 9, such item always exists.(ii)
TheoryPropagate: assume that M=l1∧l2∧⋯∧lm and M⊨Tl; then, the reason is a certificate item D such that ⟦D⟧=¬l1∨¬l2∨¬⋯∨¬lm∨l.(iii)
T-Backjump: the reason for l′ is a certificate item D such that ⟦D⟧=C′∨l′. We will show in the following that such certificate item always exists when T-Backjump is applicable.For convenience, a subscript is used to denote the reason, for example, l(D) denotes the literal l asserted by the reason ⟦D⟧.


## 4.2.2. Learn Clauses

In rulesT-Backjump and Fail, once there is a conflict, a backjump clause needs be learned. Furthermore, if there are some branches that have not been explored, T-Backjump is applied; otherwise, Fail is applied. Each clause learning procedure introduces some new certificate items.We use implication graph to analyze the clause learning process. Remember that in DPLL all literals are propositional atoms, the implication graph is simply a direct acyclic graph (DAG) where each edge corresponds to a deduction step. In CDPLL(T), the implication graph has two kinds of deductions: propositional deduction (which is similar to DPLL) and theory deduction. Each deduction step in the implication graph is labelled with a reason C. This graph can be viewed as a generalized implication graph. Without causing ambiguity, we still call it an implication graph.In the implication graph of DPLL, each cut containing the conflict literals corresponds to a learned clause (by resolving all the associated clauses of edges in this cut) [4]. No matter which criteria (e.g., 1-UIP) is used, the rule for clause learning is applicable. For CDPLL(T), when considering the generalized implication graphs, the clause learning rule is also applicable.There are two situations whereT-Backjump can be applied. Given a state M∥F⊕P, the first situation is that there exists a clause C∈F which is falsified by M, that is, ⊭M,C. Then, C is called the conflict clause. As in the rule, some backjump clause C′∨l′ should be learned by analyzing the conflict. Usually, C′∨l′ is a resolvent of a linear resolution. A certificate item with resolution type will be learned.The other situation is thatM itself becomes T-inconsistent. Then, a subset {l1,l2,…,lm} of M is unsatisfiable, that is, ⊨T¬l1∨¬l2∨⋯∨¬lm. This is also a conflict clause. It may not belong to F, but it can definitely be learned from F along with some theory lemmas. The fact that l1,…,lm leads to conflict is represented in the generalized implication graph. Furthermore, the clause C′∨l′ that is required by the rule T-Backjump can also be learned by generalized conflict clause analysis.In both situations, the backjump clauses are learned by clause learning. The certificate for unsatisfiability is actually a well-organized collection of these clause items. IfFail is applicable, no literal in M is decision variable; then, the learnt clause is the empty clause which shows F⊨T□.Example 10.
A generalized implication graph is shown in Figure2, where the literals are as follows: l0:x=y, l1:f(x)=f(y), and p is a propositional literal. Clauses are as follows:
(19)C0:¬l0∨¬l1:=¬(x=y)∨(f(x)=f(y)),C1:l0∨p:=x=y∨p,C2:l0∨¬p:=x=y∨¬p.Figure 2
Example of a generalized implication graph.Assume the current assignmentM=p,l0,¬l1. Then, there is a conflict between ¬l1 and l1. In all, there are 3 deductions in the implication graph: p→l0 forced by C2, l0→¬l1 by C0 and l0→l1 by the theory lemma C3. Among those reasons, solid lines correspond to existing clauses in F, while dashed lines correspond to theory lemmas. C3 is actually a theory lemma l0→l1(x=y→f(x)=f(y)).In the clause learning procedure, we start from the conflict(¬(l1∧¬l1)=¬l1∨l1) and trace back (apply a sequence of resolutions). If the 1st UIP schema [4] is used, it is possible to learn ¬p or ¬l0 (corresponds to cut1 and cut2, resp.). The resolution steps for learning ¬p are shown in Figure 3. Actually, ¬p is the resolvent of {C3,C0,C2} which are exactly the reasons labeled on the edges from the conflict to the cut. Among those, C0,C2 are normal clauses, and C3 is a theory lemma.Figure 3
Resolution steps for learning¬p.Based on the above discussions, the related rules can be interpreted more precisely as follows.(i)TheoryPropagate:
(20)M∥F⊕P↦Ml(C)∥F⊕P.
The precondition requires that M⊨Tl. Let M′ be a subset of M which entails l (possibly M′=M). Let C=¬M′∨l, then ⊨TC. Furthermore, M,C⊨Tl, which means C is a unit clause under the assignment M. Thus, C is the reason of l.(ii)UnitPropagate:
(21)M∥F,C∨l⊕P↦Ml(C∨l)∥F,C∨l⊕P.
The precondition requires that M⊨¬C; thus, C∨l is a unit clause under M. So, the reason of l is C∨l.(iii)T-Backjump:
(22)MldN∥F,C⊕P↦Ml′(C′∨l′)∥F,C⊕(P⊲Res(R)).
The precondition requires that there exits some clause C′∨l′ such that F,C⊨TC′∨l′ and M⊨¬C′. The clause C′∨l′ is then used as the reason for l′. As the clause learning is always applicable [9], this clause always exists. If the assignment MldN is T-consistent, then there must be some conflict clause C∈F. As explained above, the clause learning will then be applied, and the learned clause will be C′∨l′. On the other hand, when MldN is T-inconsistent, clause learning is also applicable in the generalized implication graph and generates a candidate C′∨l′. In both cases, C′∨l′ can be learned by applying linear regular resolutions on a clause set R [4]. Moreover, such R is the union of a subset of reasons in MldN and a group of theory lemmas.(iv)Fail:
(23)M∥F,C⊕P↦〈Fail〉⊕(P⊲Res(R)).
The Fail rule is similar to T-Backjump except that the learned clause is the empty clause.


## 4.3. Properties of CDPLL(T)

The soundness and completeness of CDPLL(T) are proven in this subsection.Lemma 11.
A well-formed certificate modified byT-Backjump, T-Learn(I), T-Learn(II), Fail, or T-Forget is still well formed.Proof.
Each of the 4 rules appends a new item to the certificate. Assume that the certificateP is modified to P′=P⊲I where I is the appended certificate item. The well-formed property of P′ is checked by case studying the rules applied.(i)
ForT-Backjump: a certificate item of resolution type is appended. According to the precondition, the certificate items referred by I are already defined in ⌊P⌋. So, P′ is still well formed.(ii)
ForT-Learn(I): similar to the previous case. The dependency of appended certificate item is satisfied.(iii)
ForT-Learn(II): a theory lemma item C is appended. It is required that ⊨TC. Thus, P′ is still well formed.(iv)
ForFail: similar to the T-Backjump case.(v)
ForT-Forget: the rule requires that the forgotten clause is in the clause set. By Lemma 9, we know that there is a certificate item in P which defines C. Thus, the well formedness is ensured.With the help of this lemma, it can be proven that CDPLL(T) procedure always generates well-formed certificates.Lemma 12.
Given any reachable stateM∥F⊕P in any CDPLL(T) procedure, P is a well-formed certificate.Proof.
First of all, the initial certificateP0 is well formed because it only contains initial items. Secondly, the certificate is only modified in T-Backjump, T-Learn(I), T-Learn(II), Fail, and T-Forget. By Lemma 11, these rules will preserve well formedness. So, following any path of CDPLL(T) will always generate a well-formed certificate. That completes the proof.Theorem 13 (soundness).
Given a clause setF0, for any certificate P, if Mx∥Fx⊕Px is reachable in a CDPLL(T)  procedure, then Mx∥Fx is also reachable in a DPLL(T) procedure. Specially, if 〈Fail〉  ⊕P is reachable in CDPLL(T), then 〈Fail〉 is also reachable in DPLL(T).Proof.
For each transition step in CDPLL(T):
(24)M∥F⊕P⟶CDPLL(T)M′∥F′⊕P′,
it holds that
(25)M∥F⟶DPLL(T)M′∥F′.
So, given a CDPLL(T) trace, a trace in DPLL(T) can be obtained by removing the certificate part. If Mx∥Fx⊕Px is reachable in CDPLL(T) so is Mx∥Fx in DPLL(T).Theorem 14 (completeness).
Given a clause setF0, if the state Mx∥Fx is reachable in a DPLL(T) procedure, then there must be a certificate Px such that Mx∥Fx⊕Px is reachable in a DPLL(T) procedure. Furthermore, if 〈Fail〉 is reachable in a DPLL(T) procedure, then 〈Fail〉  ⊕Px is reachable in a CDPLL(T) and □∈⌊Px⌋.Proof.
For rulesDecide, TheoryPropagate, UnitPropagate, T-Learn(II), T-Forget, and Restart, the preconditions are equal to those in CDPLL(T). So, if there is a transition in DPLL(T)  labelled with one of these rules, there could also be the same transition in CDPLL(T).
For other rules,T-Backjump, T-Learn(I), and Fail, we need to prove that: if Mx∥Fx is reachable, then there is some certificate Px such that Mx∥Fx⊕Px is reachable. We prove that by induction. Initially, this condition holds because the initial state M0∥F0 corresponds to M0∥F0⊕P0. Inductively, if
(26)M∥F⟶DPLL(T)M′∥F′
is a possible transition in DPLL(T), and there is some P such that M∥F⊕P is reachable in CDPLL(T).  (i)
If it is labelled withT-Learn(I), because the learned clause is from clause learning, and clause learning corresponds to linear regular resolution. It is always possible that necessary theory lemmas in the implication graph are learned at first by Learn(II) and get to a state M∥F⊕P′′, on which the preconditions of Learn(I) are satisfied. Then, M′∥F′⊕P′ is reached.(ii)
If it is labelled withT-Backjump or Fail, the situation is similar.Our approach can be well adapted to any DPLL(T)-based SMT solver. It is sound and complete regardless of the theory learning scheme used or the order of the decision procedure. It works well as long as clause learning is based on the generalized implication graph.


## 4.4. Examples

A couple of examples are discussed in this subsection. The first example is given as a CNF formula on propositional variables. In this case, the SMT problem reduces to an SAT problem. No theory deduction is involved in this example; so, we can get a general idea of the structure of certificates.Example  1. Consider the following clause set:
(27)C1=¬l1∨¬l2∨¬l3,C2=¬l1∨¬l2∨l3,C3=¬l1∨l2,C4=l1∨¬l2,C5=l1∨l2.LetF0={C1,C2,C3,C4,C5}; assume that P0 defines everything in F0 as initial clause; then, a possible CDPLL(T) procedure is shown in Table 2, where “~” means this field is the same as that in the previous row.Table 2
The  CDPLL(T)  procedure for Example  1.
No.
M
∥
F
⊕
P
Reason
Explanation
1
∅
∥
F
0
⊕
P
0
∅
Initial state
2
l
1
d
∥
~
⊕~
∅
Decide
3
l
1
d
,
l
2
∥
~
⊕~
l
2
↦
C
3
UnitPropagate
4
l
1
d
,
l
2
,
¬
l
3
∥
~
⊕~
{
l
2
↦
C
3
¬
l
3
↦
C
1
UnitPropagate now C2 is falsified
5
¬
l
1
∥
{
F
0
C
6
=
¬
l
1
⊕
[
P
0
⊲
R
e
s
{
C
1
,
C
2
,
C
3
}
=
C
6
]
¬
l
1
↦
C
6
C
6
=
¬
l
1 is learned
T-Backjump
6
¬
l
1
,
¬
l
2
∥
~
⊕~
{
¬
l
1
↦
C
6
¬
l
2
↦
C
4
UnitPropagate
7
〈
Fail
〉
∥
~
⊕
[
P
0
⊲
R
e
s
{
C
1
,
C
2
,
C
3
}
=
C
6
R
e
s
{
C
4
,
C
5
,
C
6
}
=
□
]
∅
FailIn step 4,C2=¬l1∨¬l2∨l3 is falsified. By analysing the implication graph, a clause is learned from C1,C2,C3. Among the referred clauses, C2 is a falsified clause, and C1,C3 are in the reasons. In step 7, C4 is falsified, but there is no decision variable. By analysing the implication graph, we can find a resolution from C4,C5,C6 to the empty clause. Among the referred clauses, C4 is a falsified clause, and C5,C6 are in the reasons.Example  2. Consider the background theory TEUF and a clause set F containing the following:
(28)(C1)a=b∨g(a)≠g(b),(C2)h(a)≠h(c)∨p,(C3)g(a)=g(b)∨¬p,(C4)h(a)=h(c)∨a=c,(C5)f(a)≠f(b),(C6)b=c.
Its boolean structure is
(29)C1=l1∨¬l5,C2=¬l6∨p,C3=l5∨¬p,C4=l6∨l2,C5=¬l4,C6=l3,
where
(30)l1:a=b,l2:a=c,l3:b=c,l4:f(a)=f(b),l5:g(a)=g(b),l6:h(a)=h(c).A possible CDPLL(T) procedure is shown in Table 3, where the referred certificates are as follows:
(31)P1=[P0⊲Lemma(¬l1∨l4)=C7],P2=[P0⊲Lemma(¬l1∨l4)=C7Lemma(l2∧l3⟶l1)=C8],P3=[P0⊲Lemma(¬l1∨l4)=C7Lemma(l2∧l3⟶l1)=C8Res{C8,C7,C4,C6,C2,C3,C1}=□].Table 3
A possible  CDPLL(T)  procedure.
No.
M
∥
F
⊕
P
Reason
Explanation
1
∅
∥
F
0
⊕
P
0
∅
Initial state
2
¬
l
4
∥
~
⊕
~
¬
l
4
↦
C
5
UnitPropagation
3
¬
l
4
,
l
3
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
UnitPropagation
4
¬
l
4
,
l
3
,
l
1
d
∥
~
⊕~
~
Decide  M becomes T-inconsistent
5
~
∥
F
0
∪
{
C
7
}
⊕
P
1
~
T-Learn(II), C7 is learned
6
¬
l
4
,
l
3
,
¬
l
1
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
T-Backjump
7
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
UnitPropagation
8
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
,
¬
p
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
¬
p
↦
C
3
UnitPropagation
9
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
,
¬
p
,
¬
l
6
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
¬
p
↦
C
3
¬
l
6
↦
C
2
UnitPropagation
10
¬
l
4
,
l
3
,
¬
l
1
,
¬
l
5
,
¬
p
,
¬
l
6
,
l
2
∥
~
⊕~
{
¬
l
4
↦
C
5
l
3
↦
C
6
¬
l
1
↦
C
7
¬
l
5
↦
C
1
¬
p
↦
C
3
¬
l
6
↦
C
2
l
2
↦
C
4
UnitPropagation  M becomes T-inconsistent
11
~
∥
F
0
∪
{
C
7
,
C
8
}
⊕
P
2
~
T-Learn(II), C8 is learned
12
~
∥
F
0
∪
{
C
7
,
C
8
}
⊕
P
3
~
Fail, □ derivedIn step 4,M becomes T-inconsistent. The generalized implication graph is shown in Figure 4. A theory lemma C7=¬l1∨l4 is learned (instantiated the monotonicity property of the equality) firstly, then the backjump rule is applicable. In steps 11 and 12, M becomes T-inconsistent again. A theory lemma C8=l2∧l3→l1 is then learned (transitivity of equality), and then clause learning is performed which learns the empty clause. The implication graph is shown in Figure 5.Figure 4
The implication graph in step 4.Figure 5
The implication graph in steps 11 and 12.


## 5. The Certificate Checking

Lemma 15.
For any initial clause setF0, given a well-formed certificate P and 0≤i≤|P|, if P[i] is a certificate item that defines a clause, then F0⊨T⟦P[i]⟧.Proof.
We prove that by induction. The base case is easy to prove because for any initial itemP[i] that defines a clause, P[i]∈F0. Therefore, it is trivial that F0⊨⟦P[i]⟧. Thus, F0⊨T⟦P[i]⟧.  (i)
For resolution certificate items, assume thatP[i]=Res{C1,C2,…,Cn}. By definition, all Ci are all defined in ⌊P⌋i-1. Then by the inductive hypothesis, we know F0⊨T⟦Ci⟧. By the property of resolution, it is true that F0⊨T⟦P[i]⟧.(ii)
For theory lemma, it is true that⊨T⟦P[i]⟧. So, F0⊨T⟦P[i]⟧.Theorem 16.
Given a clause setF0, if a certificate P for F0 is well formed and □∈⌊P⌋, then F0 is unsatisfiable.Proof.
By Lemma15, we know that F0⊨T□ in this case.By Theorem16, certificate checking is actually checking whether the certificate is well formed and contains the empty clause. Checking the well formedness of a certificate can directly follow Definition 7. Only one traverse from the first item to the last one is needed. Moreover, the following properties make the checking process even easier.(i)
Only checking for theory lemma is performed in theoryT. Once a theory lemma is proved valid, it can be treated as a propositional clause.(ii)
For each individual proof rule, we have a dedicated checker to check if the theory lemma is an instance of the rule. In this way, the certificate checker is extensible. Given a new proof rule, we need only to add the corresponding lemma checker. Notice that each proof rule defines an atomic deduction step; the checking effort is much less than solving a constraint in the theoryT. For instance, only pattern matching is needed to check if a theory lemma is an instance of the monotonicity property of equality.


## 6. Experiments

Two criteria are adopted to assess our certificate approach: the overhead for generating certificates, and the cost for certificate checking. We implemented an SMT solveraCiNO based on the CDPLL(T) algorithm. It uses the Nelson-Oppen framework to solve combined theory. Currently, TEUF and TLRA are considered. The experiments are carried out on a machine with a E7200 dual core CPU (2.53 GHz per core) and 2.0 GB RAM.All test cases are taken from SMT-LIB [22]. Our approach is tested on 19 unsatisfiable instances from different folders (in order to test it on different kinds of problem instances). Experiment results are shown in Table 4.Table 4
Experiment results.
Case
Input
CDPLL (T)
Certificate
Checking
Lit
Clause
Learnt
Time
Lemmas
Res
Forget
Mem
Time
1
2
3
0
0.01 s
2
2
0
4
0.01 s
2
10
15
1
0.01 s
4
8
3
10
0.00 s
3
17
25
3
0.01 s
8
14
4
17
0.00 s
4
66
95
1069
0.08 s
1024
550
490
66
0.05 s
5
87
125
9537
0.71 s
8192
4146
4043
87
0.18 s
6
1157
2611
5197
1.39 s
22383
3711
2635
1051
0.23 s
7
1582
2173
16735
21.30 s
859886
8529
7438
1148
1.16 s
8
811
1037
5164
5.80 s
248159
4286
3580
555
0.41 s
9
4687
9433
759
1.00 s
1021
751
430
617
0.03 s
10
167
308
60
0.04 s
934
77
48
79
0.02 s
11
447
883
1464
0.53 s
15894
965
995
399
0.09 s
12
3930
6584
3046
2.22 s
8555
2468
1617
1639
0.14 s
13
3362
5154
2310
1.68 s
6204
1916
1251
1467
0.13 s
14
4615
7036
3244
3.71 s
9521
2308
1633
1776
0.13 s
15
2422
3726
828
0.43 s
587
616
509
428
0.03 s
16
5226
8614
9781
7.85 s
6305
3457
1723
2199
0.12 s
17
3073
4821
128729
87.65 s
74289
85711
84269
5899
5.16 s
18
2415
3710
2511
1.29 s
2165
1781
1377
1367
0.27 s
19
4151
6492
32991
21.26 s
26011
21015
20792
4497
1.24 sIn Table4, the first column-group describes the scale of the input problem. The input is transformed to its equivalent conjunctive normal form, and the number of literals and clauses are counted. In the CDPLL(T) procedure, once a closed branch is encountered, a new clause will be learned. The number of learned clauses is listed in the second column-group. This number is equal to that in DPLL(T) since certificate generation will not affect the search procedure of the SMT problem. As in the DPLL(T) algorithm, the number of clause learning can be quite large (e.g., the 17th case). The time used in CDPLL(T) is also presented. The third column-group summarises the generated certificates. It is obvious that the number of theory lemma items is usually very large. The column of “Forget” is the number of forget items that forgets an initial or resolution certificate item. All theory lemmas are eventually forgotten, these items are not counted here. For SMT problem, this is not surprising since the major work of SMT solvers is in reasoning in the background theory. The resources and time required to check the certificates are listed in the Checking column-group. All certificates are checked to be well formed. The “Mem” column is not the size of memory consumed but the maximal number of clause items that are stored in the memory during checking. Also, the time for certificate checking is listed besides.Regarding the certificate checking, the number of initial clauses and memory consumption is compared in Figure6. It is rather interesting that although the certificate itself could be exponentially large with respect to the input problem, the memory consumption will not grow in the same way. The reason is that we have explicitly forgotten many items. In particular, many theory lemma are referred locally. They are only available in a short period of time, after which they are forgotten. With the technique of forgetting items, the certificate checking becomes more efficient. This is also supported by data from the “Time” column in Table 4.Figure 6
Comparison between the number of initial clauses and memory usage.Towards the overhead of our approach, the experiment is shown in Table5. Tested cases are also from SMT-LIB. In order to suppress the inaccurate measurement of time, we intentionally selected time consuming cases (e.g., longer than 0.01 sec). The maximal overhead is about 27.33%, and the average overhead is about 10.5%. It is much smaller compared to other approaches [17, 21].Table 5
Overhead of our approach.
Test Case
With cert (sec.)
Without cert (sec.)
Overhead (%)
NEQ.NEQ004_size4.smt2
0.63
0.60
4.62
NEQ.NEQ004_size5.smt2
19.87
18.27
8.74
PEQ.PEQ002_size5.smt2
5.29
4.85
9.07
PEQ.PEQ020_size5.smt2
1.29
1.20
7.47
QG-classification.loops6.dead_dnd001.smt2
1.34
1.20
11.94
QG-classification.loops6.gensys_brn004.smt2
1.06
0.95
11.81
QG-classification.loops6.gensys_icl001.smt2
2.59
2.22
16.62
QG-classification.loops6.iso_brn005.smt2
0.18
0.14
27.33
QG-classification.loops6.iso_icl030.smt2
3.32
3.05
8.68
QG-classification.qg5.dead_dnd007.smt2
35.62
34.55
3.09
QG-classification.qg5.gensys_brn007.smt2
0.74
0.71
4.52
QG-classification.qg5.gensys_icl100.smt2
14.29
13.60
5.07
SEQ.SEQ004_size5.smt2
0.68
0.54
26.93
SEQ.SEQ050_size3.smt2
0.19
0.18
7.03


## 7. Conclusion

In this paper, a unified certificate framework for quantifier-free SMT instances was presented. The certificate format is simple, clean, and extensible to other background theories. The certificate generation procedure can be easily integrated to any DPLL(T)-based SMT solver. Soundness and completeness of the extension of DPLL(T) with the certificate generation procedure were established. Experimental results show that our certificate framework outperforms others in both certificate generation and certificate checking.



---

*Source: 964682-2013-05-23.xml*