Renaming a Set of Clauses as a Horn Set

DOI10.1145/322047.322059zbMath0365.68082OpenAlexW1981549588WikidataQ55952577 ScholiaQ55952577MaRDI QIDQ4140416

Harry R. Lewis

Publication date: 1978

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/322047.322059

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Algorithms in computer science (68W99)

Related Items (45)

Properties of SLUR Formulae ⋮ Recognition of \(q\)-Horn formulae in linear time ⋮ Backdoors to Satisfaction ⋮ Polynomial-time inference of all valid implications for Horn and related formulae ⋮ On renamable Horn and generalized Horn functions ⋮ On propositional definability ⋮ Domain permutation reduction for constraint satisfaction problems ⋮ Variable and term removal from Boolean formulae ⋮ On renaming a set of clauses as a Horn set ⋮ On the Boolean connectivity problem for Horn relations ⋮ Computation of Renameable Horn Backdoors ⋮ A CNF Class Generalizing Exact Linear Formulas ⋮ Non-Horn clause logic programming ⋮ Trichotomy for integer linear systems based on their sign patterns ⋮ Analyzing fractional Horn constraint systems ⋮ Existence of simple propositional formulas ⋮ Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search ⋮ Maximum renamable Horn sub-CNFs ⋮ Disjunctive closures for knowledge compilation ⋮ On some tractable classes in deduction and abduction ⋮ Unique Horn renaming and Unique 2-Satisfiability ⋮ Resolution search ⋮ Autark assignments of Horn CNFs ⋮ About some UP-based polynomial fragments of SAT ⋮ Automatic decidability and combinability ⋮ On exact selection of minimally unsatisfiable subformulae ⋮ Unnamed Item ⋮ Satisfiability of mixed Horn formulas ⋮ Computational Aspects of Quasi-Classical Entailment ⋮ Recognizing renamable generalized propositional Horn formulas is NP- complete ⋮ Sorting, linear time and the satisfiability problem ⋮ Unnamed Item ⋮ Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas ⋮ Renaming a set of non-Horn clauses ⋮ Recognition and dualization of disguised bidual Horn functions. ⋮ The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas ⋮ A short note on some tractable cases of the satisfiability problem. ⋮ A sharp threshold for the renameable-Horn and the \(q\)-Horn properties ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ Feasibility checking in Horn constraint systems through a reduction based approach ⋮ A perspective on certain polynomial-time solvable classes of satisfiability ⋮ A linear algorithm for renaming a set of clauses as a Horn set ⋮ On functional dependencies in \(q\)-Horn theories ⋮ A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets ⋮ Backdoors to q-Horn

This page was built for publication: Renaming a Set of Clauses as a Horn Set