Branch-and-cut solution of inference problems in propositional logic
Tóm tắt
We describe and test computationally a branch-and-cut algorithm for solving inference problems in propositional logic. The problem is written as an integer program whose variables correspond to atomic propositions. We generate cuts for the integer program using a separation algorithm based on the resolution method for theorem proving. We find that the algorithm substantially reduces the size of the search tree when it is large. It is faster than Jeroslow and Wang's method on hard problems and slower on easy problems.
Tài liệu tham khảo
C. Blair, R.G. Jeroslow and J.K. Lowe, some results and experiments in programming techniques for propositional logic, Comp. Oper. Res. 13 (1988) 633–645.
S.A. Cook, The complexity of theorem-proving procedures,Proc. 3rd ACM Symp. on the Theory of Computing (1971) pp. 151–158.
M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM 7 (1960) 201–215.
W.F. Dowling and J.H. Gallier, Linear time algorithms for testing the satisfiability of Horn formulas, J. Logic Programming 3 (1984) 267–284.
J. Franco, On the probabilistic performance of algorithms for the satisfiability problem, Information Processing Lett. 23 (1986) 103–106.
J. Franco and M. Paul, Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem, Discrete Appl. Math. 5 (1983) 77–87.
M.R. Genesereth and N.J. Nilsson,Logical Foundations of Artificial Intelligence (Morgan Kaufmann, Los Altos, CA, 1987).
J.N. Hooker, Generalized resolution and cutting planes, Ann. Oper. Res. 12 (1988) 217–239.
J.N. Hooker, A quantitative approach to logical inference, Decision Support Systems 4 (1988) 45–69.
J.N. Hooker, Resolution vs cutting plane solution of inference problems: Some computational experience, Oper. Res. Lett. 7 (1988) 1–7.
J.N. Hooker, Input proofs and rank one cutting planes, ORSA J. Computing 1 (1989) 137–145.
R.G. Jeroslow and J. Wang, Solving propositional satisfiability problems, Ann. Math. AI 1 (1990) 167–187.
D.W. Loveland,Automated Theorem Proving: A Logical Basis (North-Holland, 1978).
E.R. Marsten, The design of the XMP linear programming library, ACM Trans. Math. Software 7 (1981) 481–497.
M. Minoux, LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation, Information Processing Lett. 29 (1988) 1–12.
P.W. Purdom and C.A. Brown, Polynomial-average-time satisfiability problems, Information Sci. 41 (1987) 23–42.
A.P. Sethi and G.L. Thompson, The pivot and probe algorithm for solving a linear program, Math. Programming 29 (1984) 219–233.