PolyBoRi
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.
This software is also referenced in ORMS.
Keywords for this software
References in zbMATH (referenced in 48 articles , 1 standard article )
Showing results 1 to 20 of 48.
Sorted by year (- Huang, Zhenyu; Sun (c), Yao; Lin, Dongdai: On the efficiency of solving Boolean polynomial systems with the characteristic set method (2021)
- Horáček, Jan; Kreuzer, Martin: On conversions from CNF to ANF (2020)
- Horáček, Jan; Kreuzer, Martin; Messeng Ekossono, Ange-Salomé: A signature based border basis algorithm (2020)
- Agudelo-Agudelo, Juan C.; Echeverri-Valencia, Santiago: Polynomial semantics for modal logics (2019)
- 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)
- Horáček, Jan; Kreuzer, Martin: 3BA: a border bases solver with a SAT extension (2018)
- Lauria, Massimo; Elffers, Jan; Nordström, Jakob; Vinyals, Marc: CNFgen: a generator of crafted benchmarks (2017)
- Atserias, Albert; Lauria, Massimo; Nordström, Jakob: Narrow proofs may be maximally long (2016)
- Cifuentes, Diego; Parrilo, Pablo A.: Exploiting chordal structure in polynomial ideals: a Gröbner bases approach (2016)
- Hernando, Antonio; Maestre-Martínez, Roberto; Roanes-Lozano, Eugenio: A natural language for implementing algebraically expert systems (2016)
- Maestre-Martínez, Roberto; Hernando, Antonio; Roanes-Lozano, Eugenio: An algebraic approach for detecting nearly dangerous situations in expert systems (2016)
- Quedenfeld, Frank-M.; Wolf, Christopher: Advanced algebraic attack on Trivium (2016)
- Filmus, Yuval; Lauria, Massimo; Nordström, Jakob; Ron-Zewi, Noga; Thapen, Neil: Space complexity in polynomial calculus (2015)
- Hernando, Antonio; Roanes-Lozano, Eugenio: An algebraic model for implementing expert systems based on the knowledge of different experts (2015)
- Lundqvist, Samuel: Boolean ideals and their varieties (2015)
- 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)
- Nagai, Akira; Inoue, Shutaro: An implementation method of Boolean Gröbner bases and comprehensive Boolean Gröbner bases on general computer algebra systems (2014)
- Roanes-Lozano, Eugenio; Alonso, José Antonio; Hernando, Antonio: An approach from answer set programming to decision making in a railway interlocking system (2014)
- Sun, Yao; Wang, Dingkang: The implementation and complexity analysis of the branch Gröbner bases algorithm over Boolean polynomial rings (2014)
- Beck, Chris; Nordstrom, Jakob; Tang, Bangsheng: Some trade-off results for polynomial calculus (extended abstract) (2013)
Further publications can be found at: http://polybori.sourceforge.net/doc/tutorial/tutorialli1.html#x6-510004.2