Thanks very much for the reply. > Finally, for solving you should use a lexicographical term ordering: > > sage: R.<a111,a112,a121,a122,b111,b112,b211,b212,c111,c112> = > BooleanPolynomialRing(order='lex') > sage: I=(a111 * b111 * c111 + a112 * b112 * c112 - 1 , a111 * b211 * c111 + > ....: a112 * b212 * c112 - 0 , a121 * b111 * c111 + a122 * b112 * c112 , > ....: a121 * b211 * c111 + a122 * b212 * c112 - 1)*R > > sage: I.groebner_basis() > [a111 + b212, a112 + b211, a121 + b112, a122 + b111, c111 + 1, c112 + 1] > > Then, the Gröbner basis has a triangular shape and allows you to read the > solution. > > The introduction of my Diplomarbeit describes this in more detail: > > http://bit.ly/B4zdThttp://sage.math.washington.edu/home/malb/thesis-1.0.pdf >
Thanks, that's very helpful. > > Also, I read back in April that there was a plan to implement > > Faugere's F4 algorithm. > > There have been numerous attempts to implement F4 efficiently in the open- > source world but non of them succeeded to satisfaction. However, PolyBoRi's > SlimGB algorithm is heavily inspired by F4 and you can even use linear > algebra. PolyBoRi is used behind the scene when you construct a > BooleanPolynomialRing. > The problem in my case is really one of scale. I have put a larger example at the bottom of this message. When I try to find the groebner basis in sage 4.1 (which seems to use polybori-0.5rc.p8) the memory usage goes over 1.6GB and then sage crashes. It is possible that it just isn't realistic to solve it using Groebner Bases. However, I should say that when reformulated as a SAT solving problem, the standard off the shelf minisat 2.0 code can solve it in 0.04 seconds. This is despite the fact that minisat only takes CNF as the input which means that all the structure of the problem has been removed before it sees it. Raphael --- Larger example that crashes sage/polybori but which can be solved instantly by minisat --- R.<a111,a112,a113,a114,a115,a116,a117,a121,a122,a123,a124,a125,a126,a127,a211,a212,a213,a214,a215,a216,a217,a221,a222,a223,a224,a225,a226,a227,b111,b112,b113,b114,b115,b116,b117,b121,b122,b123,b124,b125,b126,b127,b211,b212,b213,b214,b215,b216,b217,b221,b222,b223,b224,b225,b226,b227,c111,c112,c113,c114,c115,c116,c117,c121,c122,c123,c124,c125,c126,c127,c211,c212,c213,c214,c215,c216,c217,c221,c222,c223,c224,c225,c226,c227> = BooleanPolynomialRing(order='lex') I = ( a111 * b111 * c111 + a112 * b112 * c112 + a113 * b113 * c113 + a114 * b114 * c114 + a115 * b115 * c115 + a116 * b116 * c116 + a117 * b117 * c117 -1, a111 * b111 * c121 + a112 * b112 * c122 + a113 * b113 * c123 + a114 * b114 * c124 + a115 * b115 * c125 + a116 * b116 * c126 + a117 * b117 * c127 , a111 * b111 * c211 + a112 * b112 * c212 + a113 * b113 * c213 + a114 * b114 * c214 + a115 * b115 * c215 + a116 * b116 * c216 + a117 * b117 * c217 , a111 * b111 * c221 + a112 * b112 * c222 + a113 * b113 * c223 + a114 * b114 * c224 + a115 * b115 * c225 + a116 * b116 * c226 + a117 * b117 * c227 , a111 * b121 * c111 + a112 * b122 * c112 + a113 * b123 * c113 + a114 * b124 * c114 + a115 * b125 * c115 + a116 * b126 * c116 + a117 * b127 * c117 , a111 * b121 * c121 + a112 * b122 * c122 + a113 * b123 * c123 + a114 * b124 * c124 + a115 * b125 * c125 + a116 * b126 * c126 + a117 * b127 * c127 , a111 * b121 * c211 + a112 * b122 * c212 + a113 * b123 * c213 + a114 * b124 * c214 + a115 * b125 * c215 + a116 * b126 * c216 + a117 * b127 * c217 -1, a111 * b121 * c221 + a112 * b122 * c222 + a113 * b123 * c223 + a114 * b124 * c224 + a115 * b125 * c225 + a116 * b126 * c226 + a117 * b127 * c227 , a111 * b211 * c111 + a112 * b212 * c112 + a113 * b213 * c113 + a114 * b214 * c114 + a115 * b215 * c115 + a116 * b216 * c116 + a117 * b217 * c117 , a111 * b211 * c121 + a112 * b212 * c122 + a113 * b213 * c123 + a114 * b214 * c124 + a115 * b215 * c125 + a116 * b216 * c126 + a117 * b217 * c127 , a111 * b211 * c211 + a112 * b212 * c212 + a113 * b213 * c213 + a114 * b214 * c214 + a115 * b215 * c215 + a116 * b216 * c216 + a117 * b217 * c217 , a111 * b211 * c221 + a112 * b212 * c222 + a113 * b213 * c223 + a114 * b214 * c224 + a115 * b215 * c225 + a116 * b216 * c226 + a117 * b217 * c227 , a111 * b221 * c111 + a112 * b222 * c112 + a113 * b223 * c113 + a114 * b224 * c114 + a115 * b225 * c115 + a116 * b226 * c116 + a117 * b227 * c117 , a111 * b221 * c121 + a112 * b222 * c122 + a113 * b223 * c123 + a114 * b224 * c124 + a115 * b225 * c125 + a116 * b226 * c126 + a117 * b227 * c127 , a111 * b221 * c211 + a112 * b222 * c212 + a113 * b223 * c213 + a114 * b224 * c214 + a115 * b225 * c215 + a116 * b226 * c216 + a117 * b227 * c217 , a111 * b221 * c221 + a112 * b222 * c222 + a113 * b223 * c223 + a114 * b224 * c224 + a115 * b225 * c225 + a116 * b226 * c226 + a117 * b227 * c227 , a121 * b111 * c111 + a122 * b112 * c112 + a123 * b113 * c113 + a124 * b114 * c114 + a125 * b115 * c115 + a126 * b116 * c116 + a127 * b117 * c117 , a121 * b111 * c121 + a122 * b112 * c122 + a123 * b113 * c123 + a124 * b114 * c124 + a125 * b115 * c125 + a126 * b116 * c126 + a127 * b117 * c127 , a121 * b111 * c211 + a122 * b112 * c212 + a123 * b113 * c213 + a124 * b114 * c214 + a125 * b115 * c215 + a126 * b116 * c216 + a127 * b117 * c217 , a121 * b111 * c221 + a122 * b112 * c222 + a123 * b113 * c223 + a124 * b114 * c224 + a125 * b115 * c225 + a126 * b116 * c226 + a127 * b117 * c227 , a121 * b121 * c111 + a122 * b122 * c112 + a123 * b123 * c113 + a124 * b124 * c114 + a125 * b125 * c115 + a126 * b126 * c116 + a127 * b127 * c117 , a121 * b121 * c121 + a122 * b122 * c122 + a123 * b123 * c123 + a124 * b124 * c124 + a125 * b125 * c125 + a126 * b126 * c126 + a127 * b127 * c127 , a121 * b121 * c211 + a122 * b122 * c212 + a123 * b123 * c213 + a124 * b124 * c214 + a125 * b125 * c215 + a126 * b126 * c216 + a127 * b127 * c217 , a121 * b121 * c221 + a122 * b122 * c222 + a123 * b123 * c223 + a124 * b124 * c224 + a125 * b125 * c225 + a126 * b126 * c226 + a127 * b127 * c227 , a121 * b211 * c111 + a122 * b212 * c112 + a123 * b213 * c113 + a124 * b214 * c114 + a125 * b215 * c115 + a126 * b216 * c116 + a127 * b217 * c117 -1, a121 * b211 * c121 + a122 * b212 * c122 + a123 * b213 * c123 + a124 * b214 * c124 + a125 * b215 * c125 + a126 * b216 * c126 + a127 * b217 * c127 , a121 * b211 * c211 + a122 * b212 * c212 + a123 * b213 * c213 + a124 * b214 * c214 + a125 * b215 * c215 + a126 * b216 * c216 + a127 * b217 * c217 , a121 * b211 * c221 + a122 * b212 * c222 + a123 * b213 * c223 + a124 * b214 * c224 + a125 * b215 * c225 + a126 * b216 * c226 + a127 * b217 * c227 , a121 * b221 * c111 + a122 * b222 * c112 + a123 * b223 * c113 + a124 * b224 * c114 + a125 * b225 * c115 + a126 * b226 * c116 + a127 * b227 * c117 , a121 * b221 * c121 + a122 * b222 * c122 + a123 * b223 * c123 + a124 * b224 * c124 + a125 * b225 * c125 + a126 * b226 * c126 + a127 * b227 * c127 , a121 * b221 * c211 + a122 * b222 * c212 + a123 * b223 * c213 + a124 * b224 * c214 + a125 * b225 * c215 + a126 * b226 * c216 + a127 * b227 * c217 -1, a121 * b221 * c221 + a122 * b222 * c222 + a123 * b223 * c223 + a124 * b224 * c224 + a125 * b225 * c225 + a126 * b226 * c226 + a127 * b227 * c227 , a211 * b111 * c111 + a212 * b112 * c112 + a213 * b113 * c113 + a214 * b114 * c114 + a215 * b115 * c115 + a216 * b116 * c116 + a217 * b117 * c117 , a211 * b111 * c121 + a212 * b112 * c122 + a213 * b113 * c123 + a214 * b114 * c124 + a215 * b115 * c125 + a216 * b116 * c126 + a217 * b117 * c127 -1, a211 * b111 * c211 + a212 * b112 * c212 + a213 * b113 * c213 + a214 * b114 * c214 + a215 * b115 * c215 + a216 * b116 * c216 + a217 * b117 * c217 , a211 * b111 * c221 + a212 * b112 * c222 + a213 * b113 * c223 + a214 * b114 * c224 + a215 * b115 * c225 + a216 * b116 * c226 + a217 * b117 * c227 , a211 * b121 * c111 + a212 * b122 * c112 + a213 * b123 * c113 + a214 * b124 * c114 + a215 * b125 * c115 + a216 * b126 * c116 + a217 * b127 * c117 , a211 * b121 * c121 + a212 * b122 * c122 + a213 * b123 * c123 + a214 * b124 * c124 + a215 * b125 * c125 + a216 * b126 * c126 + a217 * b127 * c127 , a211 * b121 * c211 + a212 * b122 * c212 + a213 * b123 * c213 + a214 * b124 * c214 + a215 * b125 * c215 + a216 * b126 * c216 + a217 * b127 * c217 , a211 * b121 * c221 + a212 * b122 * c222 + a213 * b123 * c223 + a214 * b124 * c224 + a215 * b125 * c225 + a216 * b126 * c226 + a217 * b127 * c227 -1, a211 * b211 * c111 + a212 * b212 * c112 + a213 * b213 * c113 + a214 * b214 * c114 + a215 * b215 * c115 + a216 * b216 * c116 + a217 * b217 * c117 , a211 * b211 * c121 + a212 * b212 * c122 + a213 * b213 * c123 + a214 * b214 * c124 + a215 * b215 * c125 + a216 * b216 * c126 + a217 * b217 * c127 , a211 * b211 * c211 + a212 * b212 * c212 + a213 * b213 * c213 + a214 * b214 * c214 + a215 * b215 * c215 + a216 * b216 * c216 + a217 * b217 * c217 , a211 * b211 * c221 + a212 * b212 * c222 + a213 * b213 * c223 + a214 * b214 * c224 + a215 * b215 * c225 + a216 * b216 * c226 + a217 * b217 * c227 , a211 * b221 * c111 + a212 * b222 * c112 + a213 * b223 * c113 + a214 * b224 * c114 + a215 * b225 * c115 + a216 * b226 * c116 + a217 * b227 * c117 , a211 * b221 * c121 + a212 * b222 * c122 + a213 * b223 * c123 + a214 * b224 * c124 + a215 * b225 * c125 + a216 * b226 * c126 + a217 * b227 * c127 , a211 * b221 * c211 + a212 * b222 * c212 + a213 * b223 * c213 + a214 * b224 * c214 + a215 * b225 * c215 + a216 * b226 * c216 + a217 * b227 * c217 , a211 * b221 * c221 + a212 * b222 * c222 + a213 * b223 * c223 + a214 * b224 * c224 + a215 * b225 * c225 + a216 * b226 * c226 + a217 * b227 * c227 , a221 * b111 * c111 + a222 * b112 * c112 + a223 * b113 * c113 + a224 * b114 * c114 + a225 * b115 * c115 + a226 * b116 * c116 + a227 * b117 * c117 , a221 * b111 * c121 + a222 * b112 * c122 + a223 * b113 * c123 + a224 * b114 * c124 + a225 * b115 * c125 + a226 * b116 * c126 + a227 * b117 * c127 , a221 * b111 * c211 + a222 * b112 * c212 + a223 * b113 * c213 + a224 * b114 * c214 + a225 * b115 * c215 + a226 * b116 * c216 + a227 * b117 * c217 , a221 * b111 * c221 + a222 * b112 * c222 + a223 * b113 * c223 + a224 * b114 * c224 + a225 * b115 * c225 + a226 * b116 * c226 + a227 * b117 * c227 , a221 * b121 * c111 + a222 * b122 * c112 + a223 * b123 * c113 + a224 * b124 * c114 + a225 * b125 * c115 + a226 * b126 * c116 + a227 * b127 * c117 , a221 * b121 * c121 + a222 * b122 * c122 + a223 * b123 * c123 + a224 * b124 * c124 + a225 * b125 * c125 + a226 * b126 * c126 + a227 * b127 * c127 , a221 * b121 * c211 + a222 * b122 * c212 + a223 * b123 * c213 + a224 * b124 * c214 + a225 * b125 * c215 + a226 * b126 * c216 + a227 * b127 * c217 , a221 * b121 * c221 + a222 * b122 * c222 + a223 * b123 * c223 + a224 * b124 * c224 + a225 * b125 * c225 + a226 * b126 * c226 + a227 * b127 * c227 , a221 * b211 * c111 + a222 * b212 * c112 + a223 * b213 * c113 + a224 * b214 * c114 + a225 * b215 * c115 + a226 * b216 * c116 + a227 * b217 * c117 , a221 * b211 * c121 + a222 * b212 * c122 + a223 * b213 * c123 + a224 * b214 * c124 + a225 * b215 * c125 + a226 * b216 * c126 + a227 * b217 * c127 -1, a221 * b211 * c211 + a222 * b212 * c212 + a223 * b213 * c213 + a224 * b214 * c214 + a225 * b215 * c215 + a226 * b216 * c216 + a227 * b217 * c217 , a221 * b211 * c221 + a222 * b212 * c222 + a223 * b213 * c223 + a224 * b214 * c224 + a225 * b215 * c225 + a226 * b216 * c226 + a227 * b217 * c227 , a221 * b221 * c111 + a222 * b222 * c112 + a223 * b223 * c113 + a224 * b224 * c114 + a225 * b225 * c115 + a226 * b226 * c116 + a227 * b227 * c117 , a221 * b221 * c121 + a222 * b222 * c122 + a223 * b223 * c123 + a224 * b224 * c124 + a225 * b225 * c125 + a226 * b226 * c126 + a227 * b227 * c127 , a221 * b221 * c211 + a222 * b222 * c212 + a223 * b223 * c213 + a224 * b224 * c214 + a225 * b225 * c215 + a226 * b226 * c216 + a227 * b227 * c217 , a221 * b221 * c221 + a222 * b222 * c222 + a223 * b223 * c223 + a224 * b224 * c224 + a225 * b225 * c225 + a226 * b226 * c226 + a227 * b227 * c227 -1)*R I.groebner_basis() --~--~---------~--~----~------------~-------~--~----~ To post to this group, send email to sage-support@googlegroups.com To unsubscribe from this group, send email to sage-support-unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sage-support URLs: http://www.sagemath.org -~----------~----~----~----~------~----~------~--~---
