A P-SPACE Algorithm for Groebner Bases Computation in Boolean Rings

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 setting. In this paper, we give an algorithm to show that Groebner bases computation is P-SPACE 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.1334139

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] P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, and P. Pudlak. Lower bounds on Hilbert-s nullstellansatz and propositional proofs. In Proceddings of the 35th Annual Symposium on Foundations of Computer Science, pages 794-806, Santa Fe, NM, 1994.
[3] 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.
[4] 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.
[5] 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.
[6] S. N. Burris and H. P. Sankappanavar. A Course in Universal Algebra. Springer-Verlag, 1981.
[7] M. Clegg, J. Edmonds, and R. Impagliazzo. Using Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of STOC-96, pages 174-183, Philadelphia, PA, USA, 1996. ACM.
[8] S. Collart, M. Kalkbrener, and D. Mall. Converting bases with the Groebner walk. Journal of Symbolic Computation, 24(3/4):465-469, 1997.
[9] L. Csanky. Fast parallel matrix conversion algorithms. SIAM J. Comput., 5:618-623, 1976.
[10] N. Dershowitz, J. Hsiang, G. Huang, and D. Kaiss. Boolean ring satisfiability.
[11] N. Dershowitz, J. Hsiang, G. Huang, and D. Kaiss. Intersection-based methods for satisfiability using boolean rings.
[12] T. D. Dub'e. The structure of polynomial ideals and Groebner bases. SIAM J. Comput., 19(4):750-773, 1990.
[13] 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.
[14] Z. Galil and V. Pan. Parallel evaluation of the determinant and of the inverse of a matrix. Inform. Proc. Lett., 30:41- 45, 1989.
[15] G. Hermann. Die Frage der endlich vielen Schritte in der Theorie der Polynomideale. Mathematische Annalen, 95:736-788, 1925.
[16] J. Hsiang. Refutational theorem proving using term rewriting systems. Artificial Intelligence, 25:255-300, 1985.
[17] G. Huang, N. Dershowitz, and J. Hsiang. Satisfiability testing using simplification in boolean rings.
[18] 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.
[19] D. Kaiss and N. Dershowitz. Boosting satisfiability testing using boolean rings.
[20] K. Kuehnle and E. Mayr. Exponential space computation of groebner bases. In Proceedings of ISSAC. ACM, 1996.
[21] O. Kupferman, M. Vardi, and P. Wolper. An automatatheoretic approach to branching-time model checking. Journal of the ACM, 47(2):312-360, 2000.
[22] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
[23] F. Preparata and D. Sarwata. An improved parallel processor bound in fast matrix inversion. Inform. Proc. Lett., 1978.
[24] M. Sipser. Introduction to the Theory of Computation. PWS Publishing, Boston, 2nd edition, 1997.
[25] M. Sipser. Introduction to the Theory of Computation. Course Technology, 2nd edition, 2005.
[26] M. Stone. The theory of representation for boolean algebras. Trans. Amer. Math. Soc., 1936.
[27] M. Stone. Applications of the theory of boolean rings to general topology. Trans. Amer. Math. Soc., 1937.
[28] Q.-N. Tran. A fast algorithm for Groebner basis conversion and its applications. Journal of Symbolic Computation, 30:451-468, 2000.
[29] Q.-N. Tran. A new class of term orders for elimination and applications. Journal of Symbolic Computation, 42, 2007.
[30] 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.
[31] F. Winkler. Polynomial Algorithms in Computer Algebra. Texts and Monographs in Symbolic Computation. Springer-Verlag, 1996.