Recognizing disguised NR(1) instances of the satisfiability problem
From MaRDI portal
Publication:3898029
DOI10.1016/0196-6774(80)90007-3zbMath0451.68037OpenAlexW1978253773WikidataQ55952578 ScholiaQ55952578MaRDI QIDQ3898029
Publication date: 1980
Published in: Journal of Algorithms (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0196-6774(80)90007-3
satisfiability problemBoolean expressionsconjunctive normal formHorn setconstructive linear-time algorithmnegation restricted
Related Items
Properties of SLUR Formulae, Recognition of \(q\)-Horn formulae in linear time, A new algorithm for the propositional satisfiability problem, Polynomial-time inference of all valid implications for Horn and related formulae, On renamable Horn and generalized Horn functions, Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing, Domain permutation reduction for constraint satisfaction problems, Testing heuristics: We have it all wrong, Horn functions and submodular Boolean functions, 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, Unique Horn renaming and Unique 2-Satisfiability, Detecting embedded Horn structure in propositional logic, On generalized Horn formulas and \(k\)-resolution, On exact selection of minimally unsatisfiable subformulae, Solving the resolution-free SAT problem by submodel propagation in linear time, Recognizing renamable generalized propositional Horn formulas is NP- complete, Sorting, linear time and the satisfiability problem, Recognition and dualization of disguised bidual Horn functions., A perspective on certain polynomial-time solvable classes of satisfiability, A linear algorithm for renaming a set of clauses as a Horn set
