The family of SCL (Clause Learning from Simple Models) calculi learns clauses with respect to a partial model assumption, similar to CDCL (Conflict Driven Clause Learning). The partial model always consists of ground first-order literals and is built by decisions and propagations. In contrast to propositional logic where propagation chains are limited, in first-order logic they can become infinite. Therefore, the SCL family does not require exhaustive propagation and the size of the partial model is always finitely bounded. Any partial model not leading to a conflict constitutes a model for the respective finitely bounded ground clause set. We show that all potential partial models can be explored as part of the SCL calculus for first-order logic without equality and that any overall model is an extension of a partial model considered.
There are meanwhile three instances of the SCL calculus family: SCL for first-order logic
without equality [
The family of propositional CDCL calculi uses similar ideas if extended to
optimization [
The paper is now organized as follows. After clarifying some notions, Section 2, the
HSCL calculus is introduced in Section 3. The HSCL calculus is an extension and
unification of the already existing calculi for first-order logic without equality [
We assume a first-order language without equality where N denotes a clause set; C, D denote clauses; L, K, H denote literals; A, B denote atoms; P, Q, R denote predicates; t, s terms; f, g, h function symbols; a, b, c constants; and x, y, z variables. Atoms, literals, clauses and clause sets are considered as usual, where in particular clauses are identified both with their disjunction and multiset of literals. The complement of a literal is denoted by the function comp. Semantic entailment |= is defined as usual where variables in clauses are assumed to be universally quantified. Substitutions σ, τ are total mappings from variables to terms, where dom(σ) := {x | xσ 6= x} is finite and codom(σ) := {t | xσ = t, x ∈ dom(σ)}. Their application is extended to literals, clauses, and sets of such objects in the usual way. A term, atom, clause, or a set of these objects is ground if it does not contain any variable. A substitution σ is ground if codom(σ) is ground. A substitution σ is grounding for a term t, literal L, clause C if tσ, Lσ, Cσ is ground, respectively. The function mgu denotes the most general unifier of two terms, atoms, literals. We assume that any mgu of two terms or literals does not introduce any fresh variables and is idempotent. A closure is denoted as C · σ and is a pair of a clause C and a grounding substitution σ. The function gnd returns the set of all ground instances of a literal, clause, or clause set with respect to the signature of the respective clause set.
A partial model M for a clause set N is a satisfiable set of ground literals. A ground clause C is true in M , denoted M |= C, if C ∩ M 6= ∅, and false otherwise. A ground clause set N is true in M , denoted M |= N if all clauses from N are true in M .
Let ≺ denote a well-founded, total, strict ordering on ground literals. This ordering is then lifted to clauses and clause sets by its respective multiset extension. We overload ≺ for literals, clauses, clause sets if the meaning is clear from the context. The ordering is lifted to the non-ground case via instantiation: we define C ≺ D if for all grounding substitutions σ it holds Cσ ≺ Dσ. We define N C := {D | D ∈ N and D C}. as the reflexive closure of ≺ and Definition 1 (Clause Redundancy). A ground clause C is redundant with respect to a ground clause set N and an order ≺ if N C |= C. A clause C is redundant with respect to a clause set N and an order ≺ if for all C0 ∈ gnd(C) it holds that C0 is redundant with respect to gnd(N ).
Let ≺B denote a well-founded, total, strict ordering on ground atoms such that for any ground atom A there are only finitely many ground atoms B with B ≺B A. For example, an instance of such an ordering could be KBO without zero-weight symbols. The ordering ≺B is lifted to literals by comparing the respective atoms. It is lifted to clauses by a multiset extension. Given an ordering ≺B and a ground literal β, the function gnd≺Bβ computes the set of all ground instances of a literal, clause, or clause set where the grounding is restricted to produce literals L with L ≺B β. 3. Exhaustive Partial Model Exploration with SCL In this section, we restrict model exploration to finite ground models. Hence, models are build with respect to a maximal literal β and a literal ordering ≺B. For fixed β and ≺B, the proposed calculus HSCL always terminates: Either by finding a contradiction, or by exploring all partial models that are smaller than β with respect to ≺B. Of course, those (finite) models are in general not extendable to a complete model of the clause set. If a clause set can be refuted by instantiating to ground literals smaller β, such a refutation will be found by HSCL. Thus, HSCL is complete for first-order logic when run with a suficiently large β. Even in cases where no refutation exists, enumerating partial models yields information about the overall structure of complete models. Furthermore, clauses learned from conflicts during this process can be re-used in later runs to speed up exploration of the original problem.
The HSCL Rules The inference rules of HSCL are represented by an abstract rewrite system. They operate on a problem state, a seven-tuple (Γ; N ; U ; β; N 0; k; D) where Γ is a sequence of annotated ground literals, the trail ; N and U are the sets of initial and learned clauses; β is a ground literal limiting the literals considered for instantiation; N 0 is a set of clauses that excludes all already seen partial models; k counts the number of decisions; and D is a status that is either true >, false (⊥)R, finished with exploration (⊥)E, or an annotated closure ((C · σ))u, where u ∈ {E, R}
Literals in Γ have the form X:Lr, where X ∈ {D, E, P} is the type of the literal and r its justification. The justification r is a level, a closure, or the combination of a level and a closure. We often omit irrelevant parts of the justification in specific contexts. The type can either be a Decision, a Propagation from N , or an Exclusion from N 0. As we do not want to explore partial models twice, decisions are no longer completely arbitrary. Instead, if a decision of a ground literal Lσ would lead to visiting a partial model again, HSCL will exclude this possibility by appending comp(Lσ) to the trail instead. This mechanism works similar to propagation. However, instead of propagating from N ∪ U , excluded literals are propagated from N 0 and are therefore decision literals with respect to N ∪ U . This mechanism is similar for conflict detection: Regular conflicts can be detected against clauses from N ∪ U . In contrast, excluded conflicts are to a clause in N 0. These two kinds of conflicts are distinguished by their respective annotation u ∈ {E, R}.
In the trail, furthermore, decided and excluded literals are annotated with a numerical level k, meaning that L is the k-th decided or excluded literal. Lastly, propagated and excluded literals are annotated with a closure that propagated the literal to become true.
A ground literal L is of level i with respect to a problem state (Γ; N ; U ; β; N 0; k; D) if L or comp(L) occurs in Γ and the first decision or exclusion literal left from L (comp(L)) in Γ, including L, is annotated with i. If there is no such decision literal then its level is zero. A ground clause D is of level i with respect to a problem state (Γ; N ; U ; β; N 0; k; D) if i is the maximal level of a literal in D; the level of the empty clause ⊥ is 0. A literal L is undefined in Γ if neither L nor comp(L) occur in Γ. The initial state for a first-order clause set N is ( ; N ; ∅; β; ∅; 0; >), where β is an arbitrary but fixed literal.
The basic rules for trail building, Propagate and Decide, are left unmodified compared to the original SCL calculus, except for the diference that literals on the trail are now annotated with their respective source. However, the trail building rules are supplemented with the Exclude rule.
Propagate (Γ; N ; U ; β; N 0; k; >) ⇒HSCL (Γ, P:Lσ(C0∨L)δ·σ; N ; U ; β; N 0; k; >) provided C ∨ L ∈ (N ∪ U ), C = C0 ∨ C1, C1σ = Lσ ∨ · · · ∨ Lσ, C0σ does not contain Lσ, δ is the mgu of the literals in C1 and L, (C ∨ L)σ is ground, (C ∨ L)σ ≺B {β}, C0σ is false under Γ, and Lσ is undefined in Γ
The rule Propagate applies exhaustive factoring to the propagated literal with respect to the grounding substitution σ and annotates the factored clause to the propagation literal on the trail.
provided L ∈ C for a C ∈ (N ∪ U ), Lσ is a ground literal undefined in Γ, and Lσ ≺B β (Γ; N ; U ; β; N 0; k; >) ⇒HSCL (Γ, D:Lσk+1; N ; U ; β; N 0; k + 1; >)
(Γ; N ; U ; β; N 0; k; >) ⇒HSCL (Γ, E:Lσk+1:(C0∨L)δ·σ; N ; U ; β; N 0; k + 1; >) provided C ∨ L ∈ N 0, C = C0 ∨ C1, C1σ = Lσ ∨ · · · ∨ Lσ, C0σ does not contain Lσ, δ is the mgu of the literals in C1 and L, C0σ is false under Γ, (C ∨ L)σ is ground, (C ∨ L)σ ≺B {β}, and Lσ is undefined in Γ
The rule Exclude works like Propagate, except it uses learned information from N 0 instead of N ∪ U . Thus, the inferred literal is not necessarily entailed by Γ ∪ N , but it prevents the generation of an already visited partial model (stuck state, see Definition 2 below). However, in combination with N 0, the literal must always be entailed by the clause set and the trail, i.e. Γ ∪ N ∪ N 0 |= Lσ. Hence, when only considering N ∪ U , the excluded literal will be treated as a decision, but when considering N ∪ U ∪ N 0, the excluded literal can be treated as propagated. This diference will be respected in all rules below. Most rules, in their basic form, are left essentially unmodified, but have a dual version added that treats excluded literals and information from N 0 accordingly.
provided D ∈ (N ∪ U ), Dσ false in Γ
(Γ; N ; U ; β; N 0; k; >) ⇒HSCL (Γ; N ; U ; β; N 0; k; (D · σ)R)
provided D ∈ N 0, Dσ false in Γ
(Γ; N ; U ; β; N 0; k; >) ⇒HSCL (Γ; N ; U ; β; N 0; k; (D · σ)E)
The classical rules construct a (partial) model via the trail Γ for N ∪ U until a conflict, i.e., a false clause with respect to Γ is found. In HSCL, we also allow a conflict to a clause in N 0, meaning that all partial models that could be built under this trail have already been discovered. Thus, ConflictE signals the rewrite system that all further attempts with trail Γ should be excluded from future searches.
Clearly, these two kinds of conflicts need to be separated. A conflict is annotated (D · σ)R if it was a regular conflict to N ∪ U , i.e., learning clauses from N ∪ U and searching for a refutation. In contrast, (D · σ)E denotes a conflict to a clause from N 0, i.e., the current state was already visited, resulted in a partial model and can therefore be excluded.
If a conflict is found, it is resolved by the conflict resolution rules below. Before any conflict resolution step, we assume that the respective clauses are renamed such that they do not share any variables and that the grounding substitutions of closures are adjusted accordingly.
Skip (Γ, X:L; N ; U ; β; N 0; k; (D · σ)u) ⇒HSCL (Γ; N ; U ; β; N 0; k − i; (D · σ)u) provided comp(L) does not occur in Dσ, and if X ∈ {D, E}, i.e. L is a decision or exclusion literal, then i = 1, else i = 0 Factorize (Γ; N ; U ; β; N 0; k; ((D∨L∨L0)·σ)u) ⇒HSCL (Γ; N ; U ; β; N 0; k; ((D∨L)η·σ)u) provided Lσ = L0σ, η = mgu(L, L0) ResolveR (Γ, P:Lδ(C∨L)·δ; N ; U ; β; N 0; k; ((D ∨ L0) · σ)R) ⇒HSCL (Γ, P:Lδ(C∨L)·δ; N ; U ; β; N 0; k; ((D ∨ C)η · σδ)R) provided Lδ = comp(L0σ), η = mgu(L, comp(L0))
Note that ResolveR strongly resembles the original SCL resolve. In particular, it does not remove the literal Lδ from the trail. This is needed if the clause Dσ contains further literals complementary of Lδ that have not been factorized.
ResolveE (Γ, X:Lδ(C∨L)·δ; N ; U ; β; N 0; k; ((D ∨ L0) · σ)E) ⇒HSCL (Γ, X:Lδ(C∨L)·δ; N ; U ; β; N 0; k; ((D ∨ C)η · σδ)E) provided X ∈ {E, P}, Lδ = comp(L0σ), η = mgu(L, comp(L0))
ResolveE takes all information from N ∪ U ∪ N 0. Since excluded literals act like propagations with respect to N 0, they can be resolved with during applications of ResolveE. In contrast, this is not possible in ResolveR, and excluded literals must be treated like decisions while resolving regular conflicts.
BacktrackR (Γ0, K, Γ1, X : comp(Lσ)k; N ; U ; β; N 0; k; ((D∨L)·σ)R) ⇒HSCL (Γ0; N ; U ∪ {D ∨ L}; β; N 0; j − i; >) provided X ∈ {E, D} and Dσ is of level i0 < k, and Γ0, K is the minimal trail subsequence such that there is a grounding substitution τ with (D ∨ L)τ is false in Γ0, K but not in Γ0, the literal K is of level j, if K is a decision or an exclusion literal then i = 1, otherwise i = 0 BacktrackE (Γ0, K, Γ1, D : comp(Lσ)k; N ; U ; β; N 0; k; ((D ∨ L) · σ)E) ⇒HSCL (Γ0; N ; U ; β; N 0 ∪ {D ∨ L}; j − i; >) provided Dσ is of level i0 < k, and Γ0, K is the minimal trail subsequence such that there is a grounding substitution τ with (D ∨ L)τ is false in Γ0, K but not in Γ0, the literal K is of level j, if K is a decision or an exclusion literal then i = 1, otherwise i = 0
Please note that the corner case j + 1 = k and τ = σ is also part of both backtrack rules. The rules backtrack to the minimal trail where the clause D ∨ L propagates. Also, note that the existence of the literal K is guaranteed if (D ∨ L)σ 6= ⊥ and all other preconditions of Backtrack are met. Then, (D ∨ L)σ is false under Γ0, K, Γ1, comp(Lσ) by soundness (see Definition 3). However, (D ∨ L)σ must be undefined and hence not false under the empty trail. Thus, there must be an intermediate literal K on the trail where the demanded property holds.
While BacktrackR learns to the clause set U , BacktrackE learns clauses to N 0. Here, BacktrackR can also jump back to excluded literals since they are treated like decisions w.r.t. N ∪ U . In contrast, excluded literals are propagations for conflicts with N ∪ U ∪ N 0 and, thus, cannot be backtracked to. The clause D ∨ L added by the rule BacktrackR to U is called a learned clause. Similarly, clauses added by backtrack to N 0 are called excluded clauses.
Definition 2 (Stuck State). A state (M ; N ; U ; β; N 0; k; D) is called stuck if D 6= (⊥ · σ)u and none of the above rules are applicable.
Unstuck (Γ; N ; U ; β; N 0; k; >) ⇒HSCL ( ; N ; U ; β; N 0 ∪ {C}; 0; >) provided (Γ; N ; U ; β; N 0; k; >) is a stuck state and C = WLi∈decision(Γ) comp(Li)
In this rule, the function decision(Γ) collects all decided literals D:Lk that have been introduced by applications of the rule Decide. If no such literal exists in Γ, then C = ⊥. This rule could be further refined by considering the efect of decisions on satisfying clauses from gnd≺Bβ(N ).
Finish (Γ; N ; U ; β; N 0; k; (⊥)E) ⇒HSCL (ε; N ; ∅; β; ∅; 0; >) (D:P (a)1; N ; ∅; β; ∅; 1; >) (D:P (a)1, P:¬Q(a)C2·σ; N ; ∅; β; ∅; 1; >) (ε; N ; ∅; β; N 0 = {¬P (a)}; 0; >) (E:¬P (a)1:¬P (a); N ; ∅; β; N 0; 1; >)
Decide ⇒HSCL
Propagate ⇒HSCL
Unstuck ⇒HSCL
Exclude ⇒HSCL
Propagate ⇒HSCL
ConflictR ⇒HSCL
ResolveR ⇒HSCL ⇒FHaScCtoLrize
Skip ⇒HSCL
BacktrackR (ε; N ; {P (x)}; β; N 0; 0; >) ⇒HSCL
Propagate ⇒HSCL
ConflictE ⇒HSCL
ResolveE ⇒HSCL ⇒FHiSnCisLh (ε; N ; {P (x)}; β; N 0; 0; (⊥)E) (P:P (a)P (x)·σ; N ; {P (x)}; β; N 0; 0; >) (P:P (a)P (x)·σ; N ; {P (x)}; β; N 0; 0; (¬P (a))E)
The last two rules allow us to explore stuck states. Whenever a stuck state is found, the trail is reset, and this particular stuck state will be prevented from being explored again by adding the clause consisting of the complement of all decisions to the exclusion set N 0. Notably, stuck states directly correspond to partial models with literals ≺B β, see Definition 15. Thus, exploring stuck states is a way to get insights on the literal structure of partial models. In the following, we will construct regularity rules such that a complete run will eventually explore all stuck states. This run also enumerates all partial models w.r.t. ≺B and β, as shown in Theorem 16.
A first simple example showing the application of the calculus rules is as follows. Consider N = {C1 = P (x)∨Q(x), C2 = ¬P (x)∨¬Q(x), C3 = P (x)∨¬Q(x)}. Let σ denote the substitution {x 7→ a}. Choose β and ≺B in a way that only {P (a), ¬P (a), Q(a), ¬Q(a)} ≺B {β}. Then, the following HSCL run explores all models for N :
In this example, there is only one partial model {P (a), ¬Q(a)}. Hence, Unstuck is only applied once in the overall HSCL run. A more complex example will be presented at the end of this section.
Definition 3 (Sound States). A state (Γ; N ; U ; β; N 0; k; D) is sound if the following conditions hold: 1. Γ is a consistent sequence of annotated ground literals, 2. for each decomposition Γ = Γ1, P:LσC∨L·σ, Γ2 we have that Cσ is false under Γ1 and Lσ is undefined under Γ1, N ∪ U |= C ∨ L (E:¬P (a)1:¬P (a), P:Q(a)C1·σ; N ; ∅; β; N 0; 1; >) (E:¬P (a)1:¬P (a), P:Q(a)C1·σ; N ; ∅; β; N 0; 1; (C3 · σ)R) (E:¬P (a)1:¬P (a); N ; ∅; β; N 0; 1; (P (x) · σ)R) (E:¬P (a)1:¬P (a), P:Q(a)C1·σ; N ; ∅; β; N 0; 1; (P (x) · σ)R) (E:¬P (a)1:¬P (a), P:Q(a)C1·σ; N ; ∅; β; N 0; 1; (P (x) ∨ P (x) · σ)R) Lemma 4 (Soundness of the initial state). The initial state ( ; N ; ∅; β; ∅; 0; >) is sound. Proof. Criteria 1–4 and 8 are trivially satisfied by Γ = . Furthermore, N |= ∅, fulfilling criterion 5. Lastly, criteria 6 and 7 are trivially fulfilled for D = >.
Theorem 5 (Soundness of HSCL). All HSCL rules preserve sound states. Proof. Assume a state (Γ; N ; U ; β; N 0; k; D) is sound. We show that any application of a rule results again in a sound state. For the conflict, resolve and backtrack rules we only show the extended versions, the original versions are similar. ⇒HDSecCidLe. Assume Decide is applicable to (Γ; N ; U ; β; N 0; k; D), yielding a resulting state (Γ, D:Lσk+1; N ; U ; β; N 0; k + 1; D). Then there is a L ∈ C for C ∈ N ∪ U , Lσ is ground and undefined in Γ, and Lσ ≺B β. Also, there can be no active conflict, i.e. D = >. 1, 4 By the precondition, Lσ is undefined in Γ (4). Hence, adding D:Lσ does not make Γ inconsistent (1). 2, 3, 5 Trivially fulfilled by hypothesis.
6, 7 Since D = >, the rules are trivially satisfied.
8 For all literals L0σ0 ∈ Γ, this holds by hypothesis. For Lσ this follows directly from the preconditions of the rule.
Propagate. Assume Propagate is applicable to (Γ; N ; U ; β; N 0; k; D), yielding a resulting ⇒HSCL state (Γ, P:Lσ(C0∨L)δ·σ; N ; U ; β; N 0; k; D). Then, there is a C ∨ L ∈ (N ∪ U ) such that C = C0 ∨ C1, C1σ = Lσ ∨ · · · ∨ Lσ, C0σ does not contain Lσ, δ is the mgu of the literals in C1 and L, (C ∨ L)σ is ground, (C ∨ L)σ ≺B {β}, C0σ is false under Γ, and Lσ is undefined in Γ Also, there can be no active conflict, i.e. D = >.
Exclude. Assume Exclude is applicable to (Γ; N ; U ; β; N 0; k; D), yielding a resulting state ⇒HSCL (Γ, E:Lσk+1:(C0∨L)δ·σ; N ; U ; β; N 0; k + 1; >).
Then, there is a C ∨ L ∈ N 0, C = C0 ∨ C1, C1σ = Lσ ∨ · · · ∨ Lσ, C0σ does not contain Lσ, δ is the mgu of the literals in C1 and L, C0σ is false under Γ, (C ∨ L)σ is ground, (C ∨ L)σ ≺B {β}, and Lσ is undefined in Γ. Also, there can be no active conflict, i.e. D = >.
ConflictE . Assume ConflictE is applicable to (Γ; N ; U ; β; N 0; k; D), yielding a resulting ⇒HSCL state (Γ; N ; U ; β; N 0; k; (C · σ)E). Then, there is a C ∈ N 0 such that Cσ false in Γ. 1-4, 8 Trivially fulfilled by hypothesis, as the trail Γ is not modified.
5 Follows trivially from the induction hypothesis, as U is not modified. 6 Since D = (C · σ)E, this rules is trivially satisfied. 7 It holds that D = (C · σ)E. By the preconditions of ConflictE, Cσ must be false under Γ. Furthermore, since C ∈ N 0 it holds that N 0 |= C. Hence, clearly it is also the case that N ∪ N 0 |= C. Lastly, it remains to show that gnd≺Bβ(N ∪ N 0) |= Cσ. By soundness (8), we know that for all literals Lμ ∈ Γ it holds that Lμ ≺B β. Since Cσ is false in Γ, it must hold that all literals in Cσ are also ≺B β. Combined with N ∪ N 0 |= C, this yields that gnd≺Bβ(N ∪ N 0) |= Cσ. ⇒SHkSiCpL. Assume Skip is applicable to (Γ = Γ0, X:L; N ; U ; β; N 0; k; (D · σ)u), yielding a resulting state (Γ0; N ; U ; β; N 0; k − i; (D · σ)u). By the preconditions of skip, it must hold that comp(L) does not occur in Dσ, and if X ∈ {D, E}, i.e. L is a decision or exclusion literal, then i = 1, else i = 0
Factorize. Assume Factorize is applicable to (Γ; N ; U ; β; N 0; k; ((D ∨L∨L0)·σ)u), yielding ⇒HSCL a resulting state (Γ; N ; U ; β; N 0; k; ((D ∨ L)η · σ)u). Then, Lσ = L0σ and η = mgu(L, L0). 1-4, 8 Trivially fulfilled by hypothesis, as the trail Γ is not modified.
5 Follows trivially from the induction hypothesis, as U is not modified. 6, 7 After the application of Factorize, ((D ∨ L)η · σ)u is the current conflict. W.l.o.g. assume we are in the ((D ∨ L)η · σ)R case, i.e. the factorized clause is a regular conflict. By the hypothesis N |= (D ∨ L ∨ L0). From the preconditions of Factorize, Lσ = L0σ and η = mgu(L, L0). Thus, (D ∨ L ∨ L0)η is an instance of (D ∨ L ∨ L0) and N |= (D ∨ L ∨ L0)η. Since Lη = L0η, (D ∨ L ∨ L0)η |= (D ∨ L0)η. Thus, N |= (D ∨ L)η. By the preconditions, gnd≺Bβ(N ) |= gnd≺Bβ((L ∨ L ∨ L0)σ). Hence, (D ∨ L ∨ L0)σ ≺B {β}. Thus, (D ∨ L)ησ = (D ∨ L)σ ≺B {β}. From this, it follows that gnd≺Bβ(N ) |= gnd≺Bβ((D ∨ L)σ).
Furthermore, (D ∨ L)ησ is false under Γ, since (D ∨ L)ησ = (D ∨ L)σ by the definition of an mgu, and (D ∨ L ∨ L0)σ is already false under Γ.
ResolveE. Assume ResolveE is applicable to (Γ0, X:Lδ(C∨L)·δ; N ; U ; β; N 0; k; ((D∨L0)·σ)E) ⇒HSCL yielding a resulting state (Γ0, X:Lδ(C∨L)·δ; N ; U ; β; N 0; k; ((D ∨ C)η · σδ)E)
By the preconditions of ResolveE, it holds that X ∈ {E, P}. 1-4, 8 Trivially fulfilled by hypothesis, as the trail Γ is not modified.
5 Follows trivially from the induction hypothesis, as U is not modified. 6 Since D = (C · σ)E, this rule is trivially satisfied. 7 After the application of ResolveE, ((D ∨ C)η · σδ)R is the current conflict.
By the hypothesis, (D ∨ L0)σ is false under Γ. In particular, Dσ is false under Γ. By soundness (2), we know that Cδ must be false under Γ as well. Hence, (D ∨ L)ησδ is false under Γ.
By the hypothesis, N ∪ N 0 |= (D ∨ L0). Since (D ∨ L0)η is an instance of (D ∨ L0), it holds that N ∪ N 0 |= (D ∨ L0)η. Furthermore, by soundness (3) we know that N ∪ N 0 |= (C ∨ L) By instantiation with η, it holds that N ∪ N 0 |= (C ∨ L)η. By the soundness of resolution, this implies N ∪ N 0 |= (D ∨ C)η.
Lastly, since (D ∨L0)σ is false in Γ, all occuring literals in {(D ∨L0)σ} ≺B {β}. With similar argumentation, {(C ∨L)δ} ≺B {β}. Hence, in particular, (D∨C)ησδ ≺B {β} and, thus, gnd≺Bβ(N ∪ N 0) |= gnd≺Bβ((D ∨ C)ησδ).
BacktrackE. Assume BacktrackE is applicable to (Γ = Γ0, Γ00; N ; U ; β; N 0; k; ((D∨L)·σ)E), ⇒HSCL yielding a resulting state (Γ0; N ; U ; β; N 0 ∪ {D ∨ L}; k0; >).
particular, this holds for the prefix Γ0 of Γ.
5 Follows trivially from the hypothesis, as neither N nor U are modified. 6, 7 Since after an application of BacktrackR the conflict is resolved, i.e.
rules are trivially satisfied. Γ still fulfil all properties. In
D = >, the ⇒UHnSsCtLuck. Assume Unstuck is applicable to (Γ; N ; U ; β; N 0; k; >), yielding a resulting state ( ; N ; U ; β; N 0 ∪ {C}; 0; >). 1-4, 8 For the empty trail Γ = , all properties follow directly as in Lemma 4.
5 Follows trivially from the hypothesis, as neither N nor U are modified. 6, 7 Since D = > the rules are trivially satisfied.
(Idea) By induction and case analysis for the diferent rules.
The proofs for the classical rules (Propagate, Decide, ConflictR, Skip, Factorize,
ResolveR, and BacktrackR) are similar to classical SCL, as shown in [
The ConflictE rule detects a clause D = (C · σ)E only if C ∈ N 0. Hence, N 0 |= C (7) by definition. Since Cσ is false in Γ, it must consist only of literals ≺B β. Hence, gnd≺Bβ(N ∪ N 0) |= Cσ. The rules ResolveE, Skip, BacktrackE preserve soundness by similar argumentation as classical SCL, only with respect to a clause set N ∪ N 0. Corollary 6. Assume a state (Γ; N ; U ; β; N 0; k; D) resulting from a run. Then, (Γ; N ; U ; β; N 0; k; D) is sound.
Proof. Follows with induction over the size of the run. The base case is handled by Lemma 4, the induction step is contained in Theorem 5.
Definition 7 (Reasonable Runs). A sequence of HSCL rule applications is called a reasonable run if the rule Decide does not enable an immediate application of rule ConflictR or ConflictE.
Definition 8 (Regular HSCL Runs). A sequence of HSCL rule applications is called a regular run if it is a reasonable run and the following hierarchy of rule preferences is respected: • ConflictR, ConflictE and Finish always have priority over every other rule. • Propagate always has priority over Exclude.
• Exclude always has priority over Decide.
Lemma 9 (Correct Termination without Unstuck and Finish). If in a regular run no rule except Unstuck or Finish is applicable to a state (Γ; N ; U ; β; N 0; k; D), then either D = (⊥)R, or D = (⊥)E, or D = > and Γ |= gnd≺Bβ(N ).
Proof. Consider a state (Γ; N ; U ; β; N 0; k; D) where D 6∈ {(⊥)R, (⊥)E}.
Then, D can have one of the following shapes (Case D = (Cσ)R) then one of the rules ResolveR, Skip, Factorize or BacktrackR is applicable. First, consider the case of Γ = ε. By soundness, Cσ must be false under Γ. ( )R, (⊥)E}. Thus, However, the only false clause under ε is ⊥, a contradiction to D 6∈ { ⊥ there is at least one literal on the trail. We split Γ = Γ0, X:L and distinguish on the source X of L: If X = P , i.e. the top level literal is a propagated literal, then either ResolveR or Skip are applicable. In the case that comp(L) occurs in Cσ, ResolveR is applicable. If comp(L) 6∈ Cσ, Skip is applicable.
For X ∈ {E, D}, i.e. the top level literal is a decision or exclusion literal, one of the rules Skip, BacktrackR, or Factorize is applicable. If comp(L) does not occur in Cσ, then Skip can be applied. BacktrackR can be applied in all other cases if C = (C0 ∨ comp(L)), where C0 is of level i0 < k. Note that for BacktrackR there must be a level j that is backtracked to. This level j always exists if all other preconditions are met. Hence, if Skip is not applicable, C is of the shape C0 ∨ comp(L). If C0 is of level k, then Factorize can be applied instead, as C0 must contain another instance of comp(L). Otherwise, C0 is of level i0 < k and BacktrackR can be applied. (Case D = (Cσ)E), then one of ResolveE, Skip, Factorize, or BacktrackE is applicable. This follows similarly to the previous case. (Case D = >) i.e. there is no conflict. Assume there are no undefined ground literals L ≺B β for L ∈ C, C ∈ N ∪ U in Γ. Now, either Γ |= gnd≺Bβ(N ) and thus Γ is already a partial model for N w.r.t. ≺B and β. Otherwise, if Γ 6|= gnd≺Bβ(N ) but all literals are defined, there must be a false clause C ∈ gnd≺Bβ(N ) which can be chosen as a ConflictR instance.
If there is at least one undefined ground literal L ≺B β occuring in N ∪ U , one of the trail building rules Propagate, Decide, Exclude, ConflictR or ConflictE are applicable. Decide on the undefined ground literal L is always possible, as we only consider literals L ∈ C for a C ∈ (N ∪ U ). The application of Decide can, however, be restricted by reasonability or regularity.
If Decide on L is not applicable by reasonability, then Γ, D:L must lead to a direct application of ConflictR or ConflictE. Thus, there is a clause D ∈ N ∪ U ∪ N 0 such that Dσ is false under Γ, D:L. If Dσ is already false under Γ, then either ConflictR or ConflictE are applicable, depending on if D ∈ N ∪ U or D ∈ N 0. Otherwise, D has the shape D0 ∨ D1 where D0 is false under Γ, and D1σ = comp(L) ∨ · · · ∨ comp(L). Since D0 is false under Γ, also D0 ≺B {β} and since L ≺B β it holds that D0 ∨ D1 ≺B {β}. Hence, depending on if D ∈ N ∪ U or D ∈ N 0, either Propagate or Exclude can be applied. If Decide is not applicable by regularity, another rule of Propagate, Exclude, ConflictR or ConflictE must directly be applicable, since regularity only priorizes rule applications. Corollary 10 (Correct Termination of HSCL). If in a run no rules are applicable to a state (Γ; N ; U ; β; N 0; k; D), then either D = (⊥ · σ)R and N is unsatisfiable, or the run has ended with ⇒FHiSnCisLh.
Proof. We instantiate Lemma 9. If D = (⊥ · σ)R, we are done. Similarly, if D = (⊥ · σ)E then Finish can be applied. Otherwise, if D = >, Unstuck can be applied to our state by definition.
Lemma 11 (Regular Conflict Resolution in HSCL). Consider a HSCL conflict state (Γ, X:L; N ; U ; β; N 0; k; (D)u). In a regular run, during conflict resolution, at least the rightmost literal L is resolved with.
Proof. To prove the above claim, we distinguish the two cases how a conflict can be detected in HSCL. For the resulting conflict state, only the six conflict resolution rules Skip, Factorize, ResolveR, ResolveE, BacktrackR and BacktrackE can be applicable. To prove the claim of a resolution happening, we show that only Factorize and Resolve can be applied in a regular run to the resulting conflict state. Since Factorize does not remove literals from the trail and, hence, does not enable the application of any other rule, this shows that a Resolve step must happen at least once before any further conflict resolution rules are applied.
The conflict D was either detected by the ConflictR rule. Then, it is of shape (D)R. Otherwise, the conflict was detected by the ConflictE rule and is of shape (D)E. (Case ConflictR) In a reasonable run, if the rule Decide produced the state (Γ, D:L; N ; U ; β; k; >), ConflictR is not immediately applicable. In case Backtrack produced the state (Γ, X:L; N ; U ; β; k; >), i.e., there is the sequence of rule applications
(Γ00, L, K, Γ1, X : comp(L00σ)k0 ; N ; U 0; β; k0; ((D ∨ L00) · σ)R) ⇒Backtrack (Γ, L; N ; U 0 ∪ (D ∨ L00); β; k; >) then by the definition of Backtrack, the newly learned clause (D ∨ L00) cannot be false with respect to Γ00, L. Thus, ConflictR is not applicable to (D ∨ L00). Furthermore, if there is a conflict to any other clause from N ∪ U , by regularity, ConflictR must have been applied earlier in the run. In summary, L must be either a propagated or excluded literal.
Note that it, also, is not possible for L to be an exclusion literal. If (Γ, E:L; N ; U ; β; k; >) is a state where ConflictR is applicable, then there is also an application of the rule Propagate which produces the state (Γ, P:comp(L); N ; U ; β; k; >). By regularity, Propagate has priority over Exclude and thus, no exclusion can lead to a direct application of ConflictR. Overall, L can neither be a decision nor an exclusion literal.
Then, BacktrackR is not applicable to (Γ, D:L; N ; U ; β; k; (D)R), as it requires L to be a decision or exclusion. Furthermore, L must occur in the conflict clause D. Otherwise, ConflictR could have been applied earlier to (Γ; N ; U ; β; k; >), contradicting regularity. Hence, Skip is not applicable to our state. Overall, only Factorize and Resolve can possibly be applied to our state. Factorize does not modify the trail, and, thus, cannot enable any of the rules Skip or Backtrack. Following from that, at least one application of Resolve must take place in conflict resolution. (Case ConflictE) This case works similar to the previous case. However, BacktrackE cannot be applied from a state (Γ, E:L; N ; U ; β; k; >). Hence, it is allowed for an Exclusion to lead to an application of ConflictE.
Definition 12 (State Induced Ordering). Let (L1, L2, . . . , Ln; N ; U ; N 0; β; k; D) be a sound state of HSCL. The trail induces a total well-founded strict order on the defined literals by
L1 ≺Γ comp(L1) ≺Γ L2 ≺Γ comp(L2) ≺Γ · · · ≺Γ Ln ≺Γ comp(Ln).
We extend ≺Γ to a strict total order on all literals where all undefined literals are larger than comp(Ln). We also extend ≺Γ to a strict total order on ground clauses by multiset extension and also on multisets of ground clauses and overload ≺Γ for all these cases. With Γ we denote the reflexive closure of
≺Γ.
Theorem 13 (Non-redundant Learning in HSCL). Let (Γ; N ; U ; β; N 0; k; (C0 · σ0)u) be the state after an application of ConflictR (resp. ConflictE) in a regular run and let C be the clause learned at the end of the conflict resolution, then C is not redundant with respect to N ∪ U (resp. N ∪ N 0 ∪ U ) and ≺Γ.
Proof. Consider the following fragment of a derivation learning a clause implied by N :
ConflictR ⇒HSCL
{Skip, Fact., Res.}∗ ⇒HSCL (Γ; N ; U ; N 0; β; k; (C0 · σ0)R) (Γ0; N ; U ; N 0; β; k; (C · σ)R)
BacktrackR ⇒HSCL By soundness N ∪ U |= C and Cσ is false under both Γ and Γ0. We prove that Cσ is non-redundant to N ∪ U with respect to ≺Γ.
Assume there is an S ⊆ gnd(N ∪ U ) ΓCσ s.t. S |= Cσ. There must be a clause D ∈ S false under Γ, since all clauses in S have a defined truth value (as all undefined literals are greater in ≺Γ than all defined literals) and if Γ |= S then Γ |= Cσ by transitivity of entailment, a contradiction.
By regularity, Γ must be of the shape Γ = Γ00, LδC∨L·δ, since no application of Decide can lead to an application of the rule ConflictR. Thus, the last applied rule must have been PropagateR. Furthermore, by Lemma 11, Resolve must have resolved at least the rightmost literal Lδ from Γ. Thus, Lδ 6∈ Cσ and comp(Lδ) 6∈ Cσ. Since D ≺Γ Cσ, neither Lδ nor comp(Lδ) may occur in D. However, this is a contradiction, since D is then already false under Γ00 and, thus, must have been chosen as a Conflict instance earlier in a regular run. Overall, there can be no S ⊆ gnd(N ∪ U ) ΓCσ with S |= Cσ. Hence, Cσ is non-redundant to N ∪ U with respect to ≺Γ.
Similarly, this result can be proven for learned clauses to N 0. In contrast, a derivation learning a clause to N 0 with BacktrackE learns only non-redundant clauses with respect to N ∪ U ∪ N 0 and ≺Γ.
Of course, in a regular run, the ordering of foreground literals on the trail will change, i.e., the ordering of Definition 12 will change as well. Thus the non-redundancy property of Lemma 13 reflects the situation at the time of creation of the learned clause. A non-redundancy property holding for an overall run must be invariant against changes on the ordering. However, the ordering of Definition 12 also entails a fixed subset ordering ≺⊆ that is invariant against changes on the overall ordering. This means that our dynamic ordering entails non-redundancy criteria based on subset relations including forward redundancy. From an implementation perspective, this means that learned clauses need not to be tested for forward redundancy. Current resolution or superposition based provers spent a reasonable portion of their time in testing forward redundancy of newly generated clauses. In addition, also tests for backward reduction can be restricted knowing that learned clauses are not redundant.
Theorem 14 (Termination of HSCL). All regular HSCL runs terminate.
Proof. In Theorem 9, we proved that all regular runs which do not use Unstuck terminate. Thus, it is left to show that Unstuck cannot be used infinitely often. Note that every regular use of Unstuck on a state (Γ; N ; U ; β; N 0; k; D) adds a clause C to N 0. However, by Theorem 13, C is not redundant to N ∪ U ∪ N 0 under ≺⊆, which is well-founded. Due to the restriction of all learned clauses to be smaller than {β}, the number of non-redundant ground clauses is finite. Thus, Unstuck cannot be applied infinitely often, and all regular HSCL runs must terminate.
Definition 15 (Stuck States correspond to Partial Models). Let M be a partial model for N under ≺B and β, i.e., M |= gnd≺Bβ(N ) and all ground literals Lσ with Lσ ≺B {β} and L ∈ C for a C ∈ N are defined in M . We call a stuck state (Γ; N ; U ; β; N 0; k; D) corresponding to M if Γ |= M .
Theorem 16 (Exhaustive Stuck State Exploration). Consider a HSCL run that ends with the rule (Γ; N ; U ; β; N 0; k; (⊥)E) ⇒FHiSnCisLh. For all partial models M of N under ≺B and β, a stuck state corresponding to M is eventually explored in such a run.
Proof. Assume there is a partial model M such that no stuck state corresponding to M was visited. For M , by definition M |= gnd≺Bβ(N ) and M 6|= ⊥. Since our run ended with D = (⊥)E, by soundness of the calculus it follows that gnd≺Bβ(N ∪ N 0) |= ⊥ in the final state. However, it cannot be the case that gnd≺Bβ(N ) |= ⊥, since otherwise by transitivity M |= gnd≺Bβ(N ) |= ⊥. Since initially, N 0 = ∅, there must be a HSCL rule application
(Γ; N ; U ; β; N 0; k; D) ⇒HSCL (Γ; N ; U ; β; N 0 ∪ {C}; k; D) such that M |= gnd≺Bβ(N ∪ N 0), but M 6|= gnd≺Bβ(N ∪ N 0 ∪ {C}). This clause C can
BacktrackE or ⇒HUSnsCtLuck: be added by two rules to N 0, ⇒HSCL
BacktrackE, then by soundness already gnd≺Bβ(N ∪ (Case BacktrackE) If C was added by ⇒HSCL N 0) |= Cσ. Thus, if M |= gnd≺Bβ(N ∪ N 0) then also M |= gnd≺Bβ(N ∪ N 0 ∪ {C}), a BacktrackE. contradiction. Hence, it cannot be the case that C was added by ⇒HSCL (Case Unstuck By the preconditions of the rule, (Γ; N ; U ; β; N 0; k; D) must be a stuck state. It remains to show that this state corresponds to M . By Lemma 9, since D 6= (⊥)u, it holds that Γ forms a partial model for N under ≺B and β. Thus, all ground literals Lσ occuring in N with Lσ ≺B β are defined in Γ. Hence, it is only left to prove that Γ |= M . By induction over the trail size, we show that for each literal Lσ ∈ Γ it holds that Lσ ∈ M . For the base case of Γ = , nothing is to do. In the induction step, consider a trail decomposition Γ0 = Γ00, X:Lσ, where Γ0 is a prefix of Γ. Then, X:Lσ was added to the trail by one of the following rules: (Case Unstuck: Decide) Then, Γ0 = Γ00, D:Lσ. By the definition of C = WLi∈decision(Γ) comp(Li), it holds that C = comp(Lσ) ∨ C0, since Lσ is a decision in Γ0. Furthermore, all literals in C are already ground and ≺B β. Hence, gnd≺Bβ({C}) = {comp(Lσ) ∨ C0}. Now, by assumption, M 6|= gnd≺Bβ({C}) and, thus, M 6|= comp(Lσ). Since M is a partial model that defines all ground literals ≺B β, it must hold that Lσ ∈ M . (Case Unstuck: Propagate) This implies that the literal has the form P:Lσ(C0∨L)δ·σ. By the preconditions of Propagate, there is a clause C0 ∨ C1 ∨ L ∈ (N ∪ U ) where C1σ = Lσ ∨ · · · ∨ Lσ, and C0σ is false under Γ00. By our induction hypothesis, we know that all literals defined in Γ00 are consistent with M . Now, assume that comp(Lσ) ∈ M . But now, C0σ is false under M , and C1σ is false as well. Hence, the overall clause (C0 ∨ C1 ∨ L)σ ∈ (N ∪ U ) is falsified under M . If (C0 ∨ C1 ∨ L)σ ∈ N , this directly contradicts the assumption that M is a partial model for N . If the clause is a learned clause, i.e. (C0 ∨ C1 ∨ L)σ ∈ U , by soundness of the calculus (N |= U ), this leads to the same contradiction. (Case Unstuck: Exclude) If the literal has the form E:Lσ(kC0∨L)δ·σ, with the same argumentation as in Propagate, there must be a clause C0 ∨C1 ∨L ∈ N 0 where C1σ = Lσ ∨· · ·∨Lσ, and C0σ is false under Γ00. If we assume that comp(Lσ) ∈ M , this falsifies the clause (C0 ∨ C1 ∨ L)σ under M . However, since this clause is a ground clause ≺B β, this contradicts the assumption that M |= gnd≺Bβ(N 0).
N = ( C1 = ¬P (x) ∨ Q(x)
C3 = ¬R(x) ∨ P (x) ∨ Q(x)
C2 = ¬Q(x) ∨ R(x) ) C4 = R(a) and β, ≺B chosen such that exactly {P (a), ¬P (a), Q(a), ¬Q(a), R(a), ¬R(a)} ≺B {β}. Furthermore, let σ denote the substitution {x 7→ a}. For example, a regular HSCL could explore all partial models in the following way: (P:R(a)C4·{}, D:¬Q(a)1, P:P (a)C3·σ; N ; ∅; β; ∅; 1; (¬P (x) ∨ Q(x) · σ)R) (P:R(a)C4·{}, D:¬Q(a)1, P:P (a)C3·σ; N ; ∅; β; ∅; 1; (¬R(x) ∨ Q(x) ∨ Q(x) · σ)R) (P:R(a)C4·{}, D:¬Q(a)1, P:P (a)C3·σ; N ; ∅; β; ∅; 1; (¬R(x) ∨ Q(x) · σ)R) (ε; N ; ∅; β; ∅; 0; >) (P:R(a)C4·{}; N ; ∅; β; ∅; 0; >) (P:R(a)C4·{}, D:¬Q(a)1; N ; ∅; β; ∅; 1; (¬R(x) ∨ Q(x) · σ))R (P:R(a)C4·{}, P:Q(a)C5·σ, E:¬P (a)1:¬P (a)·{}; N ; U ; β; N 0; 1; >)
Just before any use of Unstuck, the trail forms a partial model under ≺B and β. In this example, the partial models are {P (a), Q(a), R(a)} and {¬P (a), Q(a), R(a)}.
We have shown that simultaneously searching for a refutation and enumerating all potential
models, restricted to the current finite limit, can be efectively combined. There are
several directions for future research. First a procedure that takes a stuck state, or the
overall content of N 0 out of a some state (Γ; N ; U ; β; N 0; k; D) and checks for models for
N . This problem is undecidable, in general. However, for example, the following approach
will work. Take any model candidate out of N 0 and fit it into an efective first-order
model representation formalism, e.g., see [