Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

An Erratum to this article was published on 25 September 2017

This article has been updated

Abstract

This paper defines the (first-order) conflict resolution calculus: an extension of the resolution calculus inspired by techniques used in modern Sat-solvers. The resolution inference rule is restricted to (first-order) unit propagation and the calculus is extended with a mechanism for assuming decision literals and with a new inference rule for clause learning, which is a first-order generalization of the propositional conflict-driven clause learning procedure. The calculus is sound (because it can be simulated by natural deduction) and refutationally complete (because it can simulate resolution), and these facts are proven in detail here.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Change history

  • 25 September 2017

    An erratum to this article has been published.

Notes

  1. CR is based on resolution instead of superposition, because superposition’s ordering-based refinements would restrict unit-propagation and the selection of decision literals. In Sat-solvers unit-propagation is unrestricted (because it is very effective anyway) and the best literal selection strategies are not based on orderings. By extending unrestricted resolution, CR remains general enough to admit the strategies used by Sat-solvers.

  2. By Herbrand’s theorem, a finite number of instances would suffice in the case of an unsatisfiable clause set. As the logic is undecidable, however, there is no way to know in advance how many “several” might be.

  3. This rule is also known as unit-resulting resolution [24, 25]. Here we use the name unit-propagating resolution instead in order to make the connection with the technique of unit-propagation more explicit.

  4. As mentioned in Sect. 3, modern Sat-solvers implement optimized clause learning procedures that may also contain duals of propagated literals. A modification of CR ’s \(\mathbf {cl}\) inference rule to cover more sophisticated clause learning procedures is briefly discussed in Sect. 4.2.

  5. The usual definition of UIP in terms of conflict graphs also relies on the notion of decision level of assigned literals and requires that the propagated literal be assigned at the current decision level. Therefore, our definition is slightly more general. This is intentional. The notion of decision level, which keeps track of the order in which decision literals were assigned, is beyond the purely proof-theoretical scope of this paper, as it relates to particular proof search and backtracking procedures.

  6. CND is a calculus for classical logic: the law of excluded middle can be easily derived with a single application of implication introduction. Interestingly, its classicality is implicit in the use of involutive negation and the equivalence involving disjunctions and implications.

  7. Since we assume that distinct clauses in \(\psi '\) do not share variables and \(\psi '\) is tree-like, we do not need to worry about variable clashes in the composition of all substitutions. The topological order is needed because a variable x introduced by a substitution \(\sigma _1\) may be in the domain of another substitution \(\sigma _2\) occurring below \(\sigma _1\). In this case, the topologically ordered composition is \(\sigma _1 \sigma _2\) (i.e. apply first \(\sigma _1\) and then \(\sigma _2\)).

  8. TPTP’s general proof format [30] requires that the conclusion of an inference rule be a logical consequence of (or equi-satisfiable to) its premises. This limitation prevents an easy representation of natural deduction’s implication introduction rule, tableaux’s \(\beta \) rule or splitting. CR ’s conflict-driven clause learning is also affected by this limitation.

  9. It is assumed (without loss of generality) that, for every i, \(\varGamma _i\) is actually used in \(\varphi _i\). Otherwise, if \(\varGamma _j\) were not used in \(\varphi _j\) for some j, \(\varphi _j\) would already be a refutation of S, and it would not be necessary to split \(\varGamma _1 \vee \ldots \vee \varGamma _k\).

  10. It may be reused many times, since \(\varphi _i\) does not need to be tree-like.

  11. Although antecedents of sequents and a Sat-solver’s trail resemble each other, as both store decision literals, they are not quite the same thing. Whereas a Sat-solver’s trail is typically a global structure, each sequent’s antecedent is local and stores only the decisions that have been necessary to derive the sequent’s succedent.

References

  1. Alagi, G., Weidenbach, C.: Non-redundant clause learning. In: FroCoS, pp. 69–84 (2015)

  2. Beth, E.W.: Semantic entailment and formal derivability. In: Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde 18(13), 309–342 (1955)

  3. Bachmair, L., Ganzinger, H.: Completion of first-order clauses with equality by strict superposition (Extended Abstract). In: 2nd International Workshop Conditional and Typed Rewriting Systems, LNCS 516, pp. 162–180. Springer, Berlin (1990)

  4. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Baumgartner, P.: A first order Davis-Putnam-Longeman-Loveland procedure. In: Proceedings of the 17th International Conference on Automated Deduction (CADE), pp. 200–219 (2000)

  6. Baumgartner, P.: Model evolution based theorem proving. IEEE Intel. Syst. 29(1), 4–10 (2014)

    Article  Google Scholar 

  7. Baumgartner, P., Tinelli, C.: The model evolution calculus. In: CADE, pp. 350–364 (2003)

  8. Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: LPAR, pp. 572–586 (2006)

  9. Biere, A.: PicoSAT Essentials. JSAT 4(2–4), 75–97 (2008)

  10. Bonacina, M.P.: Plaisted, DA.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) 4th Workshop on Practical Aspects of Automated Reasoning, PAAR@IJCAR 2014, Vienna, Austria, 2014, vol. 31, pp. 25–38. EasyChair (2014)

  11. Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113–141 (2016)

  12. Brown, CE.: Satallax: An automatic higher-order prover. In: IJCAR, pp. 111–117 (2012)

  13. Brown, CE.: Reducing higher-order theorem proving to a sequence of SAT problems. J. Autom. Reason. 51(1), 57–77 (2013)

  14. Claessen, K.: The anatomy of equinox—an extensible automated reasoning tool for first-order logic and beyond (Talk Abstract). In: Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), pp. 1–3 (2011)

  15. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201–215 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  16. Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394–397 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  17. de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: 3rd International Joint Conference on Automated Reasoning (IJCAR), pp. 303–317 (2006)

  18. Gentzen, G.: Untersuchungen über das logische Schließen I & II. Math. Z. 39(1), 176–210, 405–431 (1935)

  19. Barbosa, H., Fontaine, P.: Congruence closure with free variables (Work in Progress). In: 2nd International Workshop on Quantification (2015)

  20. Korovin, K.: iProver—an instantiation-based theorem prover for first-order logic (system description)”. In: International Joint Conference on Automated Reasoning (IJCAR), pp. 292–298 (2008)

  21. Korovin, K.: Inst-gen—a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics, vol. 7797, pp. 239–270. Springer, Berlin (2013)

  22. Marques-Silva, J., Sakallah, K.A.: GRASP—a new search algorithm for satisfiability. In: International Conference on Computer-Aided Design, pp. 220–227 (1996)

  23. Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 127–149 (2008)

  24. McCharen, J., Overbeek, R., Wos, L.: Complexity and related enhancements for automated theorem-proving programs. Comput. Math. Appl. 2, 1–16 (1976)

    MATH  Google Scholar 

  25. McCune, W.: Prover9 Manual (2009). https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/

  26. Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2–3), 91–110 (2002)

    MATH  Google Scholar 

  27. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  28. Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order thories with equality. Mach. Intell. 4, 135–150 (1969)

    MATH  Google Scholar 

  29. Schultz, S.: System description: E 1.8. In: LPAR, pp. 735–743 (2013)

  30. Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  31. Voronkov, A.: AVATAR: The architecture for first-order theorem provers. In: CAV, pp. 696–710 (2014)

  32. Waldmann, U.: Superposition. In: Paleo, B.W. (eds.) Towards an Encyclopaedia of Proof Systems, p. 29. College Publications, London, UK (2017)

  33. Waldmann, U.: Saturation with redundancy. In: Paleo, B.W. (eds.) Towards an Encyclopaedia of Proof Systems, p. 30. College Publications, London, UK (2017)

  34. Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1965–2013. Elsevier and MIT Press (2001)

  35. Weidenbach, C.: The Theory of SPASS version 2.0. In: SPASS 2.0 documentation

  36. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: CADE, pp. 140–145 (2009)

  37. Wetzler, N., Heule, M., Hunt Jr, WA.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: SAT, pp. 422–429 (2014)

  38. Zhang, L., Madigan, CF., Moskewicz, MH., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design, pp. 279–285 (2001)

Download references

Acknowledgements

Bruno is grateful to Pascal Fontaine, who supervised him during his first post-doc in 2010, providing a great opportunity for him to learn some of the essential ideas behind current Sat-solvers. We are thankful to Peter Baumgartner, who shared his experience in model evolution and other related methods, when we discussed the idea of CR in May 2015. Bruno would also like to thank Hans de Nivelle for discussions about the Geo prover at CADE 2015. We thank Pascal Fontaine and the anonymous reviewers for their feedback on an earlier version of this paper. This research was partially funded by the Australian Government through the Australian Research Council.

Author information

Authors and Affiliations

  1. Australian National University, Canberra, Australia

    John Slaney & Bruno Woltzenlogel Paleo

Authors
  1. John Slaney
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruno Woltzenlogel Paleo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bruno Woltzenlogel Paleo.

Additional information

An erratum to this article is available at https://doi.org/10.1007/s10817-017-9434-4.

Appendix: Classical Natural Deduction

Appendix: Classical Natural Deduction

A typical non-clausal natural deduction calculus for quantified minimal logic extended with a classical rule for double negation elimination is shown in Fig. 11.

Fig. 11
figure 11

A Non-clausal natural deduction calculus

Full size image

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Slaney, J., Woltzenlogel Paleo, B. Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning. J Autom Reasoning 60, 133–156 (2018). https://doi.org/10.1007/s10817-017-9408-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-017-9408-6

Keywords

Search

Navigation