A decomposition method for CNF minimality proofs

DOI10.1016/J.TCS.2013.09.016MaRDI QIDQ392185zbMATH OpenOpenAlexDBLPWikidataFDO

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

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

Boolean functionsBoolean minimizationCNFdecomposition methodHorn minimization

Mathematics Subject Classification ID

Boolean functions (06E30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Horn minimization by iterative decomposition
• Strong duality in Horn minimization
• Hardness results for approximate pure Horn CNF formulae minimization
• Horn functions and their DNFs
• Redundancy in logic. II: 2CNF and Horn propositional formulae

Cites work

• A subclass of Horn CNFs optimally compressible in polynomial time
• Exclusive and essential sets of implicates of Boolean functions
• Hardness results for approximate pure Horn CNF formulae minimization
• Horn functions and their DNFs
• Horn minimization by iterative decomposition
• scientific article; zbMATH DE number 4053069 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Minimal Representation of Directed Hypergraphs
• Minimum Covers in Relational Database Model
• On approximate Horn formula minimization
• Optimal compression of propositional Horn knowledge bases: Complexity and approximation
• The complexity of Boolean formula minimization
• The complexity of theorem-proving procedures
• The minimum equivalent DNF problem and shortest implicants
• Unification as a complexity measure for logic programming

Cited in

(11)

• Horn minimization by iterative decomposition
• Minimal samples of positive examples identifying \(k\)-CNF Boolean functions
• Strong duality in Horn minimization
• Recognition of tractable DNFs representable by a constant number of intervals
• Hardness results for approximate pure Horn CNF formulae minimization
• Redundancy in logic. II: 2CNF and Horn propositional formulae
• Minimality of the correctness criterion for multiplicative proof nets
• Succinctness and tractability of closure operator representations
• Hydras: complexity on general graphs and a subclass of trees
• Properties of Switch-List Representations of Boolean Functions
• Approximating minimum representations of key Horn functions

Describes a project that uses

Uses Software

• Ltur

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

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