This work presents a new framework for Gröbner-basis computations with Boolean polynomials. Boolean polynomials can be modelled in a rather simple way, with both coefficients and degree per variable lying in {0,1}. The ring of Boolean polynomials is, however, not a polynomial ring, but rather the quotient ring of the polynomial ring over the field with two elements modulo the field equations x 2 =x for each variable x. Therefore, the usual polynomial data structures seem not to be appropriate for fast Gröbner-basis computations. We introduce a specialised data structure for Boolean polynomials based on zero-suppressed binary decision diagrams, which are capable of handling these polynomials more efficiently with respect to memory consumption and also computational speed. Furthermore, we concentrate on high-level algorithmic aspects, taking into account the new data structures as well as structural properties of Boolean polynomials. For example, a new useless-pair criterion for Gröbner-basis computations in Boolean rings is introduced. One of the motivations for our work is the growing importance of formal hardware and software verification based on Boolean expressions, which suffer-besides from the complexity of the problems -from the lack of an adequate treatment of arithmetic components. We are convinced that algebraic methods are more suited and we believe that our preliminary implementation shows that Gröbner-bases on specific data structures can be capable of handling problems of industrial size.

This software is also referenced in ORMS.

References in zbMATH (referenced in 36 articles , 1 standard article )

Showing results 1 to 20 of 36.
Sorted by year (citations)

1 2 next

  1. Cifuentes, Diego; Parrilo, Pablo A.: Exploiting chordal structure in polynomial ideals: a Gröbner bases approach (2016)
  2. Quedenfeld, Frank-M.; Wolf, Christopher: Advanced algebraic attack on Trivium (2016)
  3. Filmus, Yuval; Lauria, Massimo; Nordström, Jakob; Ron-Zewi, Noga; Thapen, Neil: Space complexity in polynomial calculus (2015)
  4. Lundqvist, Samuel: Boolean ideals and their varieties (2015)
  5. Chiu, Yi-Hao; Hong, Wei-Chih; Chou, Li-Ping; Ding, Jintai; Yang, Bo-Yin; Cheng, Chen-Mou: A practical attack on patched MIFARE Classic (2014)
  6. Nagai, Akira; Inoue, Shutaro: An implementation method of Boolean Gröbner bases and comprehensive Boolean Gröbner bases on general computer algebra systems (2014)
  7. Roanes-Lozano, Eugenio; Alonso, José Antonio; Hernando, Antonio: An approach from answer set programming to decision making in a railway interlocking system (2014)
  8. Sun, Yao; Wang, Dingkang: The implementation and complexity analysis of the branch Gröbner bases algorithm over Boolean polynomial rings (2014)
  9. Beck, Chris; Nordstrom, Jakob; Tang, Bangsheng: Some trade-off results for polynomial calculus (extended abstract) (2013)
  10. Bonacina, Ilario; Galesi, Nicola: Pseudo-partitions, transversality and locality, a combinatorial characterization for the space measure in algebraic proof systems (2013)
  11. Brickenstein, Michael; Dreyer, Alexander: Gröbner-free normal forms for Boolean polynomials (2013)
  12. Albrecht, Martin R.; Cid, Carlos; Faugère, Jean-Charles; Perret, Ludovic: On the relation between the MXL family of algorithms and Gröbner basis algorithms (2012)
  13. Gao, Xiao-Shan; Huang, Zhenyu: Characteristic set algorithms for equation solving in finite fields (2012)
  14. Hernando, Antonio; Roanes-Lozano, Eugenio; Maestre-Martínez, Roberto; Tejedor, Jorge: A logic-algebraic approach to decision taking in a railway interlocking system (2012)
  15. Knellwolf, Simon; Meier, Willi; Naya-Plasencia, María: Conditional differential cryptanalysis of trivium and KATAN (2012)
  16. Albrecht, Martin; Cid, Carlos; Dullien, Thomas; Faugère, Jean-Charles; Perret, Ludovic: Algebraic precomputations in differential and integral cryptanalysis (2011)
  17. Kalorkoti, K.: Model checking in the modal $\mu $-calculus and generic solutions (2011)
  18. Sato, Yosuke; Inoue, Shutaro; Suzuki, Akira; Nabeshima, Katsusuke; Sakai, Ko: Boolean Gröbner bases (2011)
  19. Wang, Meiqin; Sun, Yue; Mouha, Nicky; Preneel, Bart: Algebraic techniques in differential cryptanalysis revisited (2011)
  20. Zou, Yi Ming: Dynamics of Boolean networks (2011)

1 2 next

Further publications can be found at: http://polybori.sourceforge.net/doc/tutorial/tutorialli1.html#x6-510004.2