English

Generating clause sequences of a CNF formula

Discrete Mathematics 2020-02-18 v1 Logic in Computer Science

Abstract

Given a CNF formula Φ\Phi with clauses C1,,CmC_1,\ldots,C_m and variables V={x1,,xn}V=\{x_1,\ldots,x_n\}, a truth assignment a:V{0,1}a:V\rightarrow\{0,1\} of Φ\Phi leads to a clause sequence σΦ(a)=(C1(a),,Cm(a)){0,1}m\sigma_\Phi(a)=(C_1(a),\ldots,C_m(a))\in\{0,1\}^m where Ci(a)=1C_i(a) = 1 if clause CiC_i evaluates to 11 under assignment aa, otherwise Ci(a)=0C_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.

Cite

@article{arxiv.2002.06727,
  title  = {Generating clause sequences of a CNF formula},
  author = {Kristóf Bérczi and Endre Boros and Ondřej Čepek and Khaled Elbassioni and Petr Kučera and Kazuhisa Makino},
  journal= {arXiv preprint arXiv:2002.06727},
  year   = {2020}
}

Comments

9 pages

R2 v1 2026-06-23T13:43:25.646Z