The two-watched literal scheme for propositional logic is a core component of any eficient CDCL (Conflict Driven Clause Learning) implementation. The family of SCL (Clause Learning from Simple Models) calculi also learns clauses with respect to a partial model assumption built by decisions and propagations similar to CDCL. We show that the well-known two-watched literal scheme can be lifted to SCL for first-order logic.
if the trail is extended to [¬P Q] the clause will be visited again and it will be detected that it propagates R. The general invariant kept by the watched literal scheme for a clause with respect to a trail is: either one of the watched literals is true or if there is a watched false literal then there are no literals in the clause that are true or undefined and not watched. The second benefit is that the two-watched literal scheme invariant is invariant with respect to a shrinking trail, because this just turns true/false literals into undefined literals.
In this paper we lift the propositional two-watched literal scheme to first-order logic without equality. Our trail consists of ground first-order literals and clauses are full firstorder clauses containing implicitly universally quantified variables. Again we want to detect propagating and false clauses by the two-watched literal scheme by only considering the watched literals for trail extensions. For first-order logic the two-watched literals scheme gets more sophisticated because of variable instantiation. The first extension concerns universally quantified variables. Variable instantiation may result in merging literals and diferent clauses may produce identical instances by variable instantiation. For example, the first-order clause R(x, y) ∨ R(a, z) ∨ R(u, b) where a, b are constants and x, y, z, u are variables represents already the propagating ground instance R(a, b). Therefore, our two-watched literal scheme contains the rule FactorizeWatched for considering common instances of watched literals and assumes that all starting units, including units built by instantiation are performed right from the start. Furthermore, updates on the trail induce further instances of clauses, in general, represented by the rule CreateInstance. The second extension addresses potentially infinite trails. Consider the trail [P (a)] and the clause ¬P (x) ∨ P (g(x)). Already this clause produces an infinite trail if propagation is done exhaustively [P (a), P (g(a)), P (g(g(a))), . . . ]. Even in a first-order setting without non-constant function symbols, the trail may grow exponentially with respect to the maximal arity of a predicate symbol. Thus exhaustive propagation cannot be aforded in ifrst-order logic, in general. On the other hand any CDCL style calculus typically breaks if a decided (guessed) literal immediately results in a false clause, a conflict. Our solution to this is a one step propagation look-ahead, represented by the rule DetectPropLiteral and by separating the trail from a set of potentially propagating literals. This way our two-watched literal scheme serves the SCL family of calculi considering a first-order language [3, 4].
The paper is organized as follows: after a section on preliminaries, Section 2, we present the TWFO calculus and prove that it detects all conflicts and propagations, Section 3. Then we present some intuitive example runs of TWFO, Section 4. Next we show in Section 5 that TWFO finds all conflicts and propagations with a minimal amount of overhead: it only needs to check a clause instance for propagations and conflicts if the clause instance was recently derived or if an instance of one of its watched literals was assigned to false. Following this, we show how the interaction between the TWFO calculus and the SCL calculus works in detail. The paper ends with a discussion of the obtained results and directions for future work, Section 7.
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. A substitution σ is the minimally grounding substitution for a term/atom/literal/clause Z if Zσ is ground and there exist no substitutions τ and ρ such that τ ρ = σ and Zτ is ground.
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. The function vars(Z) returns the set of variables in a term/atom/literal/clause/clause set Z.
Let ≺B denote a well-founded, total, strict ordering on ground literals such that for any ground literal L there are only finitely many ground literals K with K ≺B L. For example, a Knuth-Bendix ordering has this property [5]. Let L be a ground literal L and let K be a non-ground literal. Then we write K ≺B L in order to denote that there exists a grounding τ for K such that Kτ ≺B L and C ≺B L in order to denote that there exists a grounding τ for C such that Kστ ≺B L for all K ∈ C.
The Two-Watched Literal Calculus for First-Order Clauses (TWFO) calculus is a lazy twowatched literals scheme for first-order logic without equality. Its purpose is to eficiently detect propagations and all immediate conflicts with respect to a ground partial model M and a set of first-order clauses without equality N . The calculus works on a tuple (M ; β; O; F ; D) called a state where M is a sequence of ground literals called a trail, β is the limit of the state, i.e., a ground literal limiting the considered ground literals and clause instances, O is a set of triples (C; L1; L2) where C is a first-order clause and L1 and L2 are the two literals that are watched in C, F is a set of annotated literals LC;K that can be propagated with the clause instance C, and D is the conflict clause or >. Annotations for literals in F mark the leftmost literal in the trail such that the respective clause propagates and > if the literal is propagated by a (implicit after factoring) unit clause. Annotations are only explicitly written where they are needed or changed.
The literals on the trail M are annotated either with a positive natural number or with a clause instance. These annotations are just the standard annotations used in CDCL [1, 2, 6] and SCL [3, 4]. So a literal annotated with a positive natural number k means that this literal is a decision literal of level k and a literal annotated with a clause instance Cσ means that this literal is a propagated literal and that the clause instance Cσ propagates that literal. A literal L is called assigned with respect to a sequence M of ground literals, if either L ∈ M or comp(L) ∈ M , i.e., it is either true or false, otherwise it is called unassigned. A ground clause {L1, . . . , Ln} is called assigned with respect to a sequence M of ground literals, if either {L1, . . . , Ln} ∩ M 6= ∅ or {comp(L1), . . . , comp(Ln)} ⊆ M , i.e., it is either true or false, otherwise it is called unassigned. A clause C can propagate the literal L with respect to a trail M if C = C0 ∨ L ∨ . . . ∨ L and L is unassigned with respect to M and M |= ¬C0. In the following the watched literals L1 and L2 are considered interchangeably. A literal Lj σ is fresh out of (C; L1; L2) if Lj σ ∈ Cσ, Lj σ 6= L1σ, Lj σ 6= L2σ.
TWFO is called lazy because: (i) TWFO does not check literals for all its instances, i.e., a literal with variables may be watched although all its instances are false. (ii) TWFO does not propagate all propagatable literals it detects but only stores them in the set of detected propagations F ; this is useful for first-order logic because there are infinitely many ground instances per predicate.
For a finite set of clauses N , also called the initial clauses, the start state for TWFO is ( ; β; O; F ; >) where (i) we choose the starting limit β such that C ≺B β for all clauses C ∈ N , (ii) the starting set O consists of exactly one instance (C; L1; L2) for all starting clauses C ∈ N such that L1 ∈ C and L2 ∈ C and L1 6= L2 if possible, and (iii) the starting set F consists of all literals LC,> we can propagate from starting units C in N , including units Cσ = L ∨ · · · ∨ L (where Cσ ≺B β) that we can build by factoring a clause C ∈ N , e.g., if N contains the clause P (x) ∨ P (a), then P (x) ∨ P (a) can be factored to P (a) ∨ P (a) so the starting F must contain the literal P (a) . Note that we only allow non-empty clauses in N . The rules of the calculus are as follows:
(Cσ; Lj σ; Lkσ)}; F ; >)
(M ; β; O ] {(C; L1; L2)}; F ; >) ⇒TWFO (M ; β; O ∪ {(C; L1; L2),
F ; >) provided comp(L1) ∈ M , provided comp(L1σ) ∈ M for some minimal grounding substitution σ, Cσ ≺B β, Lj σ ∈ Cσ, if possible Lj σ ∈ M otherwise if possible Lj σ unassigned otherwise M = M10 comp(Lj σ)M100 and for all literals Lσ ∈ Cσ holds comp(Lσ) 6∈ M100, if comp(L2σ) 6∈ M then Lk = L2 else Lkσ ∈ Cσ and if possible Lkσ 6= Lj σ and if possible Lkσ ∈ M otherwise if possible Lkσ unassigned otherwise M = M20 comp(Lkσ)M200 and for all literals Lσ ∈ Cσ \ {Lj σ} holds comp(Lσ) 6∈ M200, there exists no K1σ, K2σ ∈ Cσ such that (Cσ; K1σ; K2σ) ∈ O.
CreateInstance creates an instance as long as a watched literal gets false by instantiation and the created instance is new.
(M ; β; O ] {(C; L1; L2)}; F ; >) ⇒TWFO (M ; β; O ∪ {(C; Lj ; L2)}; L2 6∈ M , fresh Lj ∈ C where Lj ∈ M or if no such Lj exists Lj is unassigned.
UpdateWatched exchanges a false watched literal as long as the other watched is not true. It is replaced by a true or if such a literal does not exist, an unassigned literal. FactorizeWatched (M ; β; O ] {(C; L1; L2)}; F ; >) ⇒TWFO (M ; β; O0 ∪ {(C; L1; L2), (Cσ; Ljσ; Lkσ)}; F ; >) provided L1σ = L2σ for mgu σ, Cσ ≺B β, fresh Ljσ ∈ Cσ, if possible Ljσ ∈ M otherwise if possible Ljσ unassigned otherwise M = M10 comp(Ljσ)M100 and for all literals Lσ ∈ Cσ holds comp(Lσ) 6∈ M100, if comp(L2σ) 6∈ M then Lk = L2 else Lkσ ∈ Cσ and if possible Lkσ 6= Ljσ and if possible Lkσ ∈ M otherwise if possible Lkσ unassigned otherwise M = M20 comp(Lkσ)M200 and for all literals Lσ ∈ Cσ \ {Ljσ} holds comp(Lσ) 6∈ M200, there exists no K1σ, K2σ ∈ Cσ such that (Cσ; K1σ; K2σ) ∈ O.
DetectPropLiteral (M ; β; O]{(C; L1; L2)}; F ; >) ⇒TWFO (M ; β; O∪{(C; L1; L2)}; F ∪ {L2C;K }; >) provided comp(L1) ∈ M , C = C0 ∨ L2 ∨ . . . ∨ L2, L2 unassigned, M |= ¬C0, M = M 0KM 00 and comp(K) ∈ C, and for all L ∈ C holds comp(L) 6∈ M 00, there is no HD;K0 ∈ F such that Hτ = L2 for some τ with Dτ ≺B β and K0 ∈ M 0K.
So DetectPropLiteral factorizes implicitely on the unassigned literal and propagates as long as the literal is not known to be propagating. Note that we annotate the literal that we propagate with the last literal on the trail that falsifies a literal in the clause. As we will see below in a reasonable strategy this will be the last literal on the trail, that equals comp(L1), except directly after backtracking. Also only in a reasonable strategy the condition that L2 is assigned can only occur directly after backtracking, because DetectPropLiteral is complete for a reasonable strategy, as we will see.
(M ; β; O ] {(C; L1; L2)}; F ; >) ⇒TWFO (M ; β; O ∪ {(C; L1; L2)}; Conflict F ; C) provided comp(L1) ∈ M and comp(L2) ∈ M , M |= ¬C.
ConflictF F ∪ {L1C1, L2C2}; C2σ)
(M ; β; O; F ] {L1C1, L2C2}; >) ⇒TWFO (M L1σC1σ; β; O; there is a grounding unifier σ such that L1σ = comp(L2σ), L1σ 6∈ M , L2σ 6∈ M , C1σ ≺B β and C2σ ≺B β
Note that in the ConflictF rule we do not need the prerequisites that comp(L1σ) 6∈ M and comp(L2σ) 6∈ M hold because comp(L1σ) = L2σ 6∈ M and comp(L2σ) = L1σ 6∈ M hold.
DecLiteral(Lk) (M ; β; O; F ; >) ⇒TWFO (M Lk; β; O; F ; >) provided L ground and not defined in M , there is no L0 ∈ F and grounding substitution σ such that comp(L) = L0σ and Lσ ≺B β PropLiteral(LσCσ) (M ; β; O; F ; >) ⇒TWFO (M LσCσ; β; O; F ; >) provided Lσ ground and not defined in M , there is a literal LC ∈ F , Cσ ≺B β
provided F 0 ⊆ F , for all L0C;K ∈ F 0 holds that L 6= K, for all L0C;K ∈ F \ F 0 holds that L = K, D 6= >
(M L; β; O; F ; D) ⇒TWFO (M ; β; O; F 0; D)
The clause D is the original conflict clause and the clause C in the rule Backtrack(C) below is the clause that we get from resolution in the SCL(T) calculus and learn as a new clause. The learned clause C in Backtrack(C) is a new clause and not an instance of an already existing clause, as we know from the SCL(T) calculus, and is therefore not already in O.
Backtrack(C)
(M ; β; O; F ; D) ⇒TWFO (M ; β; O0 ∪ {(C; L1; L2)}; F 0; >) provided D 6= >, there is a grounding σ such that Cσ can propagate L1σ, Cσ ≺B β there is no τ and M = M 0M 00 where M 00 is non-empty such that Cτ can propagate with respect to M 0, Cτ ≺B β L1, L2 ∈ C, L1 6= L2 if C contains diferent literals, L1 unassigned, if possible L2 unassigned otherwise M = M 0 comp(L2)M 00 and for all literals L ∈ C holds comp(L) 6∈ M 00, if there is a minimal substitution τ with Cτ ≺B β such that Cτ = Lτ ∨ . . . ∨ Lτ then F 0 = F ∪ {Lτ Cτ;>} else F 0 = F
The learned clause C in the Backtrack rule is a clause with a ground instance that propagates directly. So there are no true literals in C and at least one unassigned literal, the one that propagates. All other literals can be unassigned if not ground or false if ground. So we can watch one unassigned literal and the other watched literal can be unassigned or false.
Forget(V )
(M ; β; O; F ; >) ⇒TWFO ( ; β; O0; F 0; >) provided O0 = {(C; K1; K2) ∈ O | C 6∈ V } and F 0 = {LCσ;> ∈ F }
Note that the Forget rule only keeps clause instances annotated with >. Also we only forget clauses when we restart and therefore the rule Forget(V ) not only removes the given clauses V but also restarts with an empty trail and removes all clause instances that are not original instances. It also removes all literals in F that can not be directly propagated from the kept clauses, i.e. literals that can be propagated from factorized unit instances.
Grow(β0) provided β ≺B β0.
( ; β; O; F ; >) ⇒TWFO ( ; β0; O; F ; >)
The TWFO-calculus is part of a larger calculus to ecfiiently detect propagations and conflicts. So the rules DecLiteral( Lk), PropLiteral(LσCσ), RemoveLiteral, Backtrack(C), Forget(V ) and Grow(B0) are rules that are used to update the TWFO-calculus such that it has the same trail, uninstantiated clauses and the same state of the conflict clause, if it is > or not, as the larger calculus. Therefore the rules DecLiteral(Lk), PropLiteral(LσCσ), Backtrack(C), Forget(V ) and Grow(B0) have arguments.
CDCL-like calculi typically only forget clauses after a restart. Hence, Forget(V ) not only removes the clauses V but also restarts with an empty trail and removes all clause instances that are not original instances. It also removes all literals in F that can not be directly propagated from the kept clauses, i.e. literals that can be propagated from factorized unit instances.
The TWFO-calculus is supposed to eficiently detect propagations and conflicts for a larger calculus. The intended larger calculus is the SCL calculus presented in [3], but there are also other calculi to which it could be adapted, e.g., the SCL(T) calculus [4]. The rules DecLiteral(Lk), PropLiteral(LσCσ), RemoveLiteral, Backtrack(C), Forget(V ), and Grow(β0) are rules that are used to update the TWFO calculus such that it has the same trail, uninstantiated clauses and the same state of the conflict clause, if it is > or not, as the larger calculus. Therefore the rules DecLiteral(Lk), PropLiteral(LσCσ), Backtrack(C), Forget(V ), and Grow(β0) have arguments. In order to keep TWFO in sync with the SCL calculus, it has to detect all propagations and conflicts before SCL can change the trail with the rules DecLiteral(Lk) and PropLiteral(LσCσ). We ensure this with the help of a strategy: Definition 1 (Reasonable Strategy). A strategy is called reasonable if the rules CreateInstance, UpdateWatched, FactorizeWatched, DetectPropLiteral, and Conflict are preferred over the rules DecLiteral(Lk) and PropLiteral(LσCσ). To newly created instances by CreateInstance, UpdateWatched, FactorizeWatched, Backtrack(C) these rules are exhaustively applied before any other rule is applied. The rules ConflictF, RemoveLiteral, Backtrack( C) may be applied without further restrictions.
Given this strategy TWFO actually finds all propagations and conflicts before SCL can change the trail. But in order to prove this, we first must ensure some invariants that each state reachable by TWFO from a starting state must fulfill: Definition 2 (Consistent State). A state (M ; β; O; F ; D) is called consistent if all of the following properties hold: 1. Every instance (D; L1; L2) ∈ O is an instance of an initial clause or of a learned clause. 2. For every clause C there is at most one instance (C; L1; L2) ∈ O.
Lemma 1 (Consistency of Starting States). A starting state ( ; β; O; F ; >) for clause set N is consistent.
Lemma 2 (Preservation). Let (M ; β; O; F ; D) be a consistent state. Then any state reachable from (M ; β; O; F ; D) by a sequence of TWFO reasonable rule applications is consistent.
Theorem 1 (Correctness). The following properties hold for a consistent state (M ; β; O; F ; D) and every clause instance (C, L1, L2) ∈ O: 1. If D = > and there is a ground instance Cσ ≺B β such that M |= ¬Cσ, then Conflict or ConflictF is applicable to Cσ after a series of rule applications that consist only of the rules CreateInstance, UpdateWatched, and FactorizeWatched. 2. If D = > and there is a ground instance Cσ ≺B β such that M |= ¬Cσ, then any sequence of rule applications that follows a reasonable strategy will apply one of the rules Conflict, ConflictF, or Forget( V ), before the rules DecLiteral(Lk) and PropLiteral(LσCσ) are applicable. This means if there is a clause in conflict with the trail, then the calculus will detect a conflict clause or forget/reset the trail, before it can propagate or decide new literals onto the trail. 3. If D = > and there is an instance Cσ = C0σ ∨ Lσ ∨ · · · ∨ Lσ where Cσ ≺B β, C0σ is ground, M |= ¬C0σ and Lσ is unassigned with respect to M , and there exists no H ∈ F and substitution τ such that Hτ = Lσ, then DetectPropLiteral is applicable to Lσ or a literal H that can be instantiated to Lσ after a series of rule applications that consist only of the rules CreateInstance, UpdateWatched, and FactorizeWatched.
Let (M ; β; O; F ; >) be a consistent state. Together the above properties show that our calculus is correct. That means in any reasonable run starting from (M ; β; O; F ; >), TWFO tries to exhaustively apply the rules CreateInstance, UpdateWatched, FactorizeWatched, and DetectPropLiteral. This can end in one of three ways (Theorem 1.1 and 1.3): (i) TWFO finds a conflict and interrupts the exhaustive exploration with Conflict or ConflictF, (ii) TWFO finds all literals that can be potentially propagated, and (iii) TWFO interrupts the exhaustive exploration by resetting the trail with rule Forget(V ). Either way, the exhaustive exploration for trail M will terminate (Theorem 1.5). With regard to DecLiteral(Lk) and PropLiteral this means that TWFO will detect any conflicts and any literals that can be potentially propagated before the trail can be extended by DecLiteral(Lk) and PropLiteral (Theorem 1.2 and 1.3). Moreover, all detected conflicts and propagatable literals are sound (Theorem 1.6–8).
We now present some examples that intuitively show how each rule of the TWFO calculus
is used. Note that the trails in the examples are not annotated with the clauses that
propagated the literals to shorten the notation. Also instead of writing down the tuple
(C; L1; L2) for elements in the set O we will annotate watched literals with ∗.
Example 1 (Example run 1). Let N = {(
Then the following is a run of the TWFO calculus:
PropLiteral(R(a,b)) ⇒TWFO
(¬P (a)1Q(a)R(a, b); β; O1; {Q(a)P (a)∨Q(a);¬P (a), ( ; β; O0; ∅; >)
DecLiteral(¬P (a)1) ⇒TWFO
CreateInstance(
DetectPropLit(2) ⇒TWFO
DetectPropLit(3) ⇒TWFO
PropLiteral(Q(a)) ⇒TWFO
DetectPropLit(1.1) ⇒TWFO
Conflict (3) ⇒TWFO
In the last step the notation for the rule Backtrack(P (a) ∨ P (x)) was shortened to Backtrack(4). Note that in the last step where we use the rule Backtrack(P (a) ∨ P (x)) we got the clause P (a) ∨ P (x) just from resolving the conflict clause with the propagating clauses and fully factorizing the resulting clause. We use the original uninstantiated clauses to resolve.
Example 2 (Example run 2). Let the clause set N = {P (x)∨Q(a)∨Q(x), P (x)∨¬Q(x)∨ (¬P (a)1; β; O1; {Q(a)P (a)∨Q(a);¬P (a)}; >) (¬P (a)1; β; O1; {Q(a)P (a)∨Q(a);¬P (a), ¬R(x, b)P (a)∨¬R(x,b);¬P (a)}; >) (¬P (a)1Q(a); β; O1; {Q(a)P (a)∨Q(a);¬P (a), ¬R(x, b)P (a)∨¬R(x,b);¬P (a)}; >) (¬P (a)1Q(a); β; O1; {Q(a)P (a)∨Q(a);¬P (a), ¬R(x, b)P (a)∨¬R(x,b);¬P (a), R(a, y)P (a)∨¬Q(a)∨R(a,y);Q(a)}; >) ¬R(x, b)P (a)∨¬R(x,b);¬P (a), R(a, y)P (a)∨¬Q(a)∨R(a,y);Q(a)}; >) (¬P (a)1Q(a)R(a, b); β; O1; {Q(a)P (a)∨Q(a);¬P (a), ¬R(x, b)P (a)∨¬R(x,b);¬P (a), R(a, y)P (a)∨¬Q(a)∨R(a,y);Q(a)}; P (a) ∨ ¬R(a, b)) (¬P (a)1Q(a); β; O1; {Q(a)P (a)∨Q(a);¬P (a), ¬R(x, b)P (a)∨¬R(x,b);¬P (a), R(a, y)P (a)∨¬Q(a)∨R(a,y);Q(a)}; P (a) ∨ ¬R(a, b)) (¬P (a)1; β; O1; {Q(a)P (a)∨Q(a);¬P (a), ¬R(x, b)P (a)∨¬R(x,b);¬P (a)}; P (a) ∨ ¬R(a, b)) ( ; β; O1; ∅; P (a) ∨ ¬R(a, b)) ( ; β; O2; {P (a)P (a)∨P (x);>}; >) Q(b), ¬Q(a) ∨ ¬Q(b)} be the set of starting clauses and and let ≺B be an ordering and β be a ground literal such that L ≺B β if the predicate of L is P or Q and const(L) ⊆ {a, b}. Let O0, O1, O2, and O3 be sets of clause instances such that
O0 = {(
FactorizeWatched(
DecLiteral(¬P (a)1) ⇒TWFO
CreateInstance(2) ⇒TWFO
DetectPropLit(1.1) ⇒TWFO
PropLiteral(Q(a)) ⇒TWFO
DetectPropLit(2.1) ⇒TWFO
DetectPropLit(3) ⇒TWFO
ConflictF ⇒TWFO (¬P (a)1; β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a)}; >) (¬P (a)1Q(a); β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a)}; >) (¬P (a)1Q(a); β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a), Q(b)P (a)∨¬Q(a)∨Q(b);Q(a)}; >) (¬P (a)1Q(a); β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a), Q(b)P (a)∨¬Q(a)∨Q(b);Q(a), ¬Q(b)¬Q(a)∨¬Q(b);Q(a)}; >) (¬P (a)1Q(a)Q(b); β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a), Q(b)P (a)∨¬Q(a)∨Q(b);Q(a), ¬Q(b)¬Q(a)∨¬Q(b);Q(a)}; ¬Q(a) ∨ ¬Q(b)) (¬P (a)1Q(a); β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a), Q(b)P (a)∨¬Q(a)∨Q(b);Q(a), ¬Q(b)¬Q(a)∨¬Q(b);Q(a)}; ¬Q(a) ∨ ¬Q(b)) (¬P (a)1; β; O2; {Q(a)P (a)∨Q(a)∨Q(a);¬P (a)}; ¬Q(a) ∨ ¬Q(b)) ( ; β; O2; ∅; ¬Q(a) ∨ ¬Q(b)) ( ; β; O3; {P (a)P (a),>}; >)
Here the notation for the rule Backtrack(P (x) ∨ Q(a) ∨ P (y) ∨ Q(y)) was shortened to Backtrack(4). To get the clause for backtracking we resolve ¬Q(a) ∨ ¬Q(b) · ∅ with P (x) ∨ ¬Q(x) ∨ Q(b) · {x 7→ a} resulting in P (x) ∨ ¬Q(x) ∨ ¬Q(a) · {x 7→ a} and then we factorize this to P (a) ∨ ¬Q(a) · ∅. Finally we resolve with P (x) ∨ Q(a) ∨ Q(x) · {x 7→ a} and factorize again.
Example 3 (Example run 3). Let the clause set N = {P (a) ∨ P (b) ∨ Q(a) ∨ R(x), P (a) ∨
¬P (x), P (a) ∨ ¬Q(a)} be the set of starting clauses and and let ≺B be an ordering
and β be a ground literal such that L ≺B β if the predicate of L is P , Q, or R and
const(L) ⊆ {a, b}. Let O0, O1, and O2 be sets of clause instances such that
O0 = {(
DecLiteral(¬P (a)1) ⇒TWFO
UpdateWatched(
DetectPropLit(2) ⇒TWFO
DetectPropLit(3) ⇒TWFO
PropLiteral(¬P (b)) ⇒TWFO
UpdateWatched(
PropLiteral(¬Q(a)) ⇒TWFO
DetectPropLit(
Note that the trail at the end can be extended to a satisfiable valuation as DetectPropLiteral rule was applied to every clause instance and there are no contradicting literals in F .
There are multiple reasons why the original two-watched literals scheme for SAT solving is so eficient. The most important reason is that it only has to check a clause for propagations and conflicts if one of its watched literals was assigned false. This means whenever a new literal L has been added to the trail, it only has to check clauses where comp(L) is a watched literal. For our two-watched literals scheme for first-order logic, we can prove similar properties that we assume will lead to an eficient implementation as in the SAT case.
Lemma 3 (Single Check). Let (M ; β; O0; F0; >) ⇒TWFO (M ; β; O1; F1; >) ⇒TWFO . . . ⇒TWFO (M ; β; On; Fn; >) be a reasonable run starting from a consistent state, where n may be 0 and Forget(V ) was not applied.
1. Then if none of the rules CreateInstance, UpdateWatched, FactorizeWatched, DetectPropLiteral, and Conflict are applicable to clause instance (C, L1, L2) ∈ Oi ∩ Oj in state (M ; β; Oi; Fi; >) then they are also not applicable to (C, L1, L2) in state (M ; β; Oj ; Fj ; >) with 0 ≤ i < j ≤ n. (Hence, TWFO does not have to check a clause instance again after it was fully processed and before the trail has changed.) 2. CreateInstance is applied at most twice to a clause instance C with (C, L1, L2) ∈ Oi. 3. UpdateWatched is applied at most twice to a clause instance C with (C, L1, L2) ∈ Oi independently of which literals are watched. 4. FactorizedWatched and DetectPropLiteral are applied at most once to a clause instance (C, L1, L2) ∈ Oi.
The above lemma guarantees that TWFO only has to check each clause instance once before it changes the trail again. Moreover, for a fixed trail M the maximum number of rule applications per clause instance is at most 6. Note that this does not include the rule applications to clause instances that were derived from this one.
Lemma 4 (Empty Trail Exploration). Let ( ; β; O0; F ; >) be a consistent state. Then CreateInstance, UpdateWatched, DetectPropLiteral and Conflict are not applicable. (However, all clauses have to be checked for potential applications of FactorizeWatched.)
The above lemma guarantees that only FactorizeWatched can be applied on the empty trail.
Lemma 5 (New Literal Exploration). Let (M ; β; O0; F0; >) be a consistent state such that CreateInstance, UpdateWatched, FactorizeWatched, DetectPropLiteral, and Conflict are not applicable in state (M ; β; O0; F ; >). Let (M ; β; O0; F0; >) ⇒TWFO (M L; β; O0; F0; >) ⇒TWFO (M L; β; O1; F1; >) ⇒TWFO . . . ⇒TWFO (M L; β; On; Fn; >) be a reasonable run (where n may be 0): 1. Then in state (M L; β; On; Fn; >) UpdateWatched is only applicable to clause instances (C, L1, L2) ∈ On where comp(L) = L1. 2. Then in state (M L; β; On; Fn; >) CreateInstance, DetectPropLiteral, and Conflict are only applicable to clause instances (C, L1, L2) ∈ On if there exists a substitution σ such that comp(L) = L1σ or if (C, L1, L2) 6∈ O0, i.e., the instance was added or its watched literals were modified after the trail was extended. 3. Then in state (M L; β; On; Fn; >) FactorizeWatched is only applicable to clause instances (C, L1, L2) ∈ On \ O0, i.e., only to those clause instances that where modified or added after the trail was extended.
The above lemma guarantees that after TWFO adds a new literal L to the trail, we only have to check those clause instances (C, L1, L2) for rule applications, where comp(L) is a ground instance of one of its watched literals (i.e., there exists σ and i ∈ 1, 2 so Liσ = L) and those clause instances that were added or modified after L was added to the trail.
Lemma 6 (Backtrack Exploration). Let (M M 0L; β; O0; F00; >) be a consistent state. Let (M M 0L; β; O0; F00; >) ⇒CToWnFflicOt/ConflictF (M M 0L; β; O0; F00; D) ⇒TReWmFoOveLiteral∗
Backtrack(D’) (M ; β; O1; F1; >) be a reasonable run from one application (M ; β; On; Fn0 ; D) ⇒TWFO of Conflict/ConflictF to the first subsequent application of Backtrack( D0). Let (M ; β; O1; F0; >) ⇒TWFO (M ; β; O2; F2; >) ⇒TWFO . . . ⇒TWFO (M ; β; On; Fn; >) be a reasonable run (where n may be 1) and Forget was never applied. Then in state (M L; β; On; Fn; >) UpdateWatched, FactorizeWatched, CreateInstance, DetectPropLiteral, and Conflict are only applicable to clause instances (C, L1, L2) ∈ On where (C, L1, L2) 6∈ O0.
The above lemma guarantees that after TWFO applies Backtrack(D0), we only have to check those clause instances (C, L1, L2) for applications of the rules that were (i) either added by the last Backtrack (i.e., C = D0) or (ii) derived after Backtrack by an application of the rules UpdateWatched, FactorizeWatched, and CreateInstance.
The TWFO calculus is a calculus to help detect propagations and conflicts eficiently for the SCL calculus. So we have to keep certain aspects of the state of both calculi equal, these are the trail, the clauses and the state of the conflict clause, that is if it is > or not. So for all rule applications of SCL we have to show that we can simulate them with rule applications of TWFO. We do this only for a regular run of SCL and a reasonable run of TWFO.
A SCL-state has the form (M ; N ; U ; β; k; D) and a TWFO-state has the form (M 0; β; O; F ; D0). We have to show that we can keep M and M 0 equal as well as that D = > if D0 = > and that for every C ∈ N ∪ U there are L1 and L2 such that (C; L1; L2) ∈ O.
The start state of SCL is ( ; N ; ∅; β; 0; >) and then the start state of TWFO is ( ; β; O; F ; >) such that for every C ∈ N ∪U there are L1 and L2 such that (C; L1; L2) ∈ O holds.
So now we show for every rule application in SCL how we can simulate them with TWFO. First we look at the rule propagate:
Propagate (M LσCδ·σ; N ; U ; β; k; >) (M ; N ; U ; β; k; >) ⇒SCL We know that Lσ is undefined in M . Because we can propagte Lσ in TWFO, either DetectPropLiteral was already applied or can be applied after applications of CreateInstance, UpdateWatched and FactorizeWatched. This holds because DetectPropLiteral is complete, Theorem 1.3, and F always contains all literals that we can propagate from (factorized) unit clauses, Def 2.10. So we can do the following rule applications in TWFO:
CreateInstance, UpdateWatched, FactorizeWatched,∗ (M ; β; O0; F ; >) (⇒TWFO
DetectPropLiteral ⇒TWFO
PropLiteral(Lσ) ⇒TWFO (M LσCσ; β; O0; F 0; >) (M ; β; O0; F ∪ {LσCσ;K }; >))
Note that the rules CreateInstance, UpdateWatched and FactorizeWatched do not add a clause instance (C; L1; L2). So the rule Propagate can be simulated. Moreover, TWFO never adds a literal to F that cannot be propagated by Propagate, Theorem 1.8.
The next rule we look at is the Decide rule:
Decide (M Lσk+1; N ; U ; β; k + 1; >) (M ; N ; U ; β; k; >) ⇒SCL We know that Lσ is undefined in M .
For DecLiteral to be applicable we need that there is no contradicting literal L0 ∈ F such that there is a τ where comp(Lσ) = L0τ . To show this we need that the SCL run is regular. We assume that there is such an L0C ∈ F . From Definition 2.6 we know that C = C0 ∨ L0 ∨ · · · ∨ L0 and M |= ¬C0. Because the SCL run is regular we know that there is no conflict before the application of Decide because Conflict is preferred over every other rule. In a regular run an application of Decide does not create a conflict so there is also no conflict after the application of Decide. So especially M 6|= ¬Cτ and M Lσ 6|= ¬Cτ for all grounding substitutions τ . But because M |= ¬C0 we can follow that M Lσ 6|= ¬L0τ for all grounding substitutions τ . Therefore there is no τ such that comp(Lσ) = L0τ contradicting our assumption.
So we can do the following rule application in TWFO:
DecLiteral(Lσk+1) (M Lσk+1; β; O; F ; >) (M ; β; O; F ; >) ⇒TWFO So the rule Decide can be simulated.
Now we look at the rule Conflict:
Conflict (M ; N ; U ; β; k; D · σ) (M ; N ; U ; β; k; >) ⇒SCL We know that M |= ¬Dσ holds. For TWFO we know from the completeness of the Conflict rule, Theorem 1.1, that Conflict either is applicable or will be applicable after applications of CreateInstance, UpdateWatched and FactorizeWatched. So we can do the following rule applications in TWFO: (M ; β; O; F ; >)
CreateInstance, UpdateWatched, FactorizeWatched,∗ (M ; β; O0; F ; >) ⇒TWFO ⇒CToWnFflicOt (M ; β; O0; F ; Dσ)
So the rule Conflict can be simulated.
The next rules are Resolve and Factorize. Both these rules only change the conflict clause but before the rule application it holds that the conflict clause is not > and this does not change after the rule application. So we do not have to change anything in the state of TWFO.
Then we look at the rule Skip:
(M L; N ; U ; β; k; D · σ) ⇒SSkCiLp (M ; N ; U ; β; l; D · σ) We can just remove a literal with the rule RemoveLiteral in TWFO:
RemoveLiteral (M ; β; O0; F 0; D0) (M L; β; O; F ; D0) ⇒TWFO So we can simulate the rule Skip.
Now we look at the rule Backtrack: (M Ki+1M 0; N ; U ; β; k; (D ∨ L) · σ) ⇒SCL
Backtrack (M LσC·σ; N ; U ∪ {D ∨ L}; β; i; >) In TWFO we first have to remove the literals with RemoveLiteral until the trail is M and then use Backtrack(D ∨ L) to add the new clause to O. Finally we have to apply CreateInstance, UpdateWatched and FactorizeWatched to apply DetectPropLiteral and then we can apply PropLiteral(LσCσ). (M Ki+1M 0; β; O; F ; D0) ⇒TRWemFoOveLiteral,|M0|+1 (M ; β; O1; F 1; D0) ⇒BTaWckFtOrack(D∨L) (M ; β; O2; F 2; >)
CreateInstance, UpdateWatched, FactorizeWatched,∗ (M ; β; O3; F 2; >) ⇒TWFO ⇒TDWeteFcOtPropLiteral (M ; β; O3; F 3; >)
PropLiteral(Lσ(D∨L)σ) (M Lσ(D∨L)σ; β; O3; F 3; >) ⇒TWFO
Note that after the application of Backtrack(D ∨ L) it holds again that for every C ∈ N ∪ U there are L1 and L2 such that (C; L1; L2) ∈ O. Note also that Backtrack checks whether the new clause can be factorized to a unit and adds the resulting literal to F . So Backtrack can also be simulated.
The last rule that we have to look at is the Grow rule:
Backtrack ( ; N ; U ; β0; 0; >) (M ; N ; U ; β; k; >) ⇒SCL To simulate this rule we have to use the rule Forget(∅) to restart and then use Grow(β0).
Forget(∅) (∅; β; O0; F 0; >) ⇒TWFO
Grow(β0) (∅; β0; O0; F 0; >) ⇒TWFO
So Grow can also be simulated.
So all rule applications in the SCL calculus can be simulated with rule applications in the TWFO calculus and therefore the states can stay similar.
We also want to show how we can simulate an application of the rule ConflictF with rules in SCL.
(M ; β; O; F ] {L1C1, L2C2}; >) ⇒TWFO
ConflictF (M L1σC1σ; β; O; F ∪ {L1C1, L2C2}; C2σ) We know that L1σ = comp(L2σ) and L1σ, L2σ 6∈ M hold. From Definition 2.6 we know that C1 = C10 ∨ L1 ∨ · · · ∨ L1 and M |= ¬C10 as well as C2 = C20 ∨ L2 ∨ · · · ∨ L2 and M |= ¬C20 hold. So L1σC1σ can be propagated on the trail and because L1σ = comp(L2σ) holds that M L1σC1σ |= ¬C2σ and therefore Conflict in the SCL calculus is applicable. (M ; N ; U ; β; k; >)
Propagate (M L1σC1σ; N ; U ; β; k; >) ⇒SCL ⇒SCConLflict (M L1σC1σ; N ; U ; β; k; C2σ)
So the ConflictF rule can be simulated with rules in SCL. Note that the only other rule in TWFO that is no rule to synchronize TWFO with SCL and that does afect elements that we have to keep consistent between the two calculi is the Conflict rule. But this can just easily be simulated with an application of the Conflict rule in SCL is a direct implication of the Soundness of the Conflict rule, Theorem 1.6.
We also must guarantee that for a reasonable strategy an application of the rule DecLiteral(Lk) does not create a conflict.
Lemma 7 (DecLiteral does not enable Conflict) . In a reasonable run starting from a consistent start state (∅; β; O; F ; >) an application of the rule DecLiteral(Lk) does not enable an application of the rule Conflict.
We have generalized the two-watched literal principle from propositional logic to a finite domain first-order logic (fixed β). The lifting is involved and we managed to keep the main properties of the principle: first, only watched literals need to be considered for trail changes, and, second, after backtracking no updates are needed except for the newly learned clause. We are confident that these properties will guarantee that an implementation of TWFO for first-order logic will be eficient in practice.
There is still some future work left before we can implement an eficient version of TWFO. First and foremost, we need to develop ecfiient indexing structures for TWFO. For instance, in the propositional case, we put all clauses with watched literal L into a vector watched[L]. This allows us to eficiently iterate through all clauses that need to be checked when the negation of watched literal comp(L) is added to the trail. However, when comp(L) is added to the trail in the first-order case, it is not enough to just check all clause instances C where L is watched. Instead, we have to check all clause instances C with a watched literal L0 that can be instantiated to L (i.e., there exists τ with L0τ = L). So we need an eficient data structure that finds all watched literals that can be instantiated to L. Work on indexing in first-order logic can here be a good starting point [7].
Although model building through trails has been considered in first-order logic, e.g. [ 8, 9, 10], we are not aware of any work adapting the propositional two-watched literal principle to this setting. This might also be due to the fact that exhaustive propagation, as done in propositional logic, cannot be aforded in more expressive logics [ 3] and therefore the two-watched literal scheme needs an additional laziness component, as suggested in this work. [2] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaf: Engineering an eficient sat solver, in: Design Automation Conference, 2001. Proceedings, ACM, 2001, pp. 530–535. [3] A. Fiori, C. Weidenbach, Scl clause learning from simple models, in: P. Fontaine (Ed.), 27th International Conference on Automated Deduction, CADE-27, volume 11716 of LNAI, Springer, 2019, pp. 233–249. [4] M. Bromberger, A. Fiori, C. Weidenbach, Deciding the bernays-schoenfinkel fragment over bounded diference constraints by simple clause learning over theories, in: F. Henglein, S. Shoham, Y. Vizel (Eds.), Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, Springer, 2021, pp. 511–533. [5] D. E. Knuth, P. B. Bendix, Simple word problems in universal algebras, in: I. Leech (Ed.), Computational Problems in Abstract Algebra, Pergamon Press, 1970, pp. 263–297. [6] A. Biere, M. Heule, H. van Maaren, T. Walsh (Eds.), Handbook of Satisfiability Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2021. [7] R. Nieuwenhuis, T. Hillenbrand, A. Riazanov, A. Voronkov, On the evaluation of indexing techniques for theorem proving, in: R. Goré, A. Leitsch, T. Nipkow (Eds.), Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, volume 2083 of LNCS, Springer, 2001, pp. 257–271. [8] P. Baumgartner, A. Fuchs, C. Tinelli, Lemma learning in the model evolution calculus, in: LPAR, volume 4246 of Lecture Notes in Computer Science, Springer, 2006, pp. 572–586. [9] K. Korovin, Inst-gen - A modular approach to instantiation-based automated reasoning, in: A. Voronkov, C. Weidenbach (Eds.), Programming Logics - Essays in Memory of Harald Ganzinger, volume 7797 of Lecture Notes in Computer Science, Springer, 2013, pp. 239–270. [10] M. P. Bonacina, U. Furbach, V. Sofronie-Stokkermans, On first-order model-based reasoning, in: N. Martí-Oliet, P. C. Ölveczky, C. L. Talcott (Eds.), Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Computer Science, Springer, 2015, pp. 181–204.