Groebner Bases Computation in Boolean Rings is P-SPACE

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.

Authors:

• Quoc-Nam Tran

Keywords:

• Algorithm
• Complexity
• Groebner basis
• Applications of Computer Science.

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.