Skip to main content
SpringerLink
Log in

Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction

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

Abstract

Although it is well-known that every satisfiable formula in Łukasiewicz’ infinite-valued logic \(\mathcal{L}_{\infty}\) can be satisfied in some finite-valued logic, practical methods for finding an appropriate number of truth degrees do currently not exist. Extending upon earlier results by Aguzzoli et al., which only take the total number of variable occurrences into account, we present a detailed analysis of what type of formulas require a large number of truth degrees to be satisfied. In particular, we reveal important links between this number of truth degrees and the dimension, and structure, of the cycle space of an associated bipartite graph. We furthermore propose an efficient, polynomial-time algorithm for establishing a strong upper bound on the required number of truth degrees, allowing us to check the satisfiability of sets of formulas in \(\mathcal{L}_{\infty}\), and more generally, sets of fuzzy clauses over Łukasiewicz logic formulas, by solving a small number of constraint satisfaction problems. In an experimental evaluation, we demonstrate the practical usefulness of this approach, comparing it with a state-of-the-art technique based on mixed integer programming.

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

Access this article

Log in via an institution

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

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Aguzzoli, S.: An asymptotically tight bound on countermodels for Łukasiewicz logic. Int. J. Approx. Reason. 43, 76–89 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  2. Aguzzoli, S., Ciabattoni, A.: Finiteness in infinite-valued Łukasiewicz logic. J. Logic Lang. Inf. 9, 5–29 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  3. Aguzzoli, S., Gerla, B.: Finite-valued reductions of infinite-valued logics. Arch. Math. Log. 41, 361–399 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bobillo, F., Bou, F., Straccia, U.: On the failure of the finite model property in some fuzzy description logics. Fuzzy Sets Syst. 172(1), 1–12 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bobillo, F., Straccia, U.: Fuzzy description logics with general t-norms and datatypes. Fuzzy Sets Syst. 160(23), 3382–3402 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bollobás, B.: Modern Graph Theory. Springer (1998)

  7. Hähnle, R.: Towards an efficient tableau proof procedure for multiple-valued logics. In: Börger, E., Kleine Büning, H., Richter, M., Schönfeld, W. (eds.) Selected Papers from Computer Science Logic, pp. 248–260. Springer-Verlag (1991)

  8. Hähnle, R.: Many-valued logic and mixed integer programming. Ann. Math. Artif. Intell. 12, 231–264 (1994)

    Article  MATH  Google Scholar 

  9. Hähnle, R.: Tutorial: Complexity of many-valued logics. IEEE International Symposium on Multiple-Valued Logic, pp. 137–148 (2001)

  10. Hähnle, R., Escalada-Imaz, G.: Deduction in multivalued logics: a survey. Mathw. Soft Comput. 4(2), 69–97 (1997)

    MATH  Google Scholar 

  11. Hájek, P.: Metamathematics of Fuzzy Logic, pp. 155–174. Kluwer Academic Publishers (1998)

  12. Hoffman, A., Kruskal, J.: Integral boundary points of convex polyhedra. Ann. Math. Stud. 38, 223–246 (1956)

    MathSciNet  MATH  Google Scholar 

  13. Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA ’00: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 14–25. ACM, New York (2000)

    Google Scholar 

  14. Janssen, J., Heymans, S., Vermeir, D., De Cock, M.: Compiling fuzzy answer set programs to fuzzy propositional theories. In: Proceedings of the 24th International Conference on Logic Programming, pp. 362–376 (2008)

  15. Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence, pp. 359–363 (1992)

  16. Kavitha, T., Mehlhorn, K., Michail, D., Paluch, K.: An o(m 2 n) algorithm for minimum cycle basis of graphs. Algorithmica 52, 333–349 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  17. Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artif. Intell. 157(1–2), 115–137 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  18. McNaughton, R.: A theorem about infinite-valued sentential logic. J. Symb. Log. 16, 1–13 (1951)

    Article  MathSciNet  MATH  Google Scholar 

  19. Mitchell, D., Selman, B., Levesque, H.: Generating hard satisfiability problems. Artif. Intell. 81(1–2), 17–29 (1996)

    MathSciNet  Google Scholar 

  20. Mundici, D.: Satisfiability in many-valued sentential logic is NP-complete. Theor. Comp. Sci. 52, 145–153 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  21. Mundici, D., Olivetti, N.: Resolution and model building in the infinite-valued calculus of Łukasiewicz. Theor. Comp. Sci. 200, 335–366 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  22. Olivetti, N.: Tableaux for Łukasiewicz infinite-valued logic. Stud. Log. 73(1), 81–111 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  23. Pavelka, J.: On fuzzy logic. Zeitschr. F. Math. Logik Und Grundl. Der Math. 25, 45–52, 119–134, 447–464 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  24. Pham, D., Thornton, J., Sattar, A.: Modelling and solving temporal reasoning as propositional satisfiability. Artif. Intell. 172(15), 1752–1782 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  25. Schockaert, S., De Cock, M., Kerre, E.: Spatial reasoning in a fuzzy region connection calculus. Artif. Intell. 173, 258–298 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  26. Schockaert, S., Janssen, J., Vermeir, D., Cock, M.: Finite satisfiability in infinite-valued Łukasiewicz logic. In: Proceedings of the 3rd International Conference on Scalable Uncertainty Management, pp. 240–254 (2009)

  27. Smyth, B., McClave, P.: Similarity vs. diversity. In: ICCBR ’01: Proceedings of the 4th International Conference on Case-based Reasoning, pp. 347–361. Springer, London (2001)

  28. Straccia, U., Bobillo, F.: Mixed integer programming, general concept inclusions and fuzzy description logics. Mathw. Soft Comput. 14(3), 247–259 (2007)

    MathSciNet  MATH  Google Scholar 

  29. Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. In: Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming, vol. 4204 of Lecture Notes in Computer Science, pp. 590–603 (2006)

  30. Wagner, H.: A new resolution calculus for the infinite-valued propositional logic of Łukasiewicz. In: Proceedings of the International Workshop on First order Theorem Proving, pp. 234–243 (1998)

  31. Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32(1), 565–606 (2008)

    MATH  Google Scholar 

  32. Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Proceedings of 14th International Conference on Computer Aided Verification, vol. 2404 of Lecture Notes in Computer Science, pp. 641–653 (2002)

Download references

Author information

Authors and Affiliations

  1. Department of Applied Mathematics and Computer Science, Ghent University, Ghent, Belgium

    Steven Schockaert

  2. Department of Computer Science, Vrije Universiteit Brussel, Brussel, Belgium

    Jeroen Janssen & Dirk Vermeir

Authors
  1. Steven Schockaert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jeroen Janssen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dirk Vermeir
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Steven Schockaert.

Additional information

Steven Schockaert is a Postdoctoral Fellow of the Research Foundation - Flanders (FWO).

Rights and permissions

Reprints and permissions

About this article

Cite this article

Schockaert, S., Janssen, J. & Vermeir, D. Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction. J Autom Reasoning 49, 493–550 (2012). https://doi.org/10.1007/s10817-011-9227-0

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-011-9227-0

Keywords

Search

Navigation