On Clausal Equivalence and Hull Inclusion
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.
KeywordsPolynomial Time Lattice Point Polynomial Time Algorithm Truth Assignment Boolean Formula
Unable to display preview. Download preview PDF.
- 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
- 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