Branch-and-cut solution of inference problems in propositional logic

DOI10.1007/BF01531074zbMath0878.68065OpenAlexW1976816453MaRDI QIDQ1356213

John N. Hooker, Chawki A. Fedjki

Publication date: 14 December 1997

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

Full work available at URL: https://doi.org/10.1007/bf01531074

zbMATH Keywords

propositional logicinference problems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items

GD-SAT model and crossover line, Recognition of \(q\)-Horn formulae in linear time, A linear-time transformation of linear inequalities into conjunctive normal form, Easy problems are sometimes hard, What we can learn from conflicts in propositional satisfiability, A new algorithm for the propositional satisfiability problem, Running time experiments on some algorithms for solving propositional satisfiability problems, Branching rules for satisfiability, Testing heuristics: We have it all wrong, Many-valued logic and mixed integer programming, Simplifying clausal satisfiability problems, Generating hard satisfiability problems, The satisfiability constraint gap, Learning from conflicts in propositional satisfiability, The \(Multi\)-SAT algorithm, MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability, A complete adaptive algorithm for propositional satisfiability, Computational experience with an interior point algorithm on the satisfiability problem, New methods for computing inferences in first order logic, An exact algorithm for the constraint satisfaction problem: Application to logical inference

Uses Software

• Ltur
• XMP

Cites Work

• Unnamed Item
• Unnamed Item
• Polynomial-average-time satisfiability problems
• Resolution vs. cutting plane solution of inference problems: Some computational experience
• Some results and experiments in programming techniques for propositional logic
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• Solving propositional satisfiability problems
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Input Proofs and Rank One Cutting Planes
• The pivot and probe algorithm for solving a linear program
• A Computing Procedure for Quantification Theory
• The complexity of theorem-proving procedures