A class of logic problems solvable by linear programming

ABSTRACT

In propositional logic, several problems, such as satisfiability, MAX SAT and logical inference, can be formulated as integer programs. In this paper, we consider sets of clauses for which the corresponding integer programs can be solved as linear programs. We prove that balanced sets of clauses have this property.

REFERENCES

• 1: ~BERGE, C. 1970. Sur certains hypergraphes gdndralisant les graphes bipartltes. In Combinato- ~rial Theory and its Applications I, P. Erd6s, A. R~nyi and V. S6s eds. Colloq. Math. Soc. Jcinos ~Bolyat vol. 4. North-Holland, Amsterdam, The Netherlands, 119-133.
• 2: ~BEV, GE, C. 1972. Balanced matrices. Math. Prog. 2, 19-31.
• 3: V. Chandru , J. N. Hooker, Extended Horn sets in propositional logic, Journal of the ACM (JACM), v.38 n.1, p.205-221, Jan. 1991 [doi>10.1145/102782.102789]
• 4: ~CONFOr, TI, M., COr~4U~JOLS, AND RAO, M.R. 1991. Decomposition of balanced matrices, Parts ~I-VII, preprints. MSRR 569-575, GSIA, Carnegie-Mellon Univ. Pittsburgh, Pa.
• 5: ~CONFORTI, M., CORNUEJOLS, G., KAPOOR, A., AND VUSKOVIC, K. 1994a. Balanced 0, _+ 1 ~matrices, Parts I, II, preprints. GSIA, Carnegie-Mellon Univ. Pittsburgh, Pa.
• 6: ~CONFORTI, M., CORNUEJOLS, G., KAPOOR, A., RAO, M. R., VUSKOVIC, K. 1994b. Balanced ~matrices. In Mathematical Pt'ogrammztzg: State of the Art 1994, J. R. Birge and K. G. Murty eds. ~Univ. Michigan, pp, 1-33.
• 7: ~DANTZIG, G.B. 1963. Linear Programming and Extensions. Princeton University Press, Prince- ~ton, N.J.
• 8: ~FULKERSON, D. R., HOFFMAN, A., AND HOPPENHE1M, R. 1974. On balanced matrices. Math. ~Prog. Study 1, 120-132.
• 9: J. N. Hooker, A quantitative approach to logical inference, Decision Support Systems, v.4 n.1, p.45-69, March 1988 [doi>10.1016/0167-9236(88)90097-8]
• 10: Alexandeer Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 11: ~TRUEMPER, K. 1982. Alpha-balanced graphs and matrices and GF(3)-representability of ma- ~troids. J Combitz. Theory B 32, 112-139.
• 12: ~TRUEMPER, K. 1990. Polynomial theorem proving I. Central matrices. Tech. Rep. UTDCS ~34-90. Univ. Texas at Dallas, Dallas, Tex.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization
          Subjects: Linear programming

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization
          Subjects: Integer programming

General Terms:
Algorithms

Keywords:
balanced matrices, linear programming, propositional logic