Generating clause sequences of a CNF formula

DOI10.1016/J.TCS.2020.12.021MaRDI QIDQ2219060zbMATH OpenOpenAlexFDO

Authors Kristóf Bérczi, Endre Boros, Ondřej Čepek, Petr Kučera, Kazuhisa Makino, Khaled Elbassioni

Publication date 19 January 2021

Published in Theoretical Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2002.06727

zbMATH Keywords

clause sequencesCNF formulasenumerationgeneration

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Combinatorics in computer science (68R05) Computational aspects of satisfiability (68R07)

Abstract: Given a CNF formula $Phi$ with clauses $C_1,ldots,C_m$ and variables $V=x_1,ldots,x_n$, a truth assignment $a:Vightarrow0,1$ of $Phi$ leads to a clause sequence $sigm{a}_{P}hi(a)=(C_1(a),ldots,C_m(a))in{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.

Recommendations

• On generating all solutions of generalized satisfiability problems
• An improved generator for 3-CNF formulas
• Generating all maximal models of a Boolean expression
• Generating models of a matched formula with a polynomial delay
• Two tractable subclasses of minimal unsatisfiable formulas

Cites work

• A New Algorithm for Generating All the Maximal Independent Sets
• Algorithm Theory - SWAT 2004
• Algorithms for propositional model counting
• Algorithms – ESA 2004
• Efficient enumeration of solutions produced by closure operations
• Enumerating homomorphisms
• scientific article; zbMATH DE number 7635224 (Why is no real title available?)
• On generating all maximal independent sets
• On the complexity of enumerating the answers to well-designed pattern trees
• Static analysis and optimization of semantic web queries
• The complexity of theorem-proving procedures

Cited in

(1)

• On the enumeration of signatures of XOR-CNF's

This page was built for publication: Generating clause sequences of a CNF formula

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2219060)