English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/197486
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE
Exportar a otros formatos:


New complexity results for Lukasiewicz logic

AuthorsBofill, Miquel; Manyà, Felip CSIC ORCID ; Vidal, Amanda; Villaret, Mateu
KeywordsLukasiewicz logics
Clausal forms
Instance generator
Issue DateApr-2019
PublisherSpringer Nature
CitationSoft Computing 23(7): 2187–2197 (2019)
AbstractOne aspect that has been poorly studied in multiple-valued logics, and in particular in Łukasiewicz logic, is the generation of instances of varying difficulty for evaluating, comparing and improving satisfiability solvers. With the ultimate goal of finding challenging benchmarks for Łukasiewicz satisfiability solvers, we start by defining a natural and intuitive class of clausal forms (simple Ł-clausal forms) and studying their complexity. Since we prove that the satisfiability problem of simple Ł-clausal forms can be solved in linear time, we then define two new classes of clausal forms (Ł-clausal forms and restricted Ł-clausal forms) that truly exploit the non-lattice operations of Łukasiewicz logic and whose satisfiability problems are NP-complete when clauses have at least three literals, and admit linear-time algorithms when clauses have at most two literals. We also define an efficient satisfiability preserving translation of Łukasiewicz logic formulas into Ł-clausal forms. Finally, we describe a random generator of Ł-clausal forms and report on an empirical investigation in which we identify an easy-hard-easy pattern and a phase transition phenomenon for Ł-clausal forms.
Publisher version (URL)http://dx.doi.org/10.1007/s00500-018-3365-9
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
New complexity results for Łukasiewicz logic.pdf567,51 kBAdobe PDFThumbnail
Show full item record
Review this work

Related articles:

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.