Generating clause sequences of a CNF formula
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Generating clause sequences of a CNF formula
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA19-19463S" target="_blank" >GA19-19463S: Boolean Representation Languages Complete for Unit Propagation</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2021
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Theoretical Computer Science
ISSN
0304-3975
e-ISSN
—
Volume of the periodical
856
Issue of the periodical within the volume
February
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
7
Pages from-to
68-74
UT code for WoS article
000611818700006
EID of the result in the Scopus database
2-s2.0-85099519102