Advanced search
1 file | 1.98 MB

Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction

(2012) JOURNAL OF AUTOMATED REASONING. 49(4). p.493-550
Author
Organization
Abstract
Although it is well-known that every satisfiable formula in Aukasiewicz' infinite-valued logic 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 , and more generally, sets of fuzzy clauses over Aukasiewicz 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.
Keywords
Satisfiability checking, Fuzzy logic, Lukasiewicz semantics, FUZZY LOGIC, PROPOSITIONAL CALCULI, LUKASIEWICZ LOGIC, VALUED LOGICS, SAT, ALGORITHM

Downloads

  • (...).pdf
    • full text
    • |
    • UGent only
    • |
    • PDF
    • |
    • 1.98 MB

Citation

Please use this url to cite or link to this publication:

Chicago
Schockaert, Steven, Jeroen Janssen, and Dirk Vermeir. 2012. “Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction.” Journal of Automated Reasoning 49 (4): 493–550.
APA
Schockaert, S., Janssen, J., & Vermeir, D. (2012). Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction. JOURNAL OF AUTOMATED REASONING, 49(4), 493–550.
Vancouver
1.
Schockaert S, Janssen J, Vermeir D. Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction. JOURNAL OF AUTOMATED REASONING. 2012;49(4):493–550.
MLA
Schockaert, Steven, Jeroen Janssen, and Dirk Vermeir. “Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction.” JOURNAL OF AUTOMATED REASONING 49.4 (2012): 493–550. Print.
@article{1938051,
  abstract     = {Although it is well-known that every satisfiable formula in Aukasiewicz' infinite-valued logic 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 , and more generally, sets of fuzzy clauses over Aukasiewicz 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.},
  author       = {Schockaert, Steven and Janssen, Jeroen and Vermeir, Dirk},
  issn         = {0168-7433},
  journal      = {JOURNAL OF AUTOMATED REASONING},
  keyword      = {Satisfiability checking,Fuzzy logic,Lukasiewicz semantics,FUZZY LOGIC,PROPOSITIONAL CALCULI,LUKASIEWICZ LOGIC,VALUED LOGICS,SAT,ALGORITHM},
  language     = {eng},
  number       = {4},
  pages        = {493--550},
  title        = {Satisfiability checking in \unmatched{0141}ukasiewicz logic as finite constraint satisfaction},
  url          = {http://dx.doi.org/10.1007/s10817-011-9227-0},
  volume       = {49},
  year         = {2012},
}

Altmetric
View in Altmetric
Web of Science
Times cited: