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 43 articles , 1 standard article )

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

1 2 3 next

  1. Horáček, Jan; Kreuzer, Martin: On conversions from CNF to ANF (2020)
  2. Horáček, Jan; Kreuzer, Martin; Messeng Ekossono, Ange-Salomé: A signature based border basis algorithm (2020)
  3. Agudelo-Agudelo, Juan C.; Echeverri-Valencia, Santiago: Polynomial semantics for modal logics (2019)
  4. Garcia, Rebecca; Puente, Luis David García; Kruse, Ryan; Liu, Jessica; Miyata, Dane; Petersen, Ethan; Phillipson, Kaitlyn; Shiu, Anne: Gröbner bases of neural ideals (2018)
  5. Horáček, Jan; Kreuzer, Martin: 3BA: a border bases solver with a SAT extension (2018)
  6. Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc: CNFgen: a generator of crafted benchmarks (2017)
  7. Atserias, Albert; Lauria, Massimo; Nordström, Jakob: Narrow proofs may be maximally long (2016)
  8. Cifuentes, Diego; Parrilo, Pablo A.: Exploiting chordal structure in polynomial ideals: a Gröbner bases approach (2016)
  9. Quedenfeld, Frank-M.; Wolf, Christopher: Advanced algebraic attack on Trivium (2016)
  10. Filmus, Yuval; Lauria, Massimo; Nordström, Jakob; Ron-Zewi, Noga; Thapen, Neil: Space complexity in polynomial calculus (2015)
  11. Lundqvist, Samuel: Boolean ideals and their varieties (2015)
  12. 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)
  13. Nagai, Akira; Inoue, Shutaro: An implementation method of Boolean Gröbner bases and comprehensive Boolean Gröbner bases on general computer algebra systems (2014)
  14. Roanes-Lozano, Eugenio; Alonso, José Antonio; Hernando, Antonio: An approach from answer set programming to decision making in a railway interlocking system (2014)
  15. Sun, Yao; Wang, Dingkang: The implementation and complexity analysis of the branch Gröbner bases algorithm over Boolean polynomial rings (2014)
  16. Beck, Chris; Nordstrom, Jakob; Tang, Bangsheng: Some trade-off results for polynomial calculus (extended abstract) (2013)
  17. Bonacina, Ilario; Galesi, Nicola: Pseudo-partitions, transversality and locality, a combinatorial characterization for the space measure in algebraic proof systems (2013)
  18. Brickenstein, Michael; Dreyer, Alexander: Gröbner-free normal forms for Boolean polynomials (2013)
  19. 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)
  20. Gao, Xiao-Shan; Huang, Zhenyu: Characteristic set algorithms for equation solving in finite fields (2012)

1 2 3 next

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