A decomposition method for CNF minimality proofs

DOI10.1016/j.tcs.2013.09.016zbMath1358.68120OpenAlexW1984659874WikidataQ59560508 ScholiaQ59560508MaRDI QIDQ392185

Petr Kučera, Endre Boros, Ondřej Čepek

Publication date: 13 January 2014

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2013.09.016

zbMATH Keywords

decomposition methodBoolean functionsBoolean minimizationCNFHorn minimization

Mathematics Subject Classification ID

Related Items (6)

Properties of Switch-List Representations of Boolean Functions ⋮ Succinctness and tractability of closure operator representations ⋮ Hydras: complexity on general graphs and a subclass of trees ⋮ Recognition of tractable DNFs representable by a constant number of intervals ⋮ Hardness results for approximate pure Horn CNF formulae minimization ⋮ Approximating Minimum Representations of Key Horn Functions

Uses Software

• Ltur

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of Boolean formula minimization
• A subclass of Horn CNFs optimally compressible in polynomial time
• Exclusive and essential sets of implicates of Boolean functions
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Horn functions and their DNFs
• Horn minimization by iterative decomposition
• Optimal compression of propositional Horn knowledge bases: Complexity and approximation
• The minimum equivalent DNF problem and shortest implicants
• Hardness results for approximate pure Horn CNF formulae minimization
• On Approximate Horn Formula Minimization
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Minimal Representation of Directed Hypergraphs
• Unification as a complexity measure for logic programming
• Minimum Covers in Relational Database Model
• The complexity of theorem-proving procedures

This page was built for publication: A decomposition method for CNF minimality proofs