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

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.

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] 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.