Počet záznamů: 1
New Complexity Results for Lukasiewicz Logic
- 1.
SYSNO ASEP 0491990 Druh ASEP J - Článek v odborném periodiku Zařazení RIV J - Článek v odborném periodiku Poddruh J Článek ve WOS Název New Complexity Results for Lukasiewicz Logic Tvůrce(i) Bofill, M. (ES)
Manya, F. (ES)
Vidal, Amanda (UIVT-O) RID, SAI, ORCID
Villaret, M. (ES)Zdroj.dok. Soft Computing. - : Springer - ISSN 1432-7643
Roč. 23, č. 7 (2019), s. 2187-2197Poč.str. 11 s. Jazyk dok. eng - angličtina Země vyd. DE - Německo Klíč. slova Lukasiewicz logics ; Clausal forms ; Complexity ; Instance generator Vědní obor RIV IN - Informatika Obor OECD Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8) CEP GA17-04630S GA ČR - Grantová agentura ČR Způsob publikování Open access Institucionální podpora UIVT-O - RVO:67985807 UT WOS 000461580400006 EID SCOPUS 85049926337 DOI 10.1007/s00500-018-3365-9 Anotace One aspect that has been poorly studied in multiple-valued logics, and in particular in Lukasiewicz 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 Lukasiewicz satisfiability solvers, we start by defining a natural and intuitive class of clausal forms (simple L-clausal forms) and studying their complexity. Since we prove that the satisfiability problem of simple L-clausal forms can be solved in linear time, we then define two new classes of clausal forms (L-clausal forms and restricted L-clausal forms) that truly exploit the non-lattice operations of Lukasiewicz 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 Lukasiewicz logic formulas into L-clausal forms. Finally, we describe a random generator of L-clausal forms and report on an empirical investigation in which we identify an easy-hard-easy pattern and a phase transition phenomenon for L-clausal forms. Pracoviště Ústav informatiky Kontakt Tereza Šírová, sirova@cs.cas.cz, Tel.: 266 053 800 Rok sběru 2020 Elektronická adresa http://hdl.handle.net/11104/0285586
Počet záznamů: 1