Groebner Bases Computation in Boolean Rings is P-SPACE

Authors: Quoc-Nam Tran

Abstract:

The theory of Groebner Bases, which has recently been honored with the ACM Paris Kanellakis Theory and Practice Award, has become a crucial building block to computer algebra, and is widely used in science, engineering, and computer science. It is wellknown that Groebner bases computation is EXP-SPACE in a general polynomial ring setting. However, for many important applications in computer science such as satisfiability and automated verification of hardware and software, computations are performed in a Boolean ring. In this paper, we give an algorithm to show that Groebner bases computation is PSPACE in Boolean rings. We also show that with this discovery, the Groebner bases method can theoretically be as efficient as other methods for automated verification of hardware and software. Additionally, many useful and interesting properties of Groebner bases including the ability to efficiently convert the bases for different orders of variables making Groebner bases a promising method in automated verification.

Keywords: Algorithm, Complexity, Groebner basis, Applications of Computer Science.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1078835

References:

[1] G. S. Avrunin. Symbolic model checking using algebraic geometry. In CAV -96: Proceedings of the 8th International Conference on Computer Aided Verification, pages 26-37, London, UK, 1996. Springer-Verlag.
[2] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of Design Automation Conference (DAC-99), 1999.
[3] B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-dimensional Polynomial Ideal (in German). PhD thesis, Institute of Mathematics, Univ. Innsbruck, Innsbruck, Austria, 1965.
[4] B. Buchberger. Groebner Bases: An algorithmic method in polynomial ideal theory. In N. K. Bose, editor, Multidimensional Systems Theory, chapter 6, pages 184-232. Reidel Publishing Company, Dodrecht, 1985.
[5] S. N. Burris and H. P. Sankappanavar. A Course in Universal Algebra. Springer-Verlag, 1981.
[6] S. Collart, M. Kalkbrener, and D. Mall. Converting bases with the Groebner walk. Journal of Symbolic Computation, 24(3/4):465-469, 1997.
[7] L. Csanky. Fast parallel matrix conversion algorithms. SIAM J. Comput., 5:618-623, 1976.
[8] N. Dershowitz, J. Hsiang, G. Huang, and D. Kaiss. Boolean ring satisfiability.
[9] N. Dershowitz, J. Hsiang, G. Huang, and D. Kaiss. Intersection-based methods for satisfiability using boolean rings.
[10] T. D. Dub'e. The structure of polynomial ideals and Groebner bases. SIAM J. Comput., 19(4):750-773, 1990.
[11] S. Fortune and J. Wyllie. Parallelism in random access machines. In Proceedings of the 10th annual ACM symposium on Theory of Computing, pages 114-118. ACM Press, 1978.
[12] Z. Galil and V. Pan. Parallel evaluation of the determinant and of the inverse of a matrix. Inform. Proc. Lett., 30:41-45, 1989.
[13] G. Hermann. Die Frage der endlich vielen Schritte in der Theorie der Polynomideale. Mathematische Annalen, 95:736-788, 1925.
[14] J. Hsiang. Refutational theorem proving using term rewriting systems. Artificial Intelligence, 25:255-300, 1985.
[15] G. Huang, N. Dershowitz, and J. Hsiang. Satisfiability testing using simplification in boolean rings.
[16] O. Ibarra, S. Moran, and L. Rosier. A note on the parallel complexity of computing the rank of order n matrices. Inform. Proc. Lett, 11(4):162, 1980.
[17] D. Kaiss and N. Dershowitz. Boosting satisfiability testing using boolean rings.
[18] K. Kuehnle and E. Mayr. Exponential space computation of groebner bases. In Proceedings of ISSAC. ACM, 1996.
[19] O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, 2000.
[20] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
[21] F. Preparata and D. Sarwata. An improved parallel processor bound in fast matrix inversion. Inform. Proc. Lett., 1978.
[22] M. Sipser. Introduction to the Theory of Computation. PWS Publishing, Boston, 2nd edition, 1997.
[23] M. Sipser. Introduction to the Theory of Computation. Course Technology, 2nd edition, 2005.
[24] M. Stone. The theory of representation for boolean algebras. Trans. Amer. Math. Soc., 1936.
[25] M. Stone. Applications of the theory of boolean rings to general topology. Trans. Amer. Math. Soc., 1937.
[26] Q.-N. Tran. A fast algorithm for Groebner basis conversion and its applications. Journal of Symbolic Computation, 30:451-468, 2000.
[27] Q.-N. Tran. A new class of term orders for elimination and applications. Journal of Symbolic Computation, 42, 2007.
[28] Q.-N. Tran and M. Y. Vardi. Groebner bases computation in boolean rings for symbolic model checking. In Proceedings of IASTED 2007 Conference on Modeling and Simulation, 2007.
[29] F. Winkler. Polynomial Algorithms in Computer Algebra. Texts and Monographs in Symbolic Computation. Springer-Verlag, 1996.