Polybori: A framework for Gröbner-basis computations with Boolean polynomials. 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 49 articles , 1 standard article )

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

1 2 3 next

  1. Huang, Zhenyu; Sun (c), Yao; Lin, Dongdai: On the efficiency of solving Boolean polynomial systems with the characteristic set method (2021)
  2. Indrøy, John Petter; Costes, Nicolas; Raddum, Håvard: Boolean polynomials, BDDs and CRHS equations -- connecting the dots with CryptaPath (2021)
  3. Horáček, Jan; Kreuzer, Martin: On conversions from CNF to ANF (2020)
  4. Horáček, Jan; Kreuzer, Martin; Messeng Ekossono, Ange-Salomé: A signature based border basis algorithm (2020)
  5. Agudelo-Agudelo, Juan C.; Echeverri-Valencia, Santiago: Polynomial semantics for modal logics (2019)
  6. 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)
  7. Horáček, Jan; Kreuzer, Martin: 3BA: a border bases solver with a SAT extension (2018)
  8. Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc: CNFgen: a generator of crafted benchmarks (2017)
  9. Atserias, Albert; Lauria, Massimo; Nordström, Jakob: Narrow proofs may be maximally long (2016)
  10. Cifuentes, Diego; Parrilo, Pablo A.: Exploiting chordal structure in polynomial ideals: a Gröbner bases approach (2016)
  11. Hernando, Antonio; Maestre-Martínez, Roberto; Roanes-Lozano, Eugenio: A natural language for implementing algebraically expert systems (2016)
  12. Maestre-Martínez, Roberto; Hernando, Antonio; Roanes-Lozano, Eugenio: An algebraic approach for detecting nearly dangerous situations in expert systems (2016)
  13. Quedenfeld, Frank-M.; Wolf, Christopher: Advanced algebraic attack on Trivium (2016)
  14. Filmus, Yuval; Lauria, Massimo; Nordström, Jakob; Ron-Zewi, Noga; Thapen, Neil: Space complexity in polynomial calculus (2015)
  15. Hernando, Antonio; Roanes-Lozano, Eugenio: An algebraic model for implementing expert systems based on the knowledge of different experts (2015)
  16. Lundqvist, Samuel: Boolean ideals and their varieties (2015)
  17. 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)
  18. Nagai, Akira; Inoue, Shutaro: An implementation method of Boolean Gröbner bases and comprehensive Boolean Gröbner bases on general computer algebra systems (2014)
  19. Roanes-Lozano, Eugenio; Alonso, José Antonio; Hernando, Antonio: An approach from answer set programming to decision making in a railway interlocking system (2014)
  20. Sun, Yao; Wang, Dingkang: The implementation and complexity analysis of the branch Gröbner bases algorithm over Boolean polynomial rings (2014)

1 2 3 next

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