Solving propositional satisfiability problems

Springer Science and Business Media LLC - Tập 1 Số 1-4 - Trang 167-187 - 1990
Robert G. Jeroslow1, Jinchang Wang1
1College of Management, Georgia Institute of Technology, Atlanta, USA 30332#TAB#

Tóm tắt

Từ khóa


Tài liệu tham khảo

C.E. Blair and R.G. Jeroslow, unpublished notes.

C.E. Blair, R.G. Jeroslow and J.K. Lowe, Some results and experiments on programming techniques for propositional logic (January 1986) to appear in Comp. Oper. Res.

S.A. Cook, The complexity of theorem proving procedures,Proc. 3rd SIGACT Symp. (1971) pp. 151–158.

M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM 8 (1960) 201–215.

W.F. Dowling and J.H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, Logic Programming 3 (1984) 267–284.

J. Franco and M. Paull, Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem, Discr. Appl. Math. 5 (1983) 77–87.

M. Garey and D. Johnson,Computers and Intractibility (W.H. Freeman, 1979).

R.G. Jeroslow, Notes for Rutgers Lectures, Mixed integer model formulation for logic-based decision support (1986).

R.M. Karp, Reducibility among combinatorial problems, in:Complexity of Computer Computations, eds. R.E. Miller and J.W. Thatcher (Plenum, New York, 1972) pp. 85–104.

D.W. Loveland,Automated Theorem Proving: A Logical Basis (North-Holland, Amsterdam, 1978).

J.K. Lowe, Modelling with integer variables, Ph.D. Thesis, Georgia Institute of Technology (March 1984).

A.J. Nevins, A human oriented logic for automatic theorem-proving, J.ACM 21 (1974) 606–621.

P.W. Purdom, Jr., Solving satisfiability with less searching correspondence, IEEE Trans. Pattern Anal. Machine Intell. PAMI-6 (July 1984).