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 43 articles , 1 standard article )
Showing results 1 to 20 of 43.
Sorted by year (- 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)
- 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)
- 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)
- Bonacina, Ilario; Galesi, Nicola: Pseudo-partitions, transversality and locality, a combinatorial characterization for the space measure in algebraic proof systems (2013)
- Brickenstein, Michael; Dreyer, Alexander: Gröbner-free normal forms for Boolean polynomials (2013)
- 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)
- Gao, Xiao-Shan; Huang, Zhenyu: Characteristic set algorithms for equation solving in finite fields (2012)
Further publications can be found at: http://polybori.sourceforge.net/doc/tutorial/tutorialli1.html#x6-510004.2