Generating clause sequences of a CNF formula
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F21%3A10435589" target="_blank" >RIV/00216208:11320/21:10435589 - isvavai.cz</a>
Výsledek na webu
<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=snZsQ.ubSL" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=snZsQ.ubSL</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.tcs.2020.12.021" target="_blank" >10.1016/j.tcs.2020.12.021</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Generating clause sequences of a CNF formula
Popis výsledku v původním jazyce
Given a CNF formula Phi with clauses C-1 , ..., C-m and variables V = {x(1), ..., x(n)} , a truth assignment a : V -> {0 , 1} of Phi leads to a clause sequence sigma(Phi)(a) = (C-1(a), ..., C-m(a)) is an element of {0 , 1}(m) where C-i(a) =1 if clause C-i evaluates to 1 under assignment a , otherwise C-i(a) = 0. The set of all possible clause sequences carries a lot of information on the formula, e.g. SAT, MAX-SAT and MIN-SAT can be encoded in terms of finding a clause sequence with extremal properties. We consider a problem posed at Dagstuhl Seminar 19211 "Enumeration in Data Management" (2019) about the generation of all possible clause sequences of a given CNF with bounded dimension. We prove that the problem can be solved in incremental polynomial time. We further give an algorithm with polynomial delay for the class of tractable CNF formulas. We also consider the generation of maximal and minimal clause sequences, and show that generating maximal clause sequences is NP-hard, while minimal clause sequences can be generated with polynomial delay. (C) 2020 The Author(s). Published by Elsevier B.V.
Název v anglickém jazyce
Generating clause sequences of a CNF formula
Popis výsledku anglicky
Given a CNF formula Phi with clauses C-1 , ..., C-m and variables V = {x(1), ..., x(n)} , a truth assignment a : V -> {0 , 1} of Phi leads to a clause sequence sigma(Phi)(a) = (C-1(a), ..., C-m(a)) is an element of {0 , 1}(m) where C-i(a) =1 if clause C-i evaluates to 1 under assignment a , otherwise C-i(a) = 0. The set of all possible clause sequences carries a lot of information on the formula, e.g. SAT, MAX-SAT and MIN-SAT can be encoded in terms of finding a clause sequence with extremal properties. We consider a problem posed at Dagstuhl Seminar 19211 "Enumeration in Data Management" (2019) about the generation of all possible clause sequences of a given CNF with bounded dimension. We prove that the problem can be solved in incremental polynomial time. We further give an algorithm with polynomial delay for the class of tractable CNF formulas. We also consider the generation of maximal and minimal clause sequences, and show that generating maximal clause sequences is NP-hard, while minimal clause sequences can be generated with polynomial delay. (C) 2020 The Author(s). Published by Elsevier B.V.
Klasifikace
Druh
J<sub>imp</sub> - Č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)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA19-19463S" target="_blank" >GA19-19463S: Reprezentace booleovských funkcí úplné vzhledem k jednotkové propagaci</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2021
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ů
Údaje specifické pro druh výsledku
Název periodika
Theoretical Computer Science
ISSN
0304-3975
e-ISSN
—
Svazek periodika
856
Číslo periodika v rámci svazku
February
Stát vydavatele periodika
NL - Nizozemsko
Počet stran výsledku
7
Strana od-do
68-74
Kód UT WoS článku
000611818700006
EID výsledku v databázi Scopus
2-s2.0-85099519102