Hardness results for approximate pure Horn CNF formulae minimization

DOI10.1007/S10472-014-9415-9MaRDI QIDQ2254607zbMATH OpenOpenAlexWikidataFDO

Authors Endre Boros, Aritanan Gruber

Publication date 5 February 2015

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

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

zbMATH Keywords

artificial intelligenceBoolean functionscomputational complexityhardness of approximationpropositional Horn logic

Mathematics Subject Classification ID

Boolean functions (06E30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Logic in artificial intelligence (68T27)

Abstract: We study the hardness of approximation of clause minimum and literal minimum representations of pure Horn functions in $n$ Boolean variables. We show that unless P=NP, it is not possible to approximate in polynomial time the minimum number of clauses and the minimum number of literals of pure Horn CNF representations to within a factor of $2^{lo{g}^{1-o(1)}n}$. This is the case even when the inputs are restricted to pure Horn 3-CNFs with $O(n^{1+varepsilon})$ clauses, for some small positive constant $varepsilon$. Furthermore, we show that even allowing sub-exponential time computation, it is still not possible to obtain constant factor approximations for such problems unless the Exponential Time Hypothesis turns out to be false.

Recommendations

• On approximate Horn formula minimization
• On the complexity of the maximum satisfiability problem for Horn formulas
• A subclass of Horn CNFs optimally compressible in polynomial time
• On the Approximability of Splitting-SAT in 2-CNF Horn Formulas
• scientific article; zbMATH DE number 4085614
• Ruling Out Polynomial-Time Approximation Schemes for Hard Constraint Satisfaction Problems
• Tight bounds on the approximability of almost-satisfiable Horn SAT and exact hitting set
• scientific article; zbMATH DE number 6783493
• Complexity results on minimal unsatisfiable formulas
• Horn versus full first-order: complexity dichotomies in algebraic constraint satisfaction

Cites work

• A decomposition method for CNF minimality proofs
• Composition of low-error 2-query PCPs using decodable PCPs
• Computational Complexity
• Exclusive and essential sets of implicates of Boolean functions
• Hardness results for approximate pure Horn CNF formulae minimization
• Horn functions and their DNFs
• scientific article; zbMATH DE number 5852793 (Why is no real title available?)
• scientific article; zbMATH DE number 1839431 (Why is no real title available?)
• Interactive proofs and the hardness of approximating cliques
• Introduction to algorithms.
• 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
• On the complexity of k-SAT
• On the hardness of approximating label-cover
• On the hardness of approximating spanners
• Optimal compression of propositional Horn knowledge bases: Complexity and approximation
• Probabilistic checking of proofs
• Proof verification and the hardness of approximation problems
• The complexity of theorem-proving procedures
• The design of approximation algorithms
• The hardness of approximate optima in lattices, codes, and systems of linear equations
• Two-query PCP with subconstant error
• Unification as a complexity measure for logic programming

Cited in

(12)

• Strong duality in Horn minimization
• Autark assignments of Horn CNFs
• Hardness results for approximate pure Horn CNF formulae minimization
• On the hydra number of disconnected graphs
• On the Approximability of Splitting-SAT in 2-CNF Horn Formulas
• On approximate Horn formula minimization
• A decomposition method for CNF minimality proofs
• The joy of implications, aka pure Horn formulas: mainly a survey
• Hydras: complexity on general graphs and a subclass of trees
• Hydras: directed hypergraphs and Horn formulas
• Approximating minimum representations of key Horn functions
• A subclass of Horn CNFs optimally compressible in polynomial time

Describes a project that uses

Uses Software

• JBool
• Ltur

This page was built for publication: Hardness results for approximate pure Horn CNF formulae minimization

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