Satisfiability of mixed Horn formulas

DOI10.1016/J.DAM.2007.02.010MaRDI QIDQ997066zbMATH OpenOpenAlexFDO

Authors Stefan Porschen, Ewald Speckenmeyer

Publication date 19 July 2007

Published in Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.dam.2007.02.010

zbMATH Keywords

fixed-parameter tractabilityquadratic formula(hidden) Horn formula(weighted) satisfiability\(q\)-Horn formulaminimal vertex cover

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Satisfiability on mixed instances
• On Some Aspects of Mixed Horn Formulas
• scientific article; zbMATH DE number 1099516
• Satisfiability of co-nested formulas
• On the complexity of the maximum satisfiability problem for Horn formulas
• On a generalization of Horn constraint systems
• A note on the complexity of the satisfiability of modal Horn clauses
• Satisfiability in composition-nominative logics
• Combined Satisfiability Modulo Parametric Theories
• SAT-Based Horn Least Upper Bounds

Cites work

• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1161563 (Why is no real title available?)
• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A satisfiability formulation of problems on level graphs
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Maximal and maximum independent sets in graphs with at mostr cycles
• Maximal independent sets in graphs with at most one cycle
• Nested satisfiability
• On cliques in graphs
• On generating all maximal independent sets
• Polynomial-time inference of all valid implications for Horn and related formulae
• Recognition of q-Horn formulae in linear time
• Renaming a Set of Clauses as a Horn Set
• STACS 2004
• The Number of Maximal Independent Sets in Triangle-Free Graphs
• The number of maximal independent sets in a connected graph
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(17)

• A CNF Class Generalizing Exact Linear Formulas
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• Theory and Applications of Satisfiability Testing
• Horn logic, search and satisfiability. A collection of papers in memory of Robert G. Jeroslow
• Generalized \(k\)-ary tanglegrams on level graphs: a satisfiability-based approach and its evaluation
• Simple but hard mixed Horn formulas
• On the complexity of the maximum satisfiability problem for Horn formulas
• A satisfiability-based approach for embedding generalized tanglegrams on level graphs
• On a generalization of Horn constraint systems
• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• Satisfiability on mixed instances
• On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls
• SAT-Based Horn Least Upper Bounds
• On Some Aspects of Mixed Horn Formulas
• scientific article; zbMATH DE number 4118335 (Why is no real title available?)
• Unique Horn renaming and Unique 2-Satisfiability
• A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors

Describes a project that uses

Uses Software

• Ltur

This page was built for publication: Satisfiability of mixed Horn formulas

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