Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

TL;DR

Scavenger 0.1 is a novel first-order logic theorem prover utilizing conflict resolution calculus, combining unit propagation, decision literals, and conflict-driven clause learning to enhance proof search efficiency.

Contribution

It introduces the first theorem prover based on conflict resolution calculus for pure first-order logic without equality, integrating new inference rules.

Findings

Demonstrates the effectiveness of conflict resolution in first-order theorem proving

Provides a new framework combining unit propagation and clause learning

Shows potential improvements over traditional methods

Abstract

This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.

Figures

Tables

Table 1. Table 1: Number of problems solved by each prover

	Problems Solved
Prover	EPR	All
PEPR-0.0ps	432	432
GrAnDe-1.1	447	447
Paradox-3.0	467	506
ZenonModulo-0.4.1	315	628
TD-Scavenger	350	695
PD-Scavenger	252	782
Geo-III-2016C	344	840
EP-Scavenger	349	891
Metis-2.3	404	950
Z3-4.4.1	507	1027
Zipperpin-FOF-0.4	400	1029
Otter-3.3	362	1068

Equations

$$\ell \sigma \text{lx@proof@logical@and}{\ell }_1\dots {\ell }_n\overline{{\ell }_1^{\prime }}\vee \dots \vee \overline{{\ell }_n^{\prime }}\vee \ell$$

$$\perp \text{lx@proof@logical@and}\ell \overline{{\ell }^{\prime }}$$

$$(\overline{{\ell }_1}{\sigma }_1^1\vee \dots \vee \overline{{\ell }_1}{\sigma }_{m_1}^1)\vee \dots \vee (\overline{{\ell }_n}{\sigma }_1^n\vee \dots \vee \overline{{\ell }_n}{\sigma }_{m_n}^n)\perp \text{lx@proof@logical@and}[{\ell }_1{]}^{\stackrel{i}{1}}[{\ell }_n{]}^{\stackrel{i}{n}}$$

Full text

1 Introduction

The outstanding efficiency of current propositional Sat-solvers naturally raises the question of whether it would be possible to employ similar ideas for automating first-order logical reasoning. The recent Conflict Resolution calculus111Not to be confused with the homonymous calculus for linear rational inequalities [17]. (CR) [25] can be regarded as a crucial initial step to answer this question. From a proof-theoretical perspective, CR generalizes (to first-order logic) the two main mechanisms on which modern Sat-solvers are based: unit propagation and conflict-driven clause learning. The calculus is sound and refutationally complete, and CR derivations are isomorphic to implication graphs.

This paper goes one step further by defining proof search algorithms for CR. Familiarity with the propositional CDCL procedure [18] is assumed, even though it is briefly sketched in Section 2. The main challenge in lifting this procedure to first-order logic is that, unlike in propositional logic, first-order unit propagation does not always terminate and true clauses do not necessarily have uniformly true literals (cf. Section 4). Our solutions to these challenges are discussed in Section 5 and Section 6, and experimental results are presented in Section 7.

Related Work:

CR’s unit-propagating resolution rule can be traced back to unit-resulting resolution [20]. Other attempts to lift DPLL [13, 19] or CDCL [18] to first-order logic include Model Evolution [2, 5, 3, 4], Geometric Resolution [24], Non-Redundant Clause Learning [1] and the Semantically-Guided Goal Sensitive procedure [6, 7, 8, 9]. A brief summary of these approaches and a comparison with CR can be found in [25]. Furthermore, many architectures [12, 15, 16, 29, 11] for first-order and higher-order theorem proving use a Sat-solver as a black box for propositional reasoning, without attempting to lift it; and Semantic Resolution [26, 14] is yet another related approach that uses externally built first-order models to guide resolution.

2 Propositional CDCL

During search in the propositional case, a Sat-solver keeps a model (a.k.a. trail) consisting of a (conjunctive) list of decision literals and propagated literals. Literals of unit clauses are automatically added to the trail, and whenever a clause has only one literal that is not falsified by the current model, this literal is added to the model (thereby satisfying that clause). This process is known as unit-propagation. If unit propagation reaches a conflict (i.e. a situation where the dual of a literal already contained in the model would have to be added to it), the Sat-solver backtracks, removing from the model decision literals responsible for the conflict (as well as propagated literals entailed by the removed decision literals) and deriving, or learning, a conflict-driven clause consisting222In practice, optimizations (e.g. 1UIP) are used, and more sophisticated clauses, which are not just disjunctions of duals of the decision literals involved in the conflict, can be derived. But these optimizations are inessential to the focus of this paper. of duals of the decision literals responsible for the conflict (or the empty clause, if there were no decision literals). If unit propagation terminates without reaching a conflict and all clauses are satisfied by the model, then the input clause set is satisfiable. If some clauses are still not satisfied, the Sat-solver chooses and assigns another decision literal, adding it to the trail, and satisfying the clauses that contain it.

3 Conflict Resolution

The inference rules of the conflict resolution calculus CR are shown in Figure 1. The unit propagating resolution rule is a chain of restricted resolutions with unit clauses as left premises and a unit clause as final conclusion. Decision literals are denoted by square brackets, and the conflict-driven clause learning rule infers a new clause consisting of negations of instances of decision literals used to reach a conflict (a.k.a. the empty clause $\bot$). A clause learning inference is said to discharge the decision literals that it uses. As in the resolution calculus, CR derivations are directed acyclic graphs that are not necessarily tree-like. A CR refutation is a CR derivation of $\bot$ with no undischarged decision literals.

From a natural deduction point of view, a unit propagating resolution rule can be regarded as a chain of implication eliminations taking unification into account, whereas decision literals and conflict driven clause learning are reminiscent of, respectively, assumptions and chains of negation introductions, also generalized to first-order through unification. Therefore, CR can be considered a first-order hybrid of resolution and natural deduction.

4 Lifting Challenges

First-order logic presents many new challenges for methods based on propagation and decisions, of which the following can be singled out:

(1) non-termination of unit-propagation:

In first-order logic, unit propagation may never terminate. For example, the clause set $\{p(a),\neg p(X)\lor p(f(X)),q\lor r,\neg q\lor r,q\lor\neg r,\neg q\lor\neg r\}$ is clearly unsatisfiable, because there is no assignment of $p$ and $q$ to true or false that would satisfy all the last four clauses. However, unit propagation would derive the following infinite sequence of units, by successively resolving $\neg p(X)\lor p(f(X))$ with previously derived units, starting with $p(a)$: $\{p(f(a)),p(f(f(a))),\ldots,p(f(\ldots(f(a))\ldots)),\ldots\}$. Consequently, a proof search strategy that would wait for unit propagation to terminate before making decisions would never be able to conclude that the given clause set is unsatisfiable.

(2) absence of uniformly true literals in satisfied clauses:

While in the propositional case, a clause that is true in a model always has at least one literal that is true in that model, this is not so in first-order logic, because shared variables create dependencies between literals. For instance, the clause set $\{p(X)\vee q(X),\neg p(a),p(b),q(a),\neg q(b)\}$ is satisfiable, but there is no model where $p(X)$ is uniformly true (i.e. true for all instances of $X$) or $q(X)$ is uniformly true.

(3) propagation without satisfaction:

In the propositional case, when only one literal of a clause is not false in the model, this literal is propagated and added to the model, and the clause necessarily becomes true in the model and does not need to be considered in propagation anymore, at least until backtracking. In the first-order case, on the other hand, a clause such as $p(X)\vee q(X)$ would propagate the literal $q(a)$ in a model containing $\neg p(a)$, but $p(X)\vee q(X)$ does not become true in a model where $q(a)$ is true. It must remain available for further propagations. If, for instance, the literal $\neg p(b)$ is added to the model, the clause will be used again to propagate $q(b)$.

(4) quasi-falsification without propagation:

A clause is quasi-falsified by a model iff all but one of its literals are false in the model. In first-order logic, in contrast to propositional logic, it is not even the case that a clause will necessarily propagate a literal when only one of its literals is not false in the model. For instance, the clause $p(X)\vee q(X)\vee r(X)$ is quasi-falsified in a model containing $\neg p(a)$ and $\neg q(b)$, but no instance of $r(X)$ can be propagated.

The first two challenges affect search in a conceptual level, and solutions are discussed in Section 5. The last two prevent a direct first-order generalization of the data structures (e.g. watched literals) that make unit propagation so efficient in the propositional case. Partial solutions are discussed in Section 6.

5 First-Order Model Construction and Proof Search

Despite the fundamental differences between propositional and first-order logic described in the previous section, the first-order algorithms presented aim to adhere as much as possible to the propositional procedure sketched in the Section 2. As in the propositional case, the model under construction is a (conjunctive) list of literals, but literals may now contain (universal) variables. If a literal $\ell[X]$ is in a model $M$, then any instance $\ell[t]$ is said to be true in $M$. Note that checking that a literal $\ell$ is true in a model $M$ is more expensive in first-order logic than in propositional logic: whereas in the latter it suffices to check that $\ell$ is in $M$, in the former it is necessary to find a literal $\ell^{\prime}$ in $M$ and a substitution $\sigma$ such that $\ell=\ell^{\prime}\sigma$. A literal $\ell$ is said to be strongly true in a model $M$ iff $\ell$ is in $M$.

There is a straightforward solution for the second challenge (i.e. the absence of uniformly true literals in satisfied clauses): a clause is satisfied by a model $M$ iff all its relevant instances have a literal that is true in $M$, where an instance is said to be relevant if it substitutes the clause’s variables by terms that occur in $M$. Thus, for instance, the clause $p(X)\vee q(X)$ is satisfied by the model $[\neg p(a),p(b),q(a),\neg q(b)]$, because both relevant instances $p(a)\vee q(a)$ and $p(b)\vee q(b)$ have literals that are true in the model. However, this solution is costly, because it requires the generation of many instances. Fortunately, in many (though not all) cases, a satisfied clause will have a literal that is true in $M$, in which case the clause is said to be uniformly satisfied. Uniform satisfaction is cheaper to check than satisfaction. However, a drawback of uniform satisfaction is that the model construction algorithm may repeatedly attempt to satisfy a clause that is not uniformly satisfied, by choosing one of its literals as a decision literal. For example, the clause $p(X)\vee q(X)$ is not uniformly satisfied by the model $[\neg p(a),p(b),q(a),\neg q(b)]$. Without knowing that this clause is already satisfied by the model, the procedure would try to choose either $p(X)$ or $q(X)$ as decision literal. But both choices are useless decisions, because they would lead to conflicts with conflict-driven clauses equal to a previously derived clause or to a unit clause containing a literal that is part of the current model. A clause is said to be weakly satisfied by a model $M$ if and only if all its literals are useless decisions.

Because of the first challenge (i.e. the non-termination of unit-propagation in the general first-order case), it is crucial to make decisions during unit propagation. In the example given in item 1 of Section 4, for instance, deciding $q$ at any moment would allow the propagation of $r$ and $\neg r$ (respectively due to the 4th and 6th clauses), triggering a conflict. The learned clause would be $\neg q$ and it would again trigger a conflict by the propagation of $r$ and $\neg r$ (this time due to the 3rd and 5th clauses). As this last conflict does not depend on any decision literal, the empty clause is derived and thus the clause set is refuted. The question is how to interleave decisions and propagations. One straightforward approach is to keep track of the propagation depth444Because of the isomorphism between implication graphs and subderivations in Conflict Resolution [25], the propagation depth is equal to the corresponding subderivation’s height, where initial axiom clauses and learned clauses have height [math] and the height of the conclusion of a unit-propagating resolution inference is $k+1$ where $k$ is the maximum height of its unit premises. in the implication graph: any decision literal or literal propagated by a unit clause has propagation depth [math]; any other literal has propagation depth $k+1$, where $k$ is the maximum propagation depth of its predecessors. Then propagation is performed exhaustively only up to a propagation depth threshold $h$. A decision literal is then chosen and the threshold is incremented. Such eager decisions guarantee that a decision will eventually be made, even if there is an infinite propagation path. However, eager decisions may also lead to spurious conflicts generating useless conflict-driven clauses. For instance, the clause set $\{1:p(a),2:\neg p(X)\vee p(f(X)),3:\neg p(f(f(f(f(f(f(a))))))),4:\neg r(X)\vee q(X),5:\neg q(g(X))\vee\neg p(X),6:z(X)\vee r(X)\}$ (where clauses have been numbered for easier reference) is unsatisfiable, because a conflict with no decisions can be obtained by propagating $p(a)$ (by 1), and then $p(f(a))$, $p(f(f(a)))$, …, $p(f(f(f(f(f(f(a)))))))$, (by 2, repeatedly), which conflicts with $\neg p(f(f(f(f(f(f(a)))))))$ (by 3). But the former propagation has depth $6$. If the propagation depth threshold is lower than $6$, a decision literal is chosen before that conflict is reached. If $r(X)$ is chosen, for example, in an attempt to satisfy the sixth clause, there are propagations (using $r(X)$ and clauses 1, 4, 5 and 6) with depth lower than the threshold and reaching a conflict that generates the clause $\neg r(g(a))$, which is useless for showing unsatisfiability of the whole clause set. This is not a serious issue, because useless clauses are often generated in conflicts with non-eager decisions as well. Nevertheless, this example suggests that the starting threshold and the strategy for increasing the threshold have to be chosen wisely, since the performance may be sensitive to this choice.

Interestingly, the problem of non-terminating propagation does not manifest in fragments of first-order logic where infinite unit propagation paths are impossible. A well-known and large fragment is the effectively propositional (a.k.a. Bernays-Schönfinkel) class, consisting of sentences with prenex forms that have an $\exists^{*}\forall^{*}$ quantifier prefix and no function symbols. For this fragment, a simpler proof search strategy that only makes decisions when unit propagation terminates, as in the propositional case, suffices. Infinite unit propagation paths do not occur in the effectively propositional fragment because there are no function symbols and hence the term depth555The depth of constants and variables is zero and the depth of a complex term is $k+1$ when $k$ is the maximum depth of its proper subterms. does not increase arbitrarily. Whenever the term depth is bounded, infinite unit propagation paths cannot occur, because there are only finitely many literals with bounded term depth (given the finite set of constant, function and predicate symbols with finite arity occurring in the clause set).

The insight that term depth is important naturally suggests a different approach for the general first-order case: instead of limiting the propagation depth, limit the term depth instead, allowing arbitrarily long propagations as long as the term depth of the propagated literals are smaller than the current term depth threshold. A literal is propagated only if its term depth is smaller than the threshold. New decisions are chosen when the term-depth-bounded propagation terminates and there are still clauses that are not uniformly satisfied. As before, eager decisions may lead to spurious conflicts, but bounding propagation by term depth seems intuitively more sensible than bounding it by propagation depth.

6 Implementation Details

Scavenger is implemented in Scala and its source code and usage instructions are available in https://gitlab.com/aossie/Scavenger. Its packrat combinator parsers are able to parse TPTP CNF files [28]. Although Scavenger is a first-order prover, every logical expression is converted to a simply typed lambda expression, implemented by the abstract class E with concrete subclasses Sym, App and Abs for, respectively, symbols, applications and abstractions. A trait Var is used to distinguish variables from other symbols. Scala’s case classes are used to make E behave like an algebraic datatype with (pattern-matchable) constructors. The choice of simply typed lambda expressions is motivated by the intention to generalize Scavenger to multi-sorted first-order logic and higher-order logic and support TPTP TFF and THF in the future. Every clause is internally represented as an immutable two-sided sequent consisting of a set of positive literals (succedent) and a set of negative literals (antecedent).

When a problem is unsatisfiable, Scavenger can output a CR refutation internally represented as a collection of ProofNode objects, which can be instances of the following immutable classes: UnitPropagatingResolution, Conflict, ConflictDrivenClauseLearning, Axiom, Decision. The first three classes correspond directly to the rules shown in Figure 1. Axiom is used for leaf nodes containing input clauses, and Decision represents a fictive rule holding decision literals. Each class is responsible for checking, typically through require statements, the soundness conditions of its corresponding inference rule. The Axiom, Decision and ConflictDrivenClauseLearning classes are less than 5 lines of code each. Conflict and UnitPropagatingResolution are respectively 15 and 35 lines of code. The code for analyzing conflicts, traversing the subderivations (conflict graphs) and finding decisions that contributed to the conflict, is implemented in a superclass, and is 17 lines long.

The following three variants of Scavenger were implemented:

• •

EP-Scavenger: aiming at the effectively propositional fragment, propagation is not bounded, and decisions are made only when propagation terminates.

• •

PD-Scavenger: Propagation is bounded by a propagation depth threshold starting at [math]. Input clauses are assigned depth [math]. Derived clauses and propagated literals obtained while the depth threshold is $k$ are assigned depth $k+1$. The threshold is incremented whenever every input clause that is neither uniformly satisfied nor weakly satisfied is used to derive a new clause or to propagate a new literal. If this is not the case, a decision literal is chosen (and assigned depth $k+1$) to uniformly satisfy one of the clauses that is neither uniformly satisfied nor weakly satisfied.

• •

TD-Scavenger: Propagation is bounded by a term depth threshold starting at [math]. When propagation terminates, a stochastic choice between either selecting a decision literal or incrementing the threshold is made with probability of 50% for each option. Only uniform satisfaction of clauses is checked.

The third and fourth challenges discussed in Section 4 are critical for performance, because they prevent a direct first-order generalization of data structures such as watched literals, which enables efficient detection of clauses that are ready to propagate literals. Without knowing exactly which clauses are ready to propagate, Scavenger (in its three variants) loops through all clauses with the goal of using them for propagation. However, actually trying to use a given clause for propagation is costly. In order to avoid this cost, Scavenger performs two quicker tests. Firstly, it checks whether the clause is uniformly satisfied (by checking whether one of its literals belongs to the model). If it is, then the clause is dismissed. This is an imperfect test, however. Occasionally, some satisfied clauses will not be dismissed, because (in first-order logic) not all satisfied clauses are uniformly satisfied. Secondly, for every literal $\ell$ of every clause, Scavenger keeps a set of decision literals and propagated literals that are unifiable with $\ell$. A clause $c$ is quasi-falsified when at most one literal of $c$ has an empty set associated with it. This is a rough analogue of watched literals for detecting quasi-falsified clauses. Again, this is an imperfect test, because (in first-order logic) not all quasi-falsified clauses are ready to propagate. Despite the imperfections of these tests, they do reduce the number of clauses that need to be considered for propagation, and they are quick and simple to implement.

Overall, the three variants of Scavenger listed above have been implemented concisely. Their main classes are only 168, 342 and 176 lines long, respectively, and no attempt has been made to increase efficiency at the expense of the code’s readability and pedagogical value. Premature optimization would be inappropriate for a first proof-of-concept.

Scavenger still has no sophisticated backtracking and restarting mechanism, as propositional Sat-solvers do. When Scavenger reaches a conflict, it restarts almost completely: all derived conflict-driven clauses are kept, but the model under construction is reset to the empty model.

7 Experiments

Experiments were conducted666Raw experimental data are available at https://doi.org/10.5281/zenodo.293187. in the StarExec cluster [27] to evaluate Scavenger’s performance on TPTP v6.4.0 benchmarks in CNF form and without equality. For comparison, all other 21 provers available in StarExec’s TPTP community and suitable for CNF problems without equality were evaluated as well. For each job pair, the timeouts were 300 CPU seconds and 600 Wallclock seconds.

Table 1 shows how many of the 1606 unsatisfiable CNF problems and 572 effectively propositional (EPR) unsatisfiable CNF problems each theorem prover solved; and figures 2 and 3 shows the performance in more detail. For a first implementation, the best variants of Scavenger show an acceptable performance. All variants of Scavenger outperformed PEPR, GrAnDe, DarwinFM, Paradox and ZenonModulo; and EP-Scavenger additionally outperformed Geo-III. On the effectively propositional propblems, TD-Scavenger outperformed LEO-II, ZenonModulo and Geo-III, and solved only 1 problem less than SOS-2.0 and 12 less than Otter-3.3. Although Otter-3.3 has long ceased to be a state-of-the-art prover and has been replaced by Prover9, the fact that Scavenger solves almost as many problems as Otter-3.3 is encouraging, because Otter-3.3 is a mature prover with 15 years of development, implementing (in the C language) several refinements of proof search for resolution and paramodulation (e.g. orderings, set of support, splitting, demodulation, subsumption) [21, 22], whereas Scavenger is a yet unrefined and concise implementation (in Scala) of a comparatively straightforward search strategy for proofs in the Conflict Resolution calculus, completed in slightly more than 3 months. Conceptually, Geo-III (based on Geometric Resolution) and Darwin (based on Model Evolution) are the most similar to Scavenger. While Scavenger already outperforms Geo-III, it is still far from Darwin. This is most probably due to Scavenger’s current eagerness to restart after every conflict, whereas Darwin backtracks more carefully (cf. Sections 6 and 8). Scavenger and Darwin also treat variables in decision literals differently. Consequently, Scavenger detects more (and non-ground) conflicts, but learning conflict-driven clauses can be more expensive, because unifiers must be collected from the conflict graph and composed.

EP-Scavenger solved 28.2% more problems than TD-Scavenger and 13.9% more than PD-Scavenger. This suggests that non-termination of unit-propagation is an uncommon issue in practice: EP-Scavenger is still able to solve many problems, even though it does not care to bound propagation, whereas the other two variants solve fewer problems because of the overhead of bounding propagation even when it is not necessary. Nevertheless, there were 28 problems solved only by PD-Scavenger and 26 problems solved only by TD-Scavenger (among Scavenger’s variants). EP-Scavenger and PD-Scavenger can solve 9 problems with TPTP difficulty rating 0.5, all from the SYN and FLD domains. 3 of the 9 problems were solved in less than 10 seconds.

8 Conclusions and Future Work

Scavenger is the first theorem prover based on the new Conflict Resolution calculus. The experiments show a promising, albeit not yet competitive, performance.

A comparison of the performance of the three variants of Scavenger shows that it is non-trivial to interleave decisions within possibly non-terminating unit-propagations, and further research is needed to determine (possibly in a problem dependent way) optimal initial depth thresholds and threshold incrementation strategies. Alternatively, entirely different criteria could be explored for deciding to make an eager decision before propagation is over. For instance, decisions could be made if a fixed or dynamically adjusted amount of time elapses.

The performance bottleneck that needs to be most urgently addressed in future work is backtracking and restarting. Currently, all variants of Scavenger restart after every conflict, keeping derived conflict-driven clauses but throwing away the model construct so far. They must reconstruct models from scratch after every conflict. This requires a lot of repeated re-computation, and therefore a significant performance boost could be expected through a more sensible backtracking strategy. Scavenger’s current naive unification algorithm could be improved with term indexing [23], and there might also be room to improve Scavenger’s rough first-order analogue for the watched literals data structure, even though the first-order challenges make it unlikely that something as good as the propositional watched literals data structure could ever be developed. Further experimentation is also needed to find optimal values for the parameters used in Scavenger for governing the initial thresholds and their incrementation policies.

Scavenger’s already acceptable performance despite the implementation improvement possibilities just discussed above indicates that automated theorem proving based on the Conflict Resolution calculus is feasible. However, much work remains to be done to determine whether this approach will eventually become competitive with today’s fastest provers.

Acknowledgments:

We thank Ezequiel Postan for his implementation of TPTP parsers for Skeptik [10], which we have reused in Scavenger. We are grateful to Albert A. V. Giegerich, Aaron Stump and Geoff Sutcliffe for all their help in setting up our experiments in StarExec. This research was partially funded by the Australian Government through the Australian Research Council and by the Google Summer of Code 2016 program. Daniyar Itegulov was financially supported by the Russian Scientific Foundation (grant 15-14-00066).