On Clausal Equivalence and Hull Inclusion

  • K. Subramani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


This paper is concerned with threee closely related problems, viz., checking boolean equivalence of CNF formulas, deciding hull inclusion (linear and integer) in certain polyhedral families and determining the satisfiability of CNF formulas. With the exception of linear hull inclusion, these problems are provably “hard” in that there are instances of these problems that are complete for classes, which are not known to be tractable. In the case of satisfiability testing, we design a simple randomized algorithm for the problem of checking whether a Q2CNF formula has a model.


Polynomial Time Lattice Point Polynomial Time Algorithm Truth Assignment Boolean Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aspvall, B., Plass, M.F., Tarjan, R.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information Processing Letters 8(3) (1979)Google Scholar
  2. 2.
    Bazaraa, M.S., Sherali, H.D., Shetty, C.M.: Nonlinear Programming: Theory and Algorithms, 2nd edn. John Wiley, New York (1993)zbMATHGoogle Scholar
  3. 3.
    Kleine Buning, H., Karpinski, M., Flogel, A.: Resolution for quantified Boolean formulas. Information and Computation 117, 12–18 (1995)CrossRefMathSciNetGoogle Scholar
  4. 4.
    Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. John Wiley&Sons, New York (1999)zbMATHGoogle Scholar
  5. 5.
    Papadimitriou, C.H.: On selecting a satisfying truth assignment. In: IEEE (ed.) Proceedings: 32nd annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, October 1–4, pp. 163–169. IEEE Computer Society Press, Los Alamitos (1991)CrossRefGoogle Scholar
  6. 6.
    Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)zbMATHGoogle Scholar
  7. 7.
    Ross, S.M.: Probability Models, 7th edn. Academic Press, Inc., London (2000)zbMATHGoogle Scholar
  8. 8.
    Schaefer, T.J.: The complexity of satisfiability problems. In: Aho, A. (ed.) Proceedings of the 10th Annual ACM Symposium on Theory of Computing, pp. 216–226. ACM Press, New York (1978)CrossRefGoogle Scholar
  9. 9.
    Subramani, K.: On identifying simple and quantified lattice points in the 2sat polytope. In: Calmet, J., Benhamou, B., Caprotti, O., Hénocque, L., Sorge, V. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol. 2385, pp. 217–230. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Vaidya, P.M.: An algorithm for linear programming which requires O(((m+n)n2+ (m+n)1.5n)L)arithmetic operations. In: Aho, A. (ed.) Proceedings of the 19th Annual ACM Symposium on Theory of Computing, pp. 29–38. ACM Press, New York (1987)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • K. Subramani
    • 1
  1. 1.LCSEEWest Virginia UniversityMorgantown

Personalised recommendations