TY - JOUR

T1 - Generating clause sequences of a CNF formula

AU - Bérczi, Kristóf

AU - Boros, Endre

AU - Čepek, Ondřej

AU - Elbassioni, Khaled

AU - Kučera, Petr

AU - Makino, Kazuhisa

N1 - Funding Information:
Kristóf Bérczi was supported by the János Bolyai Research Fellowship of the Hungarian Academy of Sciences and by the ÚNKP-19-4 New National Excellence Program of the Ministry for Innovation and Technology . Ondřej Čepek and Petr Kučera gratefully acknowledge a support by the Czech Science Foundation (Grant 19-19463S ). Projects no. NKFI-128673 and “Application Domain Specific Highly Reliable IT Solutions” have been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the FK_18 and the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding schemes, respectively. This work was supported by the Research Institute for Mathematical Sciences , an International Joint Usage/Research Center located in Kyoto University.
Publisher Copyright:
© 2020 The Author(s)

PY - 2021/2/8

Y1 - 2021/2/8

N2 - Given a CNF formula Φ with clauses C1,…,Cm and variables V={x1,…,xn}, a truth assignment a:V→{0,1} of Φ leads to a clause sequence σΦ(a)=(C1(a),…,Cm(a))∈{0,1}m where Ci(a)=1 if clause Ci evaluates to 1 under assignment a, otherwise Ci(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.

AB - Given a CNF formula Φ with clauses C1,…,Cm and variables V={x1,…,xn}, a truth assignment a:V→{0,1} of Φ leads to a clause sequence σΦ(a)=(C1(a),…,Cm(a))∈{0,1}m where Ci(a)=1 if clause Ci evaluates to 1 under assignment a, otherwise Ci(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.

KW - Clause sequences

KW - CNF formulas

KW - Enumeration

KW - Generation

UR - http://www.scopus.com/inward/record.url?scp=85099519102&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2020.12.021

DO - 10.1016/j.tcs.2020.12.021

M3 - Article

AN - SCOPUS:85099519102

SN - 0304-3975

VL - 856

SP - 68

EP - 74

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -