Linear-time algorithms for testing the satisfiability of propositional horn formulae
From MaRDI portal
Recommendations
- Algorithms for testing the satisfiability of propositional formulae
- LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
- A note on Dowling and Gallier's top-down algorithm for propositional Horn satisfiability
- An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
- Recognition of q-Horn formulae in linear time
Cited in
(only showing first 100 items - show all)- On the relation among answer set solvers
- An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
- On the complexity of the maximum satisfiability problem for Horn formulas
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
- LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
- Polynomially solvable satisfiability problems
- Optimizing propositional calculus formulas with regard to questions of deducibility
- A hierarchy of propositional Horn formuls
- Stratification and knowledge base management
- Reasoning with minimal models: efficient algorithms and applications
- Relevance from an epistemic perspective
- Hard problems for simple default logics
- On the consistency of defeasible databases
- Capturing complexity classes by fragments of second-order logic
- Horn functions and their DNFs
- Detecting embedded Horn structure in propositional logic
- On the complexity of propositional knowledge base revision, updates, and counterfactuals
- Sensitivity analysis for Horn formulae
- An efficient algorithm for the 3-satisfiability problem
- The logic of constraint satisfaction
- Structure identification in relational data
- A hierarchy of tractable satisfiability problems
- The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic
- Local simplification
- Double Horn functions
- Inheritance comes of age: applying nonmonotonic techniques to problems in industry
- Logic programs, well-orderings, and forward chaining
- A linear time algorithm for unique Horn satisfiability
- Optimal compression of propositional Horn knowledge bases: Complexity and approximation
- A linear algorithm for renaming a set of clauses as a Horn set
- Inference flexibility in Horn clause knowledge bases and the simplex method
- Model checking and boolean graphs
- Computing definite logic programs by partial instantiation
- Theory refinement combining analytical and empirical methods
- The complexity of propositional closed world reasoning and circumscription
- The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics
- Recognition of q-Horn formulae in linear time
- Limited reasoning in first-order knowledge bases
- The problem of asking the minimum number of questions in Horn clause systems
- A hypergraph model for constraint logic programming and applications to bus drivers' scheduling
- The unique Horn-satisfiability problem and quadratic Boolean equations.
- Polynomial-time inference of all valid implications for Horn and related formulae
- On renamable Horn and generalized Horn functions
- Branch-and-cut solution of inference problems in propositional logic
- Solving propositional satisfiability problems
- Question-asking strategies for Horn clause systems
- Positive and Horn decomposability of partially defined Boolean functions
- On resolution with short clauses
- Unification in sort theories and its applications
- On computing minimal models
- On the complexity of entailment in propositional multivalued logics
- Hierarchies of polynomially solvable satisfiability problems
- A cost effective question-asking strategy for Horn clause systems
- A fast parallel SAT-solver -- efficient workload balancing
- Max Horn SAT and the minimum cut problem in directed hypergraphs
- Revision programming
- Is intractability of nonmonotonic reasoning a real drawback?
- Reducing belief revision to circumscription (and vice versa)
- Semantical and computational aspects of Horn approximations
- Conjunctive-query containment and constraint satisfaction
- Validating firewalls using flow logics
- Extending and implementing the stable model semantics
- Ordered binary decision diagrams as knowledge-bases
- Logical analysis of binary data with missing bits
- On functional dependencies in q-Horn theories
- An efficient algorithm for a class of constraint satisfaction problems
- Conditional congruence closure over uninterpreted and interpreted symbols
- Conflict-driven answer set solving: from theory to practice
- Pseudo-models and propositional Horn inference
- Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances
- On exact selection of minimally unsatisfiable subformulae
- Solving the resolution-free SAT problem by submodel propagation in linear time
- Selecting and covering colored points
- Gainfree Leontief substitution flow problems
- Directed hypergraphs and applications
- Recognizing renamable generalized propositional Horn formulas is NP- complete
- Sorting, linear time and the satisfiability problem
- On subclasses of minimal unsatisfiable formulas
- A short note on some tractable cases of the satisfiability problem.
- Efficient and flexible matching of recursive types
- Tarskian set constraints
- Horn approximations of empirical data
- Tractable reasoning via approximation
- A perspective on certain polynomial-time solvable classes of satisfiability
- Reasoning with ordered binary decision diagrams
- Logic programs and connectionist networks
- Nesting analysis of mobile ambients
- A decision method for nonmonotonic reasoning based on autoepistemic reasoning
- The arborescence-realization problem
- Unique satisfiability of Horn sets can be solved in nearly linear time
- A new algorithm for the propositional satisfiability problem
- Complexity and undecidability results for logic programming
- Complexity of computing with extended propositional logic programs
- Maximum renamable Horn sub-CNFs
- Bidual Horn functions and extensions
- Two tractable subclasses of minimal unsatisfiable formulas
- Recognition of tractable satisfiability problems through balanced polynomial representations
- Inference approach based on Petri nets
- Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas
- Multi-agent path finding with mutex propagation
This page was built for publication: Linear-time algorithms for testing the satisfiability of propositional horn formulae
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3723723)
