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

DOI10.1007/BF01531074MaRDI QIDQ1356213zbMATH OpenOpenAlexFDO

Authors John N. Hooker, C. 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

inference problemspropositional logic

Mathematics Subject Classification ID

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

Recommendations

• Resolution vs. cutting plane solution of inference problems: Some computational experience
• Generalized resolution for 0--1 linear inequalities
• A Computational Study of Satisfiability Algorithms for Propositional Logic
• An exact algorithm for the constraint satisfaction problem: Application to logical inference

Cites work

• A Computing Procedure for Quantification Theory
• scientific article; zbMATH DE number 4053069 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• Input Proofs and Rank One Cutting Planes
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Polynomial-average-time satisfiability problems
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• Resolution vs. cutting plane solution of inference problems: Some computational experience
• Solving propositional satisfiability problems
• Some results and experiments in programming techniques for propositional logic
• The complexity of theorem-proving procedures
• The pivot and probe algorithm for solving a linear program

Cited in

(25)

• Resolution vs. cutting plane solution of inference problems: Some computational experience
• New methods for computing inferences in first order logic
• An exact algorithm for the constraint satisfaction problem: Application to logical inference
• Recognition of q-Horn formulae in linear time
• Easy problems are sometimes hard
• A complete adaptive algorithm for 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
• The Multi-SAT algorithm
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• What we can learn from conflicts in propositional satisfiability
• Generating hard satisfiability problems
• The satisfiability constraint gap
• A linear-time transformation of linear inequalities into conjunctive normal form
• Optimization methods in logic
• Learning from conflicts in propositional satisfiability
• scientific article; zbMATH DE number 1113999 (Why is no real title available?)
• scientific article; zbMATH DE number 1114456 (Why is no real title available?)
• GD-SAT model and crossover line
• Simplifying clausal satisfiability problems
• MaxSAT-based cutting planes for learning graphical models
• Computational experience with an interior point algorithm on the satisfiability problem

Describes a project that uses

Uses Software

• Ltur
• XMP

This page was built for publication: Branch-and-cut solution of inference problems in propositional logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1356213)