Maria Paola Bonacina
email: mariapaola.bonacina@univr.it

Stéphane Graham-Lengrand

Natarajan Shankar
email: shankar@csl.sri.com

Proofs in Conflict-Driven Theory Combination *

Keywords: CCS Concepts, Theory of computation → Automated reasoning; Proof generation, Lemma learning, Theory combination, Satisfiability modulo assignment

Search-based satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflict-driven SMT-solving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.

Introduction

The satisfiability problem is one of checking if a given formula has a model. Propositional satisfiability (SAT) is the problem of finding an assignment of truth values to variables that satisfies the input propositional formula, typically given as a set of clauses. Many SAT solvers employ a conflict-driven search strategy, known as Conflict-Driven Clause Learning (CDCL), in which the solver extends a partial assignment until it satisfies the formula, or a conflict arises because the assignment falsifies the formula. Nontrivial inference steps are performed in response to a conflict to roll back the partial assignment and direct the search elsewhere [START_REF] João | Conflictdriven clause learning SAT solvers[END_REF]. This conflict-driven style inspired the design of several solvers for quantifier-free fragments of arithmetic [12, 19, 23-25, 29, 35, 36]. These conflict-driven theory solvers decide the satisfiability of sets of literals in the theory. The problem of deciding the satisfiability of sets of clauses in a theory is known as Satisfiability Modulo a Theory (SMT). MCSAT, for Model Constructing SATisfiability, is an approach to conflict-driven SMT [START_REF] De | A model-constructing satisfiability calculus[END_REF]. It integrates a CDCL-based SATsolver and a conflict-driven theory solver equipped with an inference system to detect and explain conflicts in the theory. In MCSAT, both Boolean and first-order variables are given assignments in a trail representing the candidate model as a partial assignment. First-order variables are assigned constant symbols representing individuals of the corresponding sort in a model's domain. For example, integer variables are assigned integer constants, and bit vector variables are assigned constant bit vectors. MCSAT allows the introduction of new (i.e., non-input) terms in lemmas as long as these terms are drawn from a finite basis. The MCSAT approach has been shown to be quite versatile and efficient [START_REF] Jovanović | Solving nonlinear integer arithmetic with MCSAT[END_REF][START_REF] Jovanović | The design and implementation of the model-constructing satisfiability calculus[END_REF][START_REF] Zeljić | Deciding bit-vector formulas with mcSAT[END_REF].

Most problems involve more than one theory, and MC-SAT is not a combination calculus in general. In prior work, we designed a method called Conflict-Driven SATisfiability (CDSAT) to solve in a conflict-driven manner satisfiability problems in a generic combination of disjoint theories [START_REF] Paola Bonacina | A model-constructing framework for theory combination[END_REF][START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF]. CDSAT combines multiple theory solvers, all or some of which are conflict-driven, into a conflict-driven solver for the union of the theories. More precisely, CDSAT combines theory inference systems, called theory modules: the only relevant component of a conflict-driven theory solver is its inference system, since the conflict-driven search is performed by CDSAT for all theories. A non-conflict-driven solver is abstracted into a theory module whose only inference rule invokes the solver to detect unsatisfiability in the theory.

In CDSAT, a common trail contains assignments to both Boolean and first-order terms. Some assignments are decisions, that is, guesses, and others are propagated because they are entailed by the formula and prior assignments in the trail. Theory modules work on this trail to detect conflicts with any theory-specific input formula. Conflict resolution rules work to roll back the trail to a prior decision level. The CDSAT transition system is sound, terminating, and complete, relative to the theory modules and a global finite basis for all theories. CDSAT generalizes CDCL, MCSAT, and the equality sharing (Nelson-Oppen) method for combination of theories [START_REF] Krstić | Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL[END_REF][START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF]: CDSAT reduces to CDCL, if propositional logic is the only theory, to MCSAT, if the combination features propositional logic and another theory with conflictdriven solver, and to equality sharing, if no theory in the combination has a conflict-driven solver [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF].

In this paper we extend CDSAT with lemma learning (Section 3) and proof generation (Sections 4 and 5). Lemmas are formulae entailed by the input formula. Learning lemmas from conflicts is a key feature of conflict-driven reasoning engines, because conflict-driven lemmatization immediately thwarts any attempt to repeat a failed search path (e.g., [START_REF] João | Conflictdriven clause learning SAT solvers[END_REF]). Proof generating inference systems [START_REF] Shankar | Inference Systems for Logical Algorithms[END_REF] are important because for many applications a yes/no answer is not enough, and solvers are expected to generate either a satisfying assignment or a proof of unsatisfiability. For instance, proofs are useful for extracting interpolants (see [START_REF] De | Interpolation systems for ground proofs in automated deduction: a survey[END_REF] for a survey) to refine abstractions [START_REF] Henzinger | Abstractions from proofs[END_REF] or generate invariants [START_REF] Chadha | On the mechanical derivation of loop invariants[END_REF].

CDCL-based SAT solvers generate proofs by propositional resolution [START_REF] Zhang | Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications[END_REF]. Reasoners based on the DPLL(T ) paradigm [START_REF] Barrett | Splitting on demand in SAT modulo theories[END_REF][START_REF] Maria | On deciding satisfiability by theorem proving with speculative inferences[END_REF][START_REF] Krstić | Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL[END_REF][START_REF] Nieuwenhuis | Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T)[END_REF] generate proofs by propositional resolution with proofs of theory lemmas plugged in as external subproofs (see [START_REF] De | Interpolation systems for ground proofs in automated deduction: a survey[END_REF], Section 2.4). This structure reflects a hierarchy where propositional logic is at the center and the theories are satellites. In DPLL(T ) only propositional reasoning is conflictdriven, and non-conflict-driven theory solvers are integrated as black-boxes, so that their proofs also are black-boxes. In CDSAT, propositional logic and the SAT-solver lose their centrality as the sole conflict-driven component. Although propositional logic retains a special role, as all propagated assignments are Boolean, propositional logic is regarded as one of the theories, and all theory modules contribute directly to the proof, including new terms that may appear on the trail whence in the proof. For all these reasons, CD-SAT proofs do not fit in the known mold of DPLL(T ) proofs, and their generation requires machinery that goes beyond propositional resolution plus theory lemmas.

We present two approaches to proof generation in CDSAT. The first one is a proof-carrying CDSAT transition system (Section 4), where proof terms record the information needed to generate proofs. We describe different ways to turn proof terms into proofs (Section 5), including producing resolution proofs with theory lemmas. The proof objects produced by proof-carrying CDSAT can be directly checked by a verified checker [START_REF] Shankar | Trust and automation in verification tools[END_REF] or exported to a proof format that can be verified by proof checkers. Thus, proof-carrying CDSAT can slot into pipelines from proof-search to proof-checking [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF][START_REF] Christian Blanchette | Extending Sledgehammer with SMT solvers[END_REF][START_REF] Böhme | Fast LCF-style proof reconstruction for Z3[END_REF], where a minimal amount of proof information (e.g., an unsatisfiable core) might be sufficient for a theorem prover to regenerate a proof in its own format. The second approach consists of specifying a small kernel of primitives in LCF style [START_REF] Gordon | Edinburgh LCF: a mechanized logic of computation[END_REF][START_REF] Milner | LCF: A Way of Doing Proofs with a Machine[END_REF], as already explored in the Psyche prover [START_REF] Graham-Lengrand | Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture[END_REF], so that building proof objects in memory can be avoided. If CDSAT is implemented on top of this kernel, the LCF type abstraction ensures that an unsat answer is correct by construction, and CDSAT can be used as a trusted external oracle for interactive proof tools.

Background on CDSAT

CDSAT is an engine to determine the satisfiability of a quantifier-free formula modulo a combination of theories (SMT) and possibly modulo an initial assignment of values to some first-order variables or terms that appear in the formula. We call this generalization of SMT satisfiability modulo assignment (SMA). CDSAT combines in a conflict-driven manner inference systems, called theory modules, for component theories T 1 , . . . , T n . The component theories are required to be disjoint so that their signatures Σ 1 , . . . , Σ n share neither predicate nor function symbols, except equality, which is present in all signatures and for all sorts. In addition to equality, the theories typically share sorts and constant symbols.

Let T ∞ be the union of T 1 , . . . ,

T n . If Σ k =(S k , F k )
, where S k is the set of sorts and F k is the set of symbols, for all k,

1 ≤ k ≤ n, the signature of T ∞ is given by Σ ∞ =(S ∞ , F ∞ ), with S ∞ = n k =1 S k and F ∞ = n k =1 F k .
For most problems, one of the component theories is propositional logic, or the theory of Booleans, with logical connectives such as ∧, ∨, and ¬ as function symbols. For deciding the satisfiability of a set of literals in one or more convex theories (see [START_REF] De | Interpolation systems for ground proofs in automated deduction: a survey[END_REF] Definition 14, from [START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF] page 252), propositional logic is not needed as a component theory. If there is a non-convex theory (e.g., arrays), disjunction and therefore propositional reasoning are needed. Regardless of whether propositional logic is included, all theories T 1 , . . . , T n must be able to interpret the truth values true and false and therefore their signatures are required to have the sort prop = {true, false}, where prop comes from proposition. Then, formulae are terms of sort prop. We use l for formulae and t and u for terms of any sort.

CDSAT and theory modules manipulate assignments. An input problem {l 1 , . . . , l m }, where l 1 , . . . , l m are formulae, is seen as an initial assignment {l 1 ←true, . . . , l m ←true}, even when abbreviated as {l 1 , . . . , l m }. Assignments, including initial assignments, are not restricted to assigning truth values; they can assign values of any sort. For example, with propositional logic, a fragment of arithmetic, and the theory of arrays, (x > 1)←false, (x > 1) ∨ (y < 0)←true, y←-1, z← √ 2, (store(a, i, v) ≃ b)←true, select(a, j)←3, and (select(a, j) ≃ v)←true are all assignments. An assignment that assigns only values of sort prop is called Boolean. A singleton assignment that is not Boolean is called a first-order assignment, as it assigns a value to a first-order term. If the input problem is an SMT problem, it is given to CDSAT as a Boolean assignment; if it is an SMA problem, it may also include first-order assignments.

First-order assignments are a standard ingredient in the definition of a first-order model. However, in automated reasoning, models need to be represented syntactically. Firstorder assignments raise the issue of what is a value that can be assigned. The notion of using ground terms to represent individuals in a model's domain and assigning ground terms to first-order variables does not suffice for assignments such as select(a, j)←3, where a term gets a value, or z← √ 2, where √ 2 may not be a ground term in the given signature of arithmetic. A standard solution is to extend the signature with constant symbols that name all individuals in the domain of the intended model (e.g., the appropriate set of numerals for a fragment of arithmetic). Therefore, we introduce for each theory

T k , 1 ≤ k ≤ n, a conservative extension T + k with signa- ture Σ + k = (S k , F + k )
, where F + k adds to F k a possibly empty set of new constant symbols, called T + k -values, accompanied by new axioms as needed (e.g.,

√

2 with

√ 2 • √ 2 ≃ 2)
. For numerals, as for true and false, a T + k -value is both the domain element and the constant symbol that names it. F + k may be infinite, but it is countable (e.g., using the algebraic reals as real numbers), and only a finite subset of it will be used in any finite derivation. We use symbols such as c, q for T + k -values reserving b for true or false.

The union of T + 1 , . . . ,

T + n is an extension T + ∞ of T ∞ , with signature Σ + ∞ = (S ∞ , F + ∞ ) for F + ∞ = n k =1 F + k .
We assume that the extended theories are still disjoint except for the Boolean values true and false. Conservativity of an extension means that T + k -unsatisfiability implies T k -unsatisfiability for formulae in the original signature Σ k , so that the problem does not change: if CDSAT detects T + k -unsatisfiability, the problem is T k -unsatisfiable; if the problem is T k -satisfiable, there is a T + k -model that CDSAT can discover. Definition 2.1 (Assignment). Given a theory T with signature Σ and extension T + , a T -assignment is a set of pairs t←c, where t is a term and c a T + -value of the same sort.

We use J for generic T -assignments, A for singleton ones, and L or K for Boolean singletons. We abbreviate l←true as l, l←false as l, and t ≃ s u ←false as t s u, where s is the sort of t and u, that can be omitted when clear from context. The flip L of L assigns to the same formula the opposite Boolean value. We use H and E for T ∞ -assignments, that we call assignments for short. Note that replacing a first-order assignment t←c by (t ≃ c) ← true would blur the distinction between terms, on the left of an assignment, and values, on the right of an assignment.

Since assignments are not formulae, the notion of endorsement was introduced to relate assignments and models (see [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Section 6.3). For the purposes of this paper, it suffices to say that a T + ∞ -model M endorses an assignment H if (1) for every pair (t←c) in H , M satisfies the Σ + ∞ -formula t ≃ c; and (2) M interprets any two distinct values appearing in H as two distinct elements. 1 In the sequel we write H |= L to state that every T + ∞ -model endorsing H also endorses L. With a slight abuse of notation and terminology, if no T + ∞ -model endorses H , we write H |= ⊥ and say that H is unsatisfiable. Since the objective of this paper is proof generation, we are interested in the situation where CDSAT determines that the initial assignment is unsatisfiable.

In CDSAT, a theory module is an inference system for theory T k , 1 ≤ k ≤ n. Its inferences have the form J⊢ ⊢ ⊢ k L where J is a T k -assignment and L is a Boolean assignment. Theory modules are required to be sound: if J⊢ ⊢ ⊢ k L then every model endorsing J endorses L, so that J |= L.

A CDSAT-derivation transforms a state consisting of a trail Γ. A trail is a sequence of distinct singleton assignments that are either decisions, denoted ? A, or justified assignments, denoted H ⊢ A. A decision is written ? A because it is generally a guess. The justification H in H ⊢ A is a set of singleton assignments that appear before A in the trail. A theory inference J⊢ ⊢ ⊢ k L for some k, 1 ≤ k ≤ n, can justify adding J ⊢ L to the trail. Initial assignments are treated as justified assignments with empty justification, so that a derivation for the input problem {A 1 , . . . , A m } starts with the trail ∅ ⊢ A 1 , . . . , ∅ ⊢ A m . Justified assignments that are neither due to theory inferences nor initial assignments will be placed on the trail by conflictsolving transitions. Every assignment on the trail has an identifier. A trail can be used as an assignment by ignoring order, justifications, and identifiers, and as an assignment with identifiers by ignoring order and justifications. Definition 2.2 (Level). Given a trail Γ with assignments A 0 , . . . , A m , the level of a singleton assignment

A i , 0 ≤ i ≤ m, is given by level Γ (A i ) = 1 + max{level Γ (A j ) | j < i}, if A i is a decision, and level Γ (A i ) = level Γ (H ), if A i is a justified assignment with justification H . The level of a set of singleton assignments H ⊆ Γ is given by level Γ (H ) = 0, if H = ∅, and level Γ (H ) = max{level Γ (A) | A ∈ H }, otherwise.

Search rules Decide

Γ -→ Γ, ? A if A is a T k -assignment for a term that is T k -relevant for Γ, and A is acceptable for the T k -module and its view of Γ, with 1 ≤ k ≤ n The next three rules share the conditions: J ⊆ Γ, (J⊢ ⊢ ⊢ k L), and L Γ, for some k,

1 ≤ k ≤ n. Deduce Γ -→ Γ, J ⊢ L if L Γ and L is in B Fail Γ -→ unsat if L ∈ Γ and level Γ (J ∪ {L}) = 0 ConflictSolve Γ -→ Γ ′ if L ∈ Γ, level Γ (J ∪ {L}) > 0, and ⟨Γ; J ∪ {L}⟩ =⇒ * Γ ′ Conflict resolution rules Undo ⟨Γ; E ⊎ {A}⟩ =⇒ Γ ≤m-1 if A is a first-order decision of level m > level Γ (E) Resolve ⟨Γ; E ⊎ {A}⟩ =⇒ ⟨Γ; E ∪ H ⟩ if H ⊢ A is in Γ and H does not contain a first-order decision A ′ whose level is level Γ (E ⊎ {A}) UndoDecide ⟨Γ; E ⊎ {L}⟩ =⇒ Γ ≤m-1 , ? L if H ⊢ L is in Γ, m = level Γ (E) = level Γ (L)
and H contains a first-order decision

A ′ of level m LearnBackjump ⟨Γ; E ⊎ H ⟩ =⇒ Γ ≤m , E ⊢ L if L is a clausal form of H and is in B, L Γ, L Γ, and level Γ (E) ≤ m < level Γ (H )
Figure 1. The CDSAT transition system with lemma learning An assignment of level m may be added after one of level r , r > m; Γ ≤m denotes the restriction of Γ to its elements of level at most m. The rules of the CDSAT transition system comprise search rules, whose application is denoted by -→, and conflict resolution rules, whose application is denoted by =⇒, with transitive closure =⇒ * (see Fig. 1). The CD-SAT rules may place on the trail assignments for new terms, meaning terms that do not appear in the input. For termination, these terms must come from a finite set B of terms, called global basis (cf. [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Section 6.2). B is a parameter of the CDSAT transition system, whose instantiation depends on the input problem. The distinction between terms and T + -values plays a role here, as terms come from B and T +values come from F + ∞ : B is finite and fixed once the input is given and throughout the derivation, whereas F + ∞ may be an infinite supply out of which a derivation uses a finite subset that is not fixed prior to the start of the derivation. An assignment H is in B if t ∈ B for all t such that (t←c) ∈ H .

Rule Decide adds to the trail Γ a singleton assignment that is a decision, provided the term is relevant for a theory and the assignment acceptable for the theory module. Relevance (see [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Definition 4) organizes the division of labor among theories. Acceptability (see [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Definition 3) prevents adding an assignment that is already in Γ or that is so immediately inconsistent with Γ that it would have to be withdrawn without learning anything, such as adding L if L is in Γ or 1 ← 3 in arithmetic with 1 a constant symbol in F ∞ . Acceptability and relevance also imply that A is in B, which is relevant for termination [START_REF] Paola Bonacina | A model-constructing framework for theory combination[END_REF][START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF]. Rule Deduce extends Γ with a Boolean singleton assignment justified by a theory inference J⊢ ⊢ ⊢ k L from assignments J already in Γ. The system proceeds with decisions and deductions until a conflict arises, as J⊢ ⊢ ⊢ k L, for some k, 1 ≤ k ≤ n, and L ∈ Γ: the assignment J ∪ {L} is a conflict, because it is unsatisfiable. If the conflict is at level 0, rule Fail reports unsatisfiability. If the conflict is at a level greater than 0, rule ConflictSolve passes the control to the conflict resolution rules, and resumes the search from the trail Γ ′ resulting from solving the conflict.

The conflict resolution rules operate on a trail and a conflict that is an unsatisfiable set of assignments from the trail. These rules transform the conflict until either it is solved or it surfaces at level 0 so that Fail fires. The rules use the notation ⊎ for disjoint set union. Rule Undo applies if the conflict includes a first-order decision A whose level m is greater than that of any other element in the conflict: the effect of the rule is to exit the conflict by jumping back to level m -1, removing A and all its consequences from the trail. While it may seem that the resulting trail was already encountered, jeopardising termination, this is not the case [START_REF] Paola Bonacina | A model-constructing framework for theory combination[END_REF]. Acceptability ensures that A did not cause an inconsistency right away when it was added to the trail. If A is now part of a conflict, it means that some justified assignment L was added to the trail after decision A even if level Γ (L) < m (late propagation). Thus, Γ ≤m-1 is new because it contains L.

Rule Resolve explains the conflict, by replacing a justified assignment A with its justification H , unless H contains a first-order decision A ′ whose level m is that of the current conflict. In that case, using Resolve to replace A by its justification H is forbidden, and it can be shown that A must be a Boolean assignment L also of level m so that another rule applies [START_REF] Paola Bonacina | A model-constructing framework for theory combination[END_REF]. Indeed, if an assignment other than L in the conflict has level m, rule UndoDecide undoes A ′ and replaces it by a Boolean decision on L. If only one of the assignments in the conflict has the same level as the conflict, then the conflict is solved by a Backjump rule [START_REF] Paola Bonacina | A model-constructing framework for theory combination[END_REF][START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], replaced here with LearnBackjump to add learning as illustrated in Section 3.

The CDSAT transition system is non-deterministic as the rules leave room for heuristic choices. Thus, there are multiple CDSAT-derivations from a given input problem. In order to get a CDSAT procedure that yields a unique CDSATderivation from a given input, the transition rules must be coupled with a search plan that drives their application.

CDSAT with Lemma Learning

In order to enrich the CDSAT transition system with lemma learning, we turn assignments into clauses that the system can learn. First, we do this only for assignments that partake in conflicts, because in a conflict-driven system learning is also conflict-driven [START_REF] João | Conflictdriven clause learning SAT solvers[END_REF]. Second, only Boolean assignments can be turned into clauses. Third, in order to write non-unit clauses, we need disjunction. If propositional logic is not one of the combined theories, disjunction is not in the combined signature, and the only assignments that can yield clauses are singleton Boolean assignments that yield unit clauses. If propositional logic is one of the combined theories, any Boolean assignment can yield a clause.

Suppose that E ⊎ H is a conflict, where H contains only Boolean assignments. This means that E ⊎ H |=⊥. If H is a singleton L, we have E ⊎ {L} |=⊥, hence E |= L, and the flip L is the clause associated to assignment L in the conflict. If H is not a singleton, it can be rewritten as the singleton (( (l ←true)∈H l) ∧ ( (l ←false)∈H ¬l))←true that can be flipped into (( (l ←true)∈H l) ∧ ( (l ←false)∈H ¬l))←false.

In order to get a clause, the above assignment can be rewritten in the equivalent form (( (l ←true)∈H ¬l) ∨ ( (l ←false)∈H l))←true leading to the next definition. Definition 3.1 (Clausal form of an assignment in a conflict). Given a conflict E ⊎ H , where H is a Boolean assignment, the singleton Boolean assignments (( (l ←true)∈H ¬l) ∨ ( (l ←false)∈H l))←true (( (l ←true)∈H l) ∧ ( (l ←false)∈H ¬l))←false are clausal forms of H .

We now describe the new rule LearnBackjump, listed last in Fig. 1 Example 3.2. Consider the conflict on the last line of Fig. 2. Assume that LearnBackjump is applied with H = {l 2 , l 4 }, E = {(¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 )}, where ((¬l 2 ∨¬l 4 ) ← true) is a clausal form of H . We have level Γ (H ) = 4 and level Γ (E) = 0, so that any destination level m such that 0 ≤ m < 4 can be picked. A standard choice for m would be the second highest level in the conflict, namely m = 2, in which case the LearnBackjump step jumps over decision A 3 and yields Γ 0 , ? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢ (¬l 2 ∨¬l 4 ).

The derivation continues from level 2 with the learned lemma ¬l 2 ∨¬l 4 added to level 0.

We consider next learning and restart. It is common to restart after learning a clause, and search plans with aggressive restart proved successful in SAT solving. LearnBackjump makes this kind of search plan possible in CDSAT. Assume that the destination level m is chosen to be the smallest, that is, m = level Γ (E). If level Γ (E) is 0, the shape of the trail after LearnBackjump is Γ ≤0 , E ⊢ L, which means LearnBackjump performs a restart and adds E ⊢ L to level 0. as all decisions are undone and the derivation restarts with the learned lemma ¬l 2 ∨¬l 4 added to level 0.

In the rest of this section we analyze how LearnBackjump subsumes Backjump [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF] and allows CDSAT to learn assertion clauses. The Backjump rule applies when CDSAT reaches a conflict state ⟨Γ; E ⊎ {L}⟩, where level Γ (L) > m, with m = level Γ (E). Backjump solves such a conflict by producing Γ ≤m , E ⊢ L. In words, it jumps back to level m and adds to the trail the justified assignment E ⊢ L, because E ⊎ {L} |=⊥ yields E |= L. Rule LearnBackjump can behave in the same way by taking as H a singleton L. Indeed, L is a clausal form of any singleton Boolean assignment L in the conflict. However, even when it reproduces Backjump, LearnBackjump allows a choice of destination level: Backjump goes back to level m = level Γ (E), while LearnBackjump allows the system to go back to any level m such that level Γ (E) ≤ m < level Γ (L).

Example 3.4. The conflict on the last line of Fig. 2 contains an assignment, namely l 4 , whose level is greater than that of the rest of the assignment, as level Γ (l 4 ) = 4 > level Γ (E) = 2 where E = {(¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , (¬l 4 ∨l 5 )}. Thus, Backjump could apply and we can see how LearnBackjump mimics it. A LearnBackjump step with H = {l 4 } and m = 2 yields

Γ 0 , ? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , (¬l 4 ∨l 5 ) ⊢ l 4 . Alternatively, if m = 3, LearnBackjump yields Γ 0 , ? A 1 , ? l 2 , ? A 3 , (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , (¬l 4 ∨l 5 ) ⊢ l 4 .
The side-condition L Γ of LearnBackjump prevents adding to the trail clauses that are already there. Unlike Backjump, LearnBackjump does not require the occurrence in the conflict of a singleton assignment L of level greater than the rest of the conflict.

Example 3.6. In the first conflict in Fig. 2 both l 4 and l 5 have level 4. If we apply LearnBackjump with

H = {l 4 , l 5 }, E = {(¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 }, level Γ (H ) = 4, level Γ (E) = 2, and destination level m = 2, the resulting trail is Γ 0 , ? A 1 , ? l 2 , E ⊢ ¬l 4 ∨¬l 5
where (¬l 4 ∨ ¬l 5 ) ← true on level 2 is a clausal form of H .

The last conflict clause generated prior to backjumping is called backjump clause: the system learns this clause and jumps back to a prior level in such a way to undo at least one decision and satisfy the learned clause by placing on the trail one of its literals. The First Unique Implication Point (1UIP) heuristic [START_REF] João | GRASP: A search algorithm for propositional satisfiability[END_REF] picks as the backjump clause the first generated assertion clause, where an assertion clause is a conflict clause where only one of its literals, say l, is falsified at the current level. The Backjump rule of CDSAT generalizes this principle, because it applies when the conflict contains a singleton assignment L of level greater than the rest of the conflict (not necessarily the current one). However, Backjump places L on the trail without learning an assertion clause. When a CDSAT conflict contains a singleton assignment L of level greater than the rest of the conflict, it means it is possible to extract from the conflict an assertion clause. Thus, with rule LearnBackjump, CDSAT can learn assertion clauses, and a CDSAT search plan may choose to restrict the application of this rule to 1UIP conflict clauses.

Let κ = l 1 ∨• • •∨l q be an assertion clause that is in the global basis B. Let l q be the literal of κ made false by the current level and L the assignment that makes l q false. In order to learn κ, it suffices to identify the Boolean part H = H ′ ⊎{L} of the conflict that makes κ false: for all i, 1≤i≤q, (l i ← true) ∈ H if and only if ¬l i ∈ κ and (l i ← false) ∈ H if and only if l i ∈ κ. By Definition 3.1, the assignment K = (κ←true) is a clausal form of H . Let E be the rest of the conflict. Then the system applies LearnBackjump with destination level

m = level Γ (E ⊎H ′ ), which means m = level Γ (E) if level Γ (E) > level Γ (H ′ ), m = level Γ (H ′ ) if level Γ (H ′ ) > level Γ (E), and m = level Γ (H ′ ) = level Γ (E) if level Γ (H ′ ) = level Γ (E). This choice satisfies the condition level Γ (E) ≤ m < level Γ (H ), because level Γ (E) ≤ level Γ (E ⊎ H ′ ) < level Γ (H ) = level Γ (L). This LearnBackjump step yields the trail Γ ≤m , E ⊢ K,
and κ is learned. The theory module for propositional logic features inference rules for unit propagation (cf. [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Section 4.1) that allow the inference:

{K } ⊎ H ′ ⊢ ⊢ ⊢ Bool L. (1)
Indeed, K is (l 1 ∨ . . . ∨ l q-1 ∨ l q ) ← true, and H ′ makes l 1 , . . . , l q-1 false, so that unit propagation infers l q . Since L makes l q false, L makes l q true. Because the destination level m of the LearnBackjump step was chosen in such a way that m ≥ level Γ (H ′ ), the premises K, H ′ of inference (1) are all on the trail Γ ≤m , E ⊢ K. Furthermore, literal l q is in B, since L was on the trail. Thus, all conditions are met to apply a Deduce step with inference (1). The resulting trail is CDSAT with lemma learning inherits the soundness, completeness, and termination properties of CDSAT, under suitable assumptions on theory modules and the input-dependent global basis B (see [START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Section 6, and [START_REF] Paola Bonacina | A model-constructing framework for theory combination[END_REF], Sections 8 and 9). Intuitively, B needs to be finite for termination, and sufficiently large for completeness. Informally speaking, the latter means that B contains all input terms and all terms that the theory modules may need, as defined by n local basis for the combined theories T 1 , . . . , T n . Such a global basis is called stable. The theory modules need to be complete, which means that when none of them can extend the trail, the assignment on the trail is endorsed by a T + ∞ -model. Theorem 3.8. CDSAT with lemma learning is sound (if it derives unsat, the input problem is unsatisfiable), complete (if the theory modules are complete, and the global basis is stable, whenever the derivation reaches a state other than unsat such that no transition rule applies, there exists a model that endorses the input problem), and terminating (every derivation with a finite global basis is guaranteed to terminate).

Γ ≤m , E ⊢ K, {K }⊎H ′ ⊢ L which is similar to the Γ ≤m , E⊎H ′ ⊢ L produced
We leave for future work the performance analysis of different ways to apply LearnBackjump, focusing next on proof generation.

Proof Object Production in CDSAT

In this section we describe the first technique to endow CD-SAT with proof generation. This technique enables the system to build proof objects in memory. When a CDSAT derivation terminates by firing rule Fail and detecting unsatisfiability, the system engages in an activity called proof reconstruction [START_REF] Paola | On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method[END_REF], which consists of extracting a proof object from the final state of the derivation. For this, we need to instrument the transition system in such a way that the final state contains enough information to reconstruct a proof object.

Theory-Specific Proofs

Because CDSAT combines theory modules, proof object production in CDSAT requires proof object production in every theory module. Therefore, we assume that each theory module is equipped with a proof annotation system that annotates theory inferences with theory proofs:

J ⊢ ⊢ ⊢ k j k : L means that the module for theory T k infers L from J with theory proof j k . A theory proof refers to L and the individual assignments in J by means of identifiers: in J ⊢ ⊢ ⊢ k j k : L, the premise J is a T k -assignment with identifiers, that is, a set of triples a (t←c), where a is the identifier of the singleton T k -assignment t←c.

For instance, inference (1) from Section 3, representing Unit Propagation (UP) in the theory module for propositional logic, can be annotated with a theory proof denoted UP(a, {a 1 , . . . , a n }), as follows:

{ a K } ⊎ H ′ ⊢ ⊢ ⊢ Bool UP(a,
⊢ ⊢ ⊢refl : t ≃ t a (t 1 ≃ t 2 ) ⊢ ⊢ ⊢sym(a) : t 2 ≃ t 1 a 1 (t 1 ≃ t 2 ), a 2 (t 2 ≃ t 3 ) ⊢ ⊢ ⊢trans(a 1 , a 2 ) : t 1 ≃ t 3
a 1 (e 1 ≤ t), a 2 (t ≤ e 2 ) ⊢ ⊢ ⊢ LRA FM(a 1 , a 2 ) : (e 1 ≤ e 2 )
where t, e 1 , and e 2 are rational terms, and evaluation a 1 (x 1 ←q 1 ), . . . , a m (x m ←q m ) ⊢ ⊢ ⊢ LRA eval({a 1 , . . . , a m }) : l←b where formula l evaluates to the Boolean b given the firstorder assignments x 1 ←q 1 , . . . , x m ←q m for rational variables.

For Equality with Uninterpreted Functions (EUF), if J is a 1 (t 1 ≃ u 1 ), . . . , a m (t m ≃ u m ), a congruence inference is:

J ⊢ ⊢ ⊢ EUF Cong(a 1 , . . . , a m ) : f (t 1 , . . . , t m ) ≃ f (u 1 , . . . , u m ).
Theory modules to be combined in CDSAT are required to contain basic inference rules for equality. This means that theory modules must provide theory proofs refl, sym(a), trans(a 1 , a 2 ), eq(a 1 , a 2 ), neq(a 1 , a 2 ), that annotate equality inferences, as illustrated in Fig. 3.

If an assignment appears on the trail, its identifier in any theory proof is the same as its identifier on the trail. For example, when a Deduce step uses a theory inference J ⊢ ⊢ ⊢ k j k : L, the assignments in J appear on the trail Γ, and their identifiers in j k are the same as in Γ. However, since identifiers are mere names, theory proof annotations are stable under permutations of identifiers: any permutation π of identifiers transforms a theory proof j k into a theory proof π (j k ), such that, if a 1 (t

1 ←c 1 ), . . . , a m (t m ←c m ) ⊢ ⊢ ⊢ k j k : L then π (a 1 ) (t 1 ←c 1 ), . . . , π (a m ) (t m ←c m ) ⊢ ⊢ ⊢ k π (j k ) : L. Example 4.1. If we have 1 (x←c 1 ), 4 (y←c 1 ) ⊢ ⊢ ⊢ k eq(1, 4) : f (x) ≃ f (y), π (1)
= 4, and π (4) = 1, then we also have 4 (x←c 1 ), 1 (y←c 1 ) ⊢ ⊢ ⊢ k eq(4, 1) : f (x) ≃ f (y).

The assumption that every theory module has a proof annotation system is no restriction, as the proof annotation system can be a trivial one that uses a dummy theory proof for all theory inferences. The resulting theory proofs convey no information, which is acceptable if there are no requirements on the information they should offer.

Proof Terms

In order to empower CDSAT to generate proof objects, we instrument the CDSAT transition system to keep track of provability invariants. We call the outcome proof-carrying CDSAT. The provability invariants of a transition system ensure that the transitions do not change the problem. If

A is initial ∅ ⊢ ⊢ ⊢in(A) : A J ⊢ ⊢ ⊢ k j k : L J ⊢ ⊢ ⊢j k : L E ⊎ H ⊢ ⊢ ⊢c : ⊥ L is a clausal form of H E ⊢ ⊢ ⊢lem(H .c) : L J ⊢ ⊢ ⊢ k j k : L J ∪ { a L} ⊢ ⊢ ⊢cfl(j k , a) : ⊥ H ⊢ ⊢ ⊢j : A E, a A ⊢ ⊢ ⊢c : ⊥ E ∪ H ⊢ ⊢ ⊢res(j, a A.c) : ⊥ Figure 4.
Proof system for the CDSAT proof terms the transition rules preserve such invariants, they are sound. The provability invariants of CDSAT are:

1. For every assignment H ⊢ A on the trail, H |= A; 2. For every conflict state ⟨Γ; E⟩, E |= ⊥.

Proof-carrying CDSAT keeps track of provability invariants by means of a trace of proof terms. We distinguish between deduction proof terms and conflict proof terms, intuitively related to Invariants (1) and (2), respectively. A deduction proof term records why an assignment H ⊢ A is on the trail, while a conflict proof term records why the second component of a conflict state ⟨Γ; E⟩ is a conflict. where in, lem, cfl, and res are the CDSAT proof constructors, j k ranges over theory proofs for T k , 1 ≤ k ≤ n, A is a singleton assignment, and H is a Boolean assignment with identifiers; res(j, a A.c) binds a in c, and lem(H .c) binds the identifiers of H in c, as represented by the dot.

The proof system of Fig. 4 helps understanding the invariants that proof terms keep track of. The first three rules establish the derivability of judgments of the form H ⊢ ⊢ ⊢j : A, witnessing invariant H |= A. Proof term in(A), where in stands for initial, witnesses the fact that an initial assignment A holds. The second rule shows that a theory proof j k can be coerced into a CDSAT deduction proof term. The rule for lem(H .c), where lem stands for lemma, shows that, whenever there is a conflict involving a Boolean assignment H , a clausal form of H is entailed by the rest of the conflict and therefore it is a lemma. The proof term carries H to indicate which part of the conflict is turned into a lemma. Since identifiers of assignments in H may occur in c, such occurrences are bound in lem(H .c).

The last two rules establish the derivability of judgments of the form E ⊢ ⊢ ⊢c : ⊥, witnessing invariant E |= ⊥. Proof term cfl(j k , a), where cfl stands for conflict, witnesses the conflict between the conclusion L of a theory inference and its flip L (having identifier a). Proof term res(j, a A.c), where res stands for resolve, is the only construct that combines two subproofs, connecting the conclusion A of the left premise with the hypothesis a A of the right premise. Any occurrence of a in c is bound in res(j, a A.c). Using the soundness of theory inferences, a structural induction on proof terms turns the intuition of witnessing invariants into the following theorem.

Theorem 4.3. If H ⊢ ⊢ ⊢j : A, then H |= A; if E ⊢ ⊢ ⊢c : ⊥, then E |= ⊥.
This choice of proof terms and proof system allows us to associate to every rule of the CDSAT transition system the simplest trace of how the rule transforms the relevant provability invariant, leading us to the next section.

Proof-Carrying CDSAT

The proof-carrying CDSAT transition system is given in Fig. 5. While a decision ? A does not carry a proof term, a justified assignment H ⊢j : A carries a deduction proof term j such that H ⊢ ⊢ ⊢j : A. Initial assignments take the form ∅ ⊢in(A) : A where the deduction proof term presents the initial assignment as a premise of the proof. If a theory inference J⊢ ⊢ ⊢ k L, 1 ≤ k ≤ n, supports the justified assignment J ⊢ L, the same inference J ⊢ ⊢ ⊢ k j k : L annotated with a theory proof supports the justified assignment J ⊢j k : L (see rule Deduce in Fig. 5).

Because proof terms may use identifiers of assignments, proof-carrying CDSAT manipulates assignments with identifiers, and the subset relation takes identifiers into account. In Fig. 5, the condition J ⊆ Γ means that J is a T k -assignment with identifiers, and for every a (t←c) in J , the pair t←c appears in Γ with identifier a. A conflict E is an assignment with identifiers such that E |=⊥ and E ⊆ Γ with the same meaning. Conflict resolution rules operate on states of the form ⟨Γ; E ; c⟩, where c is a conflict proof term. An analysis of the rules shows that the invariants in Theorem 4.4 hold.

Theorem 4.4. For all proof-carrying CDSAT-derivations

• If a trail containing H ⊢j : A is generated, then H ⊢ ⊢ ⊢j : A;

• If a conflict state ⟨Γ; E ; c⟩ is reached, then E ⊢ ⊢ ⊢c : ⊥.

A difference between the system in Fig. 5 and that in Fig. 1 is that in proof-carrying CDSAT the dichotomy between Fail and ConflictSolve is based on the outcome of the conflict resolution phase rather than the level of the conflict. Given Theorems 4.3 and 4.4, reaching state ⟨Γ; ∅ ; c⟩ means that the input problem is unsatisfiable in T + ∞ and c is a proof term witnessing its unsatisfiability. If such a state is reached, Fail fires and terminates the derivation in state unsat(c). It is simple to show that the conflict resolution rules in Fig. 5 reduce ⟨Γ; E ; c 1 ⟩ to a state of the form ⟨Γ; ∅ ; c⟩ if and only if level Γ (E) = 0; and that they solve the conflict producing some trail Γ ′ different from Γ if and only if level Γ (E) > 0.

The CDSAT transition system of Fig. 1 returns unsat as soon as a conflict at level 0 is found, because it does not generate a proof. For proof-carrying CDSAT, detecting a conflict at level 0 does not suffice: in order to generate a proof of unsatisfiability of the initial assignment, proof-carrying CDSAT Search rules Decide Γ -→ Γ, ? A if A is a T k -assignment for a term that is T k -relevant for Γ, and A is acceptable for the T k -module and its view of Γ, with 1 ≤ k ≤ n The next three rules share the conditions: J ⊆ Γ, (J ⊢ ⊢ ⊢ k j k : L), and L Γ, for some k,

1 ≤ k ≤ n. Deduce Γ -→ Γ, J ⊢j k : L if L Γ and L is in B Fail Γ -→ unsat(c) if L ∈ Γ with id a, and ⟨Γ; J ∪ { a L} ; cfl(j k , a)⟩ =⇒ * ⟨Γ; ∅ ; c⟩ ConflictSolve Γ -→ Γ ′ if L ∈ Γ with id a, and ⟨Γ; J ∪ { a L} ; cfl(j k , a)⟩ =⇒ * Γ ′ Conflict resolution rules Undo ⟨Γ; E ⊎ { a A} ; c⟩ =⇒ Γ ≤m-1 if A is a first-order decision of level m > level Γ (E) Resolve ⟨Γ; E ⊎ { a A} ; c⟩ =⇒ ⟨Γ; E ∪ H ; res(j, a A.c)⟩ if H ⊢j : A is in Γ and H does not contain a first-order decision A ′ whose level is level Γ (E ⊎ {A}) UndoDecide ⟨Γ; E ⊎ { a L} ; c⟩ =⇒ Γ ≤m-1 , ? L if H ⊢j : L is in Γ, m = level Γ (E) = level Γ (L)
and H contains a first-order decision

A ′ of level m LearnBackjump ⟨Γ; E ⊎ H ; c⟩ =⇒ Γ ≤m , E ⊢lem(H .c) : L if L is a clausal form of H and is in B, L Γ, L Γ, and level Γ (E) ≤ m < level Γ (H )
Figure 5. The proof-carrying CDSAT transition system integrates a proof of why E follows from the initial assignment with a proof of why E is unsatisfiable. This is achieved by proof-carrying Resolve, which combines proof term c, witnessing the unsatisfiability of the conflict, with proof term j witnessing that one of the assignments in the conflict, named A, follows from prior assignments: A is retained in the proof term res(j, a A.c). Proof-carrying LearnBackjump generates the proof term lem(H .c), recording that the learned lemma L is a clausal form of H , and turning the conflict proof term c representing a proof of unsatisfiability of E ⊎ H into a deduction proof term representing a proof of L from E.

Example of Proof-Carrying Derivation

We now illustrate some operations of proof-carrying CDSAT. Fig. 6 gives a refutation for the full version of the example in Fig. 2. Adding identifiers to the first conflict in Fig. 2 we get a 7 (¬l 2 ∨¬l 4 ∨¬l 5 ), a 2 l 2 , a 4 l 4 , a 5 l 5 .

The proof term for this conflict involves Unit Propagation:

c 1 = cfl(UP(a 7 , {a 2 , a 4 }), a 5
). The next step replaces l 5 in the conflict by its justification a 6 (¬l 4 ∨l 5 ), a 4 l 4 , yielding (Fig. 6, line 2) the conflict proof term c 2 = res(UP(a 6 , {a 4 }), a 5 l 5 .c 1 ) where UP(a 6 , {a 4 }) is the theory proof that justifies why l 5 is on the trail as a result of Unit Propagation. The conflict is solved by LearnBackjump as in Example 3.2, learning (¬l 2 ∨¬l 4 ) and placing (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢j 1 : (¬l 2 ∨¬l 4 ) on the trail (line 3), where j 1 = lem({ a 2 l 2 , a 4 l 4 }.c 2 ).

These patterns repeat several times in Fig. 6. For example, j 2 , j 5 , j 6 , j 9 , j 10 (lines 4,9,10,17,18) are deduction proof terms of the form UP(_, _), as they support unit propagations, and similarly to c 1 , proof term c 8 for conflict a (¬l 2 ∨¬l 4 ), a 2 l 2 , a 4 l 4 plugs in a unit propagation subproof (line 19): c 8 = cfl(UP(a, {a 2 }), a 4 ). The derivation involves the LRA inference (line 5) a 1 (x ← 3 /4) ⊢ ⊢ ⊢j 3 : (x ≤0)

where j 3 = eval({a 1 }), and the LRA inference (line 6) a 2 (y≥0), a 8 (x+y>0), a 9 (x ≤0) ⊢ ⊢ ⊢c 3 : ⊥ where c 3 = cfl(FM(a 2 , a 8 ), a 9 ) as a 2 (0 ≤ y), a 8 (y ≤ -x) ⊢ ⊢ ⊢ LRA FM(a 2 , a 8 ) : (0 ≤ -x).

It also employs the EUF inferences (lines 11 and 12)

a 10 (f (z)←blue), a 11 (f (y)←red) ⊢ ⊢ ⊢j 7 : f (z) f (y) a 12 (z ≃ y), a 13 (f (z) f (y)) ⊢ ⊢ ⊢c 5 : ⊥
where j 7 = neq(a 10 , a 11 ) and c 5 = cfl(Cong(a 12 ), a 13 ).

Deduction proof terms j 4 and j 8 (lines 8 and 16) justify the learning of lemmas ((x ≤0)∨¬l 2 ) and (x ≤0), respectively: therefore they instantiate the same pattern as j 1 , namely lem({_}._). The conflict proof terms c 4 , c 6 , c 7 , and c 9 through c 21 all encode Resolve steps, and therefore are of the form res(_, _._) like c 2 . More precisely, c 13 , c 15 -c 18 , c 20 , and c 21 , are of the form res(in(_), _._), whose effect is simply to remove an assignment from the conflict because it is an initial assignment. In contrast, conflict proof term c 19 is of the form res(j 1 , a (¬l 2 ∨¬l 4 ).c 18 ), where a is the identifier of the learned clause (¬l 2 ∨¬l 4 ) (line Input problem: (¬l 4 ∨l 5 ), (¬l 2 ∨¬l 4 ∨¬l 5 ), (l 2 ∨(z ≃ y)), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (f (z)←blue), (f (y)←red) where l 2 is (y≥0), and l 4 is (x+y>0). Assume decision A 1 is (x ← 3 /4). Detected conflicts are introduced with symbol ! △ .

To improve readability, identifiers in justifications and conflicts are omitted; they are determined by the current trail. ! △ ⟨Γ; (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , l 4 , l 5 ; c 1 ⟩ 1 =⇒ ⟨Γ; (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , l 4 , (¬l 4 ∨l 5 ) ; c 2 ⟩ 2 =⇒ Γ 0 , ? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢j 1 : (¬l 2 ∨¬l 4 ) 3 -→ Γ 0 , ? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢j 1 : (¬l 2 ∨¬l 4 ), (¬l 2 ∨¬l 4 ), l 2 ⊢j 2 : l 4 4 -→ Γ 0 , ? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢j 1 : (¬l 2 ∨¬l 4 ), (¬l 2 ∨¬l 4 ), l 2 ⊢j 2 : l 4 , A 1 ⊢j 3 :

(x ≤0) =: Γ 1 5 ! △ ⟨Γ 1 ; l 2 , l 4 , (x ≤0) ; c 3 ⟩ 6 =⇒ ⟨Γ 1 ; l 2 , (¬l 2 ∨¬l 4 ), (x ≤0) ; c 4 ⟩ 7 =⇒ Γ 0 , ? A 1 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢j 1 : (¬l 2 ∨¬l 4 ), A 1 ⊢j 3 : (x ≤0), (¬l 2 ∨¬l 4 ) ⊢j 4 : (x ≤0)∨¬l 2 =: Γ 2 8 -→ Γ 2 , ((x ≤0)∨¬l 2 ), (x ≤0) ⊢j 5 : l 2 9
-→ Γ 2 , ((x ≤0)∨¬l 2 ), (x ≤0) ⊢j 5 : l 2 , (l 2 ∨(z ≃ y)), l 2 ⊢j 6 : (z ≃ y) 10

-→ Γ 2 , ((x ≤0)∨¬l 2 ), (x ≤0) ⊢j 5 : l 2 , (l 2 ∨(z ≃ y)), l 2 ⊢j 6 : (z ≃ y), (f (z)←blue), (f (y)←red) ⊢j 7 : (f (z) f (y)) =: Γ 3 11 ! △ ⟨Γ 3 ; (f (z) f (y)), (z ≃ y) ; c 5 ⟩ 12 =⇒ ⟨Γ 3 ; (f (z) f (y)), (l 2 ∨(z ≃ y)), l 2 ; c 6 ⟩ 13 =⇒ ⟨Γ 3 ; (f (z) f (y)), (l 2 ∨(z ≃ y)), ((x ≤0)∨¬l 2 ), (x ≤0) ; c 7 ⟩ 14 =⇒ Γ 0 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢j 1 : (¬l 2 ∨¬l 4 ), (¬l 2 ∨¬l 4 ) ⊢j 4 : (x ≤0)∨¬l 2 , (f (z)←blue), (f (y)←red) ⊢j 7 : (f (z) f (y)), 15
(f (z) f (y)), (l 2 ∨(z ≃ y)), ((x ≤0)∨¬l 2 ) ⊢j 8 : (x ≤0) =: Γ 4 16 -→ Γ 4 , (¬(x ≤0)∨l 2 ), (x ≤0) ⊢j 9 : l 2 17 -→ Γ 4 , (¬(x ≤0)∨l 2 ), (x ≤0) ⊢j 9 : l 2 , (¬(x ≤0)∨l 4 ), (x ≤0) ⊢j 10 : l 4 =: Γ 5 18 ! △ ⟨Γ 5 ;
(¬l 2 ∨¬l 4 ), l 2 , l 4 ; c 8 ⟩ 19 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), l 2 , (¬(x ≤0)∨l 4 ), (x ≤0) ; c 9 ⟩ 20 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (x ≤0) ; c 10 ⟩ 21 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (f (z) f (y)), (l 2 ∨(z ≃ y)), ((x ≤0)∨¬l 2 ) ; c 11 ⟩ 22 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (f (z) f (y)), (l 2 ∨(z ≃ y)) ; c 12 ⟩ 23 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (f (z) f (y)) ; c 13 ⟩ 24 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (f (z)←blue), (f (y)←red) ; c 14 ⟩ 25 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l 4 ), (f (z)←blue) ; c 15 ⟩ 26 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ), (¬(x ≤0)∨l

) ; c 20 ⟩ 31 =⇒ ⟨Γ 5 ; ∅ ; c 21 ⟩ 32 -→ unsat(c 21 ) 33
Figure 6. A proof-carrying continuation of the CDSAT derivation in Fig. 2 30). Note that a occurs twice in c 19 : once in the subproof c 8 (line 19), as seen above, and once in the subproof (line 23) c 12 = res(j 4 , a 14 ((x ≤0)∨¬l 2 ).c 11 ), since j 4 = lem({ a 9 (x ≤0), a 2 l 2 }.c 4 ) (line 8), c 4 = res(j 2 , a 8 l 4 .c 3 ) (line 7), and j 2 = UP(a, {a 2 }) (line 4). This double occurrence reflects the fact that lemma (¬l 2 ∨¬l 4 ) has been reused in the derivation, which is a purpose of learning. Had Backjump been applied instead of LearnBackjump (cf. Example 3.4), the trail would have been extended (line 3) with (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ), l 2 ⊢j 11 : l 4 where the deduction proof j 11 = lem({ a 4 l 4 }.c 2 ) justifies why l 4 is on the trail. If this route had been followed, the conflict reflected by c 8 (line 19) would not have been detected. More steps would have been necessary to discover it, amounting to constructing another proof of (¬l 2 ∨¬l 4 ), possibly identical to the first one that was not recorded.

A full development of the final conflict proof term c 21 would show the absence of the deduction proof term j 3 (introduced on line 5). This is a general phenomenon in CDSAT: first-order decisions play a role in finding models, not proofs; thus, deduction proof terms referring to firstorder decisions cannot appear in the final proof term, and an easy optimization is to avoid constructing them.

From Proof Terms to Proofs

The CDSAT proof terms record enough information to reconstruct a proof of unsatisfiability from a CDSAT derivation concluding unsat. The proof system in Fig. 4 describes how proof terms specify the proof reconstruction steps to be performed. A deduction proof term j with H ⊢ ⊢ ⊢j : A indicates how to reconstruct a proof of H |= A. A conflict proof term c with E ⊢ ⊢ ⊢c : ⊥ indicates how to reconstruct a proof of E |= ⊥. For instance, the rule for res(j, a A.c) can be read as: if j allows the reconstruction of a proof that A follows from H , and if c allows the reconstruction of a proof that E, a A is unsatisfiable, then res(j, a A.c) allows the reconstruction of a proof that E ∪ H is unsatisfiable. A solver implementing the proof-carrying CDSAT transition system can reconstruct the proof in any proof format that (1) features two kinds of proofs (deduction proofs and conflict proofs), and ( 2) is equipped with proof operations corresponding to the rules of Fig. 4. In this view, proof reconstruction interprets proof terms in the desired proof format.

An alternative option is that the CDSAT solver manipulates directly the proofs denoted by the expressions in(A), j k , lem(H .c), cfl(j k , a), and res(j, a A.c). The choice between the two approaches depends on whether the proofs generated by proof reconstruction are better (e.g., shorter, more readable) than the proof terms. Another factor is whether direct manipulation during the derivation causes such a high runtime overhead that proof reconstruction is preferable. A third possibility is to consider proof terms themselves as the proof objects to be produced. Then a proof-checker would check directly the proof terms, checking that the rules of Fig. 4 are applied correctly. In the the rest of this section, we see how CDSAT proof terms can be turned into resolutionstyle proofs (Subsection 5.1), and how the LCF approach to proofs can be applied to CDSAT (Subsection 5.2).

Proof Format Based on Resolution

Resolution proofs are based on clausal form. A few caveats are in order. First, CDSAT views logical connectives such as ∧ and ∨ as interpreted symbols of the Boolean theory. Second, the existence of assignments such as (l 1 ∨l 2 )←false implies that clauses l 1 ∨ • • • ∨l m may not be the only formulae in proofs. Third, CDSAT does not assume that its input is in Conjunctive Normal Form (CNF). Therefore, we distinguish between object-level clauses, that are the clauses l 1 ∨ • • • ∨l m , and CDSAT clauses, that are the clauses in resolution proofs reconstructed from CDSAT proof terms. A CDSAT clause, or clause for short when there is no ambiguity, is a set of singleton Boolean assignments, written L 1 || • • • || L m to avoid confusion with object-level clauses. A CDSAT clause is a clause in the standard propositional sense, with CDSAT formulae (i.e., terms of sort prop) in place of Boolean variables (aka propositional atoms). Since in CDSAT there are firstorder assignments, the resolution proofs reconstructed from CDSAT proof terms use guarded clauses, written H → C, where H is a set of first-order assignments and C is a CDSAT clause. Guarded or hypothetical clauses are used extensively in the literature (e.g., [START_REF] Maria | On deciding satisfiability by theorem proving with speculative inferences[END_REF][START_REF] Dierkes | Model Building for Sets of Guarded Clauses[END_REF][START_REF] Ganzinger | A superposition decision procedure for the guarded fragment with equality[END_REF]).

A resolution proof reconstructed from a CDSAT proof term is a binary tree such that:

• Every leaf is labeled with either a guarded clause, called in this case theory lemma, or an input singleton assignment; and • Every internal node is labeled with a guarded clause, and, together with its two children, forms an instance of one of the following rules:

H 1 → C 1 || L H 2 → C 1 || L H 1 ∪ H 2 → C 1 || C 2 L H → C || L H → C A H, A → C H → C
The top rule is binary resolution, generalized to the presence of first-order assignments which play no role in the rule. In the bottom two rules, the left premise is a leaf labeled by an input singleton assignment: the left-hand rule can be seen as unit resolution; the right-hand rule covers the analogous case for a first-order assignment A.

In order to illustrate theory lemmas, consider a clausal form L 0 of {L 1 , . . . , L m }. The Boolean theory has the following lemmas, that can label the leaves of resolution trees:

∅ → L 0 || L 1 || • • • || L m 1≤i≤m ∅ → L 0 || L i (2) Since L 0 is a clausal form of {L 1 , . . . , L m }, L 0 || L 1 || • • • || L m and L 0 || L i , 1 ≤ i ≤ m, are propositional tautologies.
The first lemma allows the transformation of an object-level clause, the assignment L 0 , into a CDSAT clause: . . . . . .

H → C || L 0 ∅ → L 0 || L 1 || • • • || L m H → C || L 1 || • • • || L m Conversely,
H → C || L 1 || • • • || L m ∅ → L 0 || L 1 • • • ∅ → L 0 || L m
H → C || L 0 These transformations can be expressed compactly as the derivable inference rules The interpretation is defined by induction on proof terms as shown in Fig. 7. For instance, consider the interpretations of a deduction proof term and a conflict proof term that encapsulate a unit propagation, where K is a clausal form of H = H ′ ⊎ {L} as in inference (1) from Section 3:

⟦∅ ⊢ ⊢ ⊢in(A) : A⟧

:= A ⟦E ⊢ ⊢ ⊢lem(H .c) : L⟧ := ⟦E ⊎ H ⊢ ⊢ ⊢c : ⊥⟧ E FO → E clause || H clause E FO → E clause || L ⟦J ⊢ ⊢ ⊢j k : L⟧ := J FO → J clause || L ⟦J ⊎ { a L} ⊢ ⊢ ⊢cfl(j k , a) : ⊥⟧:= J FO → J clause || L ⟦E ∪ H ⊢ ⊢ ⊢res(j, a L.c) : ⊥⟧ if j is not of the form in(A) := ⟦H ⊢ ⊢ ⊢j : L⟧ H FO → H clause || L ⟦E ⊎ { a L} ⊢ ⊢ ⊢c : ⊥⟧ E FO → E clause || L H FO ∪E FO → H clause || E clause ⟦E ⊢ ⊢ ⊢res(in(L), a L.c) : ⊥⟧ := L ⟦E ⊎ { a L} ⊢ ⊢ ⊢c : ⊥⟧ E FO → E clause || L E FO → E clause ⟦E ⊢ ⊢ ⊢res(in(A), a A.c) : ⊥⟧ if A is first-order := A ⟦E ⊎ { a A} ⊢ ⊢ ⊢c : ⊥⟧ E FO , A → E clause E FO → E clause
H → C || L 0 H → C || L 1 || • • • || L m H → C || L 1 || • • • || L m H → C || L 0 that involve
⟦{ a K } ⊎ H ′ ⊢ ⊢ ⊢UP(a, {a 1 , . . . , a n }) : L⟧ ⟦{ a K } ⊎ H ′ , a 0 L ⊢ ⊢ ⊢cfl(UP(a, {a 1 , . . . , a n }), a 0 ) : ⊥⟧
where a 1 , . . . , a n are the identifiers of the elements of H ′ . Both become an instance of a Boolean theory lemma (2):

∅ → K || H ′ clause || L
Since a CDSAT answer of the form unsat(c) means ∅ ⊢ ⊢ ⊢c : ⊥, the resolution proof reconstructed from proof term c is a refutation, as its conclusion is ∅ → ∅, that is, the empty clause. As already noted in Section 4, first-order decisions do not appear in proofs. It follows that first-order assignments may appear in proofs only if they are initial assignments. If the input problem contains no first-order assignments (i.e., it is an SMT problem), the reconstructed proof involves only singleton Boolean assignments labeling leaves and guarded clauses of the form ∅ → C labeling leaves or internal nodes. In other words, the reconstructed proof is a resolution refutation in the standard sense, deriving the empty clause, and with leaves labeled by input assignments or theory lemmas.

The use of theory lemmas for propositional reasoning is less usual and it descends from the choice of treating propositional logic as a theory. Advantages include the possibility of applying CDSAT to problems that are not in CNF, and the possibility of transforming object-level clauses into CD-SAT clauses and vice versa, as shown above. These transformations also provide a native feature for sharing resolution proofs. For instance in the refutation of Section 4.4, the conflict proof term c 19 = res(j 1 , a (¬l 2 ∨¬l 4 ).c 18 ), with j 1 = lem({ a 2 l 2 , a 4 l 4 }.c 2 ), yields a 6 L 1 , a 7 L 2 ⊢ ⊢ ⊢c 19 : ⊥, where L 1 is (¬l 4 ∨l 5 ) and L 2 is (¬l 2 ∨¬l 4 ∨¬l 5 ). The resolution proof reconstructed from c 19 is:

⟦ a 6 L 1 , a 7 L 2 , a 2 l 2 , a 4 l 4 ⊢ ⊢ ⊢c 2 : ⊥⟧ ∅ → L 1 || L 2 || l 2 || l 4 ∅ → L 1 || L 2 || (¬l 2 ∨¬l 4 ) ⟦ a (¬l 2 ∨¬l 4 ) ⊢ ⊢ ⊢c 18 : ⊥⟧ ∅ → (¬l 2 ∨¬l 4 ) ∅ → L 1 || L 2
The fact that the learned clause ¬l 2 ∨¬l 4 is reused in c 18 , as described in Section 4.4, means that the resolution proof ⟦ a (¬l 2 ∨¬l 4 ) ⊢ ⊢ ⊢c 18 : ⊥⟧ has two leaves labeled by the same theory lemma ∅ → (¬l 2 ∨¬l 4 ) || l 2 || l 4 . An alternative resolution proof with root ∅ → L 1 || L 2 can be obtained by replacing those two leaves with the subproof interpreting c 2 , and replacing (¬l 2 ∨¬l 4 ) by L 1 || L 2 in all nodes underneath. This avoids the explicit conversions between the object-level clause ¬l 2 ∨¬l 4 and the CDSAT clause l 2 || l 4 . However, in this alternative proof, the subtree interpreting c 2 is duplicated. Such duplications happen in the standard format of resolution trees where there is only one kind of clauses. By distinguishing between object-level clauses and CDSAT clauses, and using the former for input clauses and the latter for generated clauses, CDSAT natively supports the explicit sharing of subproofs as in resolution DAG's.

An LCF Architecture for CDSAT

Another example of proof format is the "dummy" one, where proofs do not contain any information other than what they are supposed to be the proofs of :

1. A deduction proof j with H ⊢ ⊢ ⊢j : L is the pair ⟨H, L⟩, and 2. A conflict proof c with H ⊢ ⊢ ⊢c : ⊥ is H . Although this "proof format" does not allow any proof checking, the trustworthiness of a reasoner producing such proofs can still be established by the LCF programming abstraction [START_REF] Gordon | Edinburgh LCF: a mechanized logic of computation[END_REF][START_REF] Milner | LCF: A Way of Doing Proofs with a Machine[END_REF]. This approach uses a type theorem , whose constructed inhabitants are provable formulae. Actually, this type is defined as an alias for the type formula of formulae, but this is known only to a fixed and well-identified piece of code, called the LCF kernel. This kernel hides the definition of theorem to the outside world and exports a range of kernel primitives to manipulate inhabitants of type theorem in a safe and provably correct way. For instance, a primitive modus_ponens : theorem -> theorem -> theorem takes as arguments two inhabitants F and G of type theorem, checks that F is of the form G ⇒ R, and returns R as an inhabitant of theorem. The kernel can export a primitive that reveals that any inhabitant of theorem is a formula, but obviously not one that casts any inhabitant of formula into type theorem. In this way, the existence of an inhabitant F of theorem witnesses the fact that F is provable, as an inhabitant only results from a series of correct manipulations by the kernel primitives: if the kernel code is trusted, then F can be trusted to be a theorem, while no proof has ever been constructed in memory.

CDSAT is well-suited for the LCF approach: given a type assign for assignments and single_assign for singleton assignments, a trusted kernel defines types type deduction = assign*single_assign type conflict = assign hides their definitions to the outside world, and exports a range of primitives corresponding to the proof term constructs. The signature in Fig. 8 lists hidden type definitions and exported primitives. The primitives check that the conditions of the rules in Fig. 4 are met: for instance, in checks that its argument is one of the initial assignments. Primitive lem takes as arguments a conflict E and an assignment H , checks that H is Boolean and is included in E, computes a clausal form L of H , and produces the deduction ⟨E\H , L⟩, where \ is set subtraction. Primitive res takes a deduction ⟨H, L⟩ and a conflict, checks that L appears in the conflict, and returns the conflict where L is replaced by H . Primitives coerc and cfl take as arguments a T k -theory proof, 1 ≤ k ≤ n, given as an inhabitant of 'k theory_proof, a type parameterized by k. Their first argument is a handler for theory T k , whose type 'k theory_handler is parameterized by type deduction type conflict in : single_assign -> deduction coerc : 'k theory_handler -> 'k theory_proof -> deduction lem : conflict -> assign -> deduction cfl : 'k theory_handler -> 'k theory_proof -> conflict res : deduction -> conflict -> conflict reveal : conflict -> assign Figure 8. API exported by a CDSAT kernel a matching k, as implemented for example by a Generalized Algebraic DataType (GADT) [START_REF] Cheney | First-class phantom types[END_REF][START_REF] Xi | Guarded recursive datatype constructors[END_REF]. The handler allows the primitives to check that T k is one of the combined theories before coercing the theory proof, trusted to be correct, into a deduction or a conflict. Proof-carrying CDSAT can be programmed on top of this kernel, so that, when it halts with answer unsat(c), the proof term c is an inhabitant of type conflict. The reveal primitive applied to c will return the empty assignment. Although no proof has been constructed in memory, the answer is correct by construction.

Discussion

Conflict-driven satisfiability procedures work by constructing partial assignments, detecting conflicts when the assignment falsifies the input formula, and performing conflictdriven inferences to learn new formulae and reorient the search. In prior work, we presented CDSAT as a combination procedure for conflict-driven theory satisfiability solvers for mutually disjoint theories, and proved its termination, soundness, and completeness under suitable assumptions. In the present work, we extend the CDSAT transition system with lemmatization so that new learned clauses can be added during backjumping from a conflict even in the context of a partial assignment. We also annotate the transition system in order to construct a proof object when the procedure discovers that the input problem is unsatisfiable. These proof objects can be rendered in a number of proof formats and the resulting proofs checked by a trusted checker or shown to be correct by construction.

In future work, we plan to implement a reasoner based on the CDSAT approach exploring different search plans and proof formats. Search plans play a key role in coordinating the work of theory modules, including prioritizing them with respect to both decisions and deductions. Topics for further investigations include extensions of proofs to account for preprocessing techniques widely used in SAT and SMT solving, evaluating the cost of proof generation and proof checking in CDSAT, and studying proof formats that reduce it as done for instance in SAT solving [START_REF] Cruz-Felipe | Efficient certified RAT verification[END_REF].

Example 3 . 3 .

 33 Consider the same LearnBackjump step as in Example 3.2 except that the destination level is m = 0. We get Γ 0 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢ (¬l 2 ∨¬l 4 )

Example 3 . 5 .

 35 LearnBackjump can be applied also to the first conflict in Fig.2, namely ⟨Γ; (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , l 4 , l 5 ⟩. Consider a step with E = {¬l 2 ∨¬l 4 ∨¬l 5 } and H = {l 2 , l 4 , l 5 }, so that level Γ (H ) = 4 and level Γ (E) = 0. Regardless of the choice of destination level m, 0 ≤ m < 4, a clausal form of H is redundant since clause ¬l 2 ∨¬l 4 ∨¬l 5 is already on the trail and LearnBackjump does not add it.

Figure 3 .

 3 Figure 3. Equality inference rules for terms of sort s

Definition 4 . 2 (

 42 CDSAT proof terms). A CDSAT proof term is either a deduction proof term j ::= in(A) j k lem(H .c)or a conflict proof term c ::= cfl(j k , a) res(j, a A.c)

  the other lemmas allow the reification of a CD-SAT clause L 1 || • • • || L m into an object-level clause:

Figure 7 .

 7 Figure 7. Interpretation of proof terms in the resolution proof format

  Input problem H 0 including:(¬l 4 ∨l 5 ), (¬l 2 ∨¬l 4 ∨¬l 5 ) Initial trail Γ 0 including: ∅ ⊢ (¬l 4 ∨l 5 ), ∅ ⊢ (¬l 2 ∨¬l 4 ∨¬l 5 ) Extending Γ 0 into Γ = Γ 0 , ? A 1 , ? l 2 , ? A 3 , ? l 4 , (¬l 4 ∨l 5 ), l 4 ⊢ l 5 (involving unrelated decisions A 1 and A 3 ) First conflict:⟨Γ; (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , l 4 , l 5 ⟩ Applying Resolve to l 5 : ⟨Γ; (¬l 2 ∨¬l 4 ∨¬l 5 ), l 2 , l 4 , (¬l 4 ∨l 5 )⟩ Figure 2. Propositional extract from a CDSAT derivationWe consider these three features in this order.Learning and backjumping is the generic behavior of rule LearnBackjump. This rule singles out a Boolean subset H of the conflict E ⊎ H , such that level Γ (H ) > level Γ (E). Then, it solves the conflict by jumping back to a level m, such that level Γ (E) ≤ m < level Γ (H ), and learning a clausal form L of H . The system learns L by adding to the trail the justified assignment E ⊢ L, since E ⊎ H |=⊥ implies E |= L, as L is a clausal form of H . The clausal form L may assign a Boolean value to a new term, and therefore it must be an element of B. Note that H does not necessarily contain all the Boolean assignments in the conflict: the choices of the Boolean subset H and the destination level m are left to the search plan.

. Rule LearnBackjump is quite versatile, since 1. It allows CDSAT to perform learning and backjumping; 2. It allows CDSAT to perform learning and restart; 3. It covers as a special case the Backjump rule of the basic version of CDSAT

[START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF]

, adding the capability to learn assertion clauses.

  by Backjump, except for the learned clause K. The advantage is that K can be reused in future branches of the search. The level of E ⊢ K is level Γ (E): the smaller level Γ (E) is, the longer K may remain on the trail and be used for inferences. , ? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢ (¬l 2 ∨¬l 4 ),

	Example 3.7. Continuing Example 3.2 from
	Γ 0 rule Deduce with inference (1) generates
	Γ 0 ,

? A 1 , ? l 2 , (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ⊢ (¬l 2 ∨¬l 4 ), (¬l 2 ∨¬l 4 ), l 2 ⊢ l 4 .

  {a 1 , . . . , a n }) : L where a 1 , . . . , a n are the identifiers of the assignments in H ′ . For Linear Rational Arithmetic (LRA) annotated inferences include instances of Fourier-Motzkin resolutiona 1 (t 1 ←c 1 ), a 2 (t 2 ←c 2 ) ⊢ ⊢ ⊢eq(a 1 , a 2 ) : t 1 ≃ t 2if c 1 and c 2 are the same T + -value of sort s a 1 (t 1 ←c 1 ), a 2 (t 2 ←c 2 ) ⊢ ⊢ ⊢neq(a 1 , a 2 ) : t 1 t 2 if c 1 and c 2 are distinct T + -values of sort s

  4 ) ; c 16 ⟩ 27 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ), (¬(x ≤0)∨l 2 ) ; c 17 ⟩ 28 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ) ; c 18 ⟩ 29 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ∨¬l 5 ), (¬l 4 ∨l 5 ) ; c 19 ⟩ 30 =⇒ ⟨Γ 5 ; (¬l 2 ∨¬l 4 ∨¬l 5

  the Boolean theory lemmas only if m ≥ 2 (i.e., the clause is not a unit clause).Given an assignment H , we write H FO for the greatest subset of H made of first-order assignments; and we write H clause for the clause L 1 || • • • || L n where L 1 , . . . , L n are the singleton Boolean assignments in H .

The resolution proof format for CDSAT interprets • A deduction proof term ∅ ⊢ ⊢ ⊢in(A) : A as a proof concluding A; • A deduction proof term H ⊢ ⊢ ⊢j : L of another form as a proof concluding H FO → H clause || L; • A conflict proof term H ⊢ ⊢ ⊢c : ⊥ as a proof concluding H FO → H clause .

The notion of endorsement given here corresponds to that of viewendorsement (see[START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Definition 7), obtained by combining the notions of endorsement for a single theory (see[START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF], Definition 6) and theory view of an assignment (see[START_REF] Paola Bonacina | Satisfiability modulo theories and assignments[END_REF],

Definition 2), omitted here for reasons of space.

while the first author was an international observer at the SRI International Computer Science Laboratory, whose support is greatly appreciated. This research was funded in part by the National Science Foundation with grants CCF-1528153 and CNS-0917375, by DARPA under agreement number FA8750-16-C-0043, and by the Università degli Studi di Verona with grant "Ricerca di base 2015. " The views and conclusions contained herein are those of the authors and should or the U.S. Government.