Resolution vs. cutting plane solution of inference problems: Some computational experience

DOI10.1016/0167-6377(88)90044-2zbMath0639.90070OpenAlexW2088377032MaRDI QIDQ1100093

John N. Hooker

Publication date: 1988

Published in: Operations Research Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0167-6377(88)90044-2

zbMATH Keywords

cutting planesresolutionpropositional calculusinference problemsResolvents

Mathematics Subject Classification ID

Numerical mathematical programming methods (65K05) Integer programming (90C10)

Related Items

Inference of a minimum size Boolean function from examples by using a new efficient branch-and-bound approach, Improving the performance of enumerative search methods. I: Exploiting structure and intelligence, Branch-and-cut solution of inference problems in propositional logic, The state of SAT, Improving the performance of enumerative search methods. II: Computational experiments, A weight-balanced branching rule for SAT, Differential approximation of MIN SAT, MAX SAT and related problems, A BDD SAT solver for satisfiability testing: An industrial case study, Simplifying clausal satisfiability problems, Generating hard satisfiability problems, Some pitfalls for experimenters with random SAT, Probabilistic bounds and algorithms for the maximum satisfiability problem, The \(Multi\)-SAT algorithm, Mixed logical-linear programming, A dual algorithm for the satisfiability problem, Computational experience with an interior point algorithm on the satisfiability problem, A linear and discrete programming framework for representing qualitative knowledge, New methods for computing inferences in first order logic, Backtracking tactics in the backtrack method for SAT, An exact algorithm for the constraint satisfaction problem: Application to logical inference, Generating logical expressions from positive and negative examples via a branch-and-bound approach, Differential approximation for optimal satisfiability and related problems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Some results and experiments in programming techniques for propositional logic
• Solving propositional satisfiability problems
• Edmonds polytopes and a hierarchy of combinatorial problems
• Hard examples for resolution
• Input Proofs and Rank One Cutting Planes
• The relative efficiency of propositional proof systems
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory