New Complexity Results for Lukasiewicz Logic

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F19%3A00491990" target="_blank" >RIV/67985807:_____/19:00491990 - isvavai.cz</a>

Výsledek na webu

<a href="http://hdl.handle.net/11104/0285586" target="_blank" >http://hdl.handle.net/11104/0285586</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s00500-018-3365-9" target="_blank" >10.1007/s00500-018-3365-9</a>

Jazyk výsledku

angličtina

Název v původním jazyce

New Complexity Results for Lukasiewicz Logic

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

New Complexity Results for Lukasiewicz Logic

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA17-04630S" target="_blank" >GA17-04630S: Predikátové škálované logiky a jejich aplikace v informatice</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Soft Computing

ISSN

1432-7643

e-ISSN

—

Svazek periodika

23

Číslo periodika v rámci svazku

7

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

11

Strana od-do

2187-2197

Kód UT WoS článku

000461580400006

EID výsledku v databázi Scopus

2-s2.0-85049926337