Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Bazaraa, M.S., Sherali, H.D., Shetty, C.M.: Nonlinear Programming: Theory and Algorithms, 2nd edn. John Wiley, New York (1993)
Kleine Buning, H., Karpinski, M., Flogel, A.: Resolution for quantified Boolean formulas. Information and Computation 117, 12–18 (1995)
Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. John Wiley&Sons, New York (1999)
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)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)
Ross, S.M.: Probability Models, 7th edn. Academic Press, Inc., London (2000)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Subramani, K. (2003). On Clausal Equivalence and Hull Inclusion. In: Blundo, C., Laneve, C. (eds) Theoretical Computer Science. ICTCS 2003. Lecture Notes in Computer Science, vol 2841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45208-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-45208-9_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20216-5
Online ISBN: 978-3-540-45208-9
eBook Packages: Springer Book Archive