Hi!
I think the problem is quite hard using Gröbner bases, I also talked
to Gregory Bard about the topic in Sage days 10.
Nevertheless it is interesting.
Did you convert the polynomial system to cnf using Martins converter.
Does it also solve the bigger problem, you gave me?
Can you please give me some code snippet for the conversion?
I'd like to have some look into it.
I think Gregory said, the full problem is resistant against all
general sort of tricks and
algorithms.
>From what I understand about the algorithm, it is obvious, that you
can fix some ones or at least one, as it is highly symmetric.
Michael
On 3 Aug., 22:12, Michael Brickenstein <brickenst...@mfo.de> wrote:
> Hi!
> I can't sleep, when fearing PolyBoRi could calculate wrong:
> Actually, it's probably just about the wrapper.
> My CVS, which is very much the same as 0.6.3 gives me:
>
> l="a111,a112,a121,a122,b111,b112,b211,b212,c111,c112".split(",")
>
> In [2]:declare_ring(l, globals())
> Out[2]:<polybori.dynamic.PyPolyBoRi.Ring object at 0xb02578>
>
> In [3]:ideal=[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]
> In [4]:grogroebner/CVS groebner/libgroebner.a groebner/
> src
> groebner/doc groebner/libgroebner.so groebner_basis
>
> In [4]:groebner_basis(ideal)
> Out[4]:
> [b211*b212 + b211 + b212 + 1,
> b112*b212 + b112 + b212 + 1,
> b111*b212 + b112*b211 + 1,
> b111*b211 + b111 + b211 + 1,
> b111*b112 + b111 + b112 + 1,
> a122 + b111,
> a121 + b112,
> a112 + b211,
> a111 + b212,
> c111 + 1,
> c112 + 1]
>
> Tomorrow, I'll have a look at the bigger system, if there are some
> tweaks.
> Can you send it as proper attachment it to me? What kind of
> application is it?
> Michael
>
> On 3 Aug., 21:54, lesshaste <drr...@gmail.com> wrote:
>
> > Hi,
>
> > On Aug 3, 7:39 pm, Martin Albrecht <m...@informatik.uni-bremen.de>
> > wrote:
>
> > > > 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.
>
> > > Hi Raphael,
>
> > > note that Gröbner basis methods will always return a complete algebraic
> > > description of the solution set while SAT solving approaches terminate
> > > once
> > > *one* solution is found. Thus if there are many solutions they have an
> > > advantage. You can try to guess some variables in order to improve the
> > > efficiency of the Gröbner basis based methods.
>
> > You are quite right of course. My example wasn't fair as in this case
> > there are in fact a really large number of solutions.
>
> > However ( :) ) attached below is another slightly smaller example
> > where there is in fact no solution, making it a fairer comparison I
> > hope. It takes minisat 2 mins 22 seconds on my computer to work that
> > out. Using polybori in sage as above takes 700-800MB of RAM and
> > doesn't terminate in the hour or so I gave it. I only mention this in
> > case anyone working on polybori is interested in specific examples.
>
> > Raphael
>
> > ---- attached system of polys with no solution ---
> > R.<a111,a112,a113,a114,a115,a116,a121,a122,a123,a124,a125,a126,a211,a212,a2
> > 13,a214,a215,a216,a221,a222,a223,a224,a225,a226,b111,b112,b113,b114,b115,b1
> > 16,b121,b122,b123,b124,b125,b126,b211,b212,b213,b214,b215,b216,b221,b222,b2
> > 23,b224,b225,b226,c111,c112,c113,c114,c115,c116,c121,c122,c123,c124,c125,c1
> > 26,c211,c212,c213,c214,c215,c216,c221,c222,c223,c224,c225,c226
>
> > > = BooleanPolynomialRing(order='lex')
>
> > I = ( a111 * b111 * c111 + a112 * b112 * c112 + a113 * b113 * c113 +
> > a114 * b114 * c114 + a115 * b115 * c115 + a116 * b116 * c116 -1, a111
> > * b111 * c121 + a112 * b112 * c122 + a113 * b113 * c123 + a114 * b114
> > * c124 + a115 * b115 * c125 + a116 * b116 * c126 , a111 * b111 * c211
> > + a112 * b112 * c212 + a113 * b113 * c213 + a114 * b114 * c214 + a115
> > * b115 * c215 + a116 * b116 * c216 , a111 * b111 * c221 + a112 * b112
> > * c222 + a113 * b113 * c223 + a114 * b114 * c224 + a115 * b115 * c225
> > + a116 * b116 * c226 , a111 * b121 * c111 + a112 * b122 * c112 + a113
> > * b123 * c113 + a114 * b124 * c114 + a115 * b125 * c115 + a116 * b126
> > * c116 , a111 * b121 * c121 + a112 * b122 * c122 + a113 * b123 * c123
> > + a114 * b124 * c124 + a115 * b125 * c125 + a116 * b126 * c126 , a111
> > * b121 * c211 + a112 * b122 * c212 + a113 * b123 * c213 + a114 * b124
> > * c214 + a115 * b125 * c215 + a116 * b126 * c216 -1, a111 * b121 *
> > c221 + a112 * b122 * c222 + a113 * b123 * c223 + a114 * b124 * c224 +
> > a115 * b125 * c225 + a116 * b126 * c226 , a111 * b211 * c111 + a112 *
> > b212 * c112 + a113 * b213 * c113 + a114 * b214 * c114 + a115 * b215 *
> > c115 + a116 * b216 * c116 , a111 * b211 * c121 + a112 * b212 * c122 +
> > a113 * b213 * c123 + a114 * b214 * c124 + a115 * b215 * c125 + a116 *
> > b216 * c126 , a111 * b211 * c211 + a112 * b212 * c212 + a113 * b213 *
> > c213 + a114 * b214 * c214 + a115 * b215 * c215 + a116 * b216 * c216 ,
> > a111 * b211 * c221 + a112 * b212 * c222 + a113 * b213 * c223 + a114 *
> > b214 * c224 + a115 * b215 * c225 + a116 * b216 * c226 , a111 * b221 *
> > c111 + a112 * b222 * c112 + a113 * b223 * c113 + a114 * b224 * c114 +
> > a115 * b225 * c115 + a116 * b226 * c116 , a111 * b221 * c121 + a112 *
> > b222 * c122 + a113 * b223 * c123 + a114 * b224 * c124 + a115 * b225 *
> > c125 + a116 * b226 * c126 , a111 * b221 * c211 + a112 * b222 * c212 +
> > a113 * b223 * c213 + a114 * b224 * c214 + a115 * b225 * c215 + a116 *
> > b226 * c216 , a111 * b221 * c221 + a112 * b222 * c222 + a113 * b223 *
> > c223 + a114 * b224 * c224 + a115 * b225 * c225 + a116 * b226 * c226 ,
> > a121 * b111 * c111 + a122 * b112 * c112 + a123 * b113 * c113 + a124 *
> > b114 * c114 + a125 * b115 * c115 + a126 * b116 * c116 , a121 * b111 *
> > c121 + a122 * b112 * c122 + a123 * b113 * c123 + a124 * b114 * c124 +
> > a125 * b115 * c125 + a126 * b116 * c126 , a121 * b111 * c211 + a122 *
> > b112 * c212 + a123 * b113 * c213 + a124 * b114 * c214 + a125 * b115 *
> > c215 + a126 * b116 * c216 , a121 * b111 * c221 + a122 * b112 * c222 +
> > a123 * b113 * c223 + a124 * b114 * c224 + a125 * b115 * c225 + a126 *
> > b116 * c226 , a121 * b121 * c111 + a122 * b122 * c112 + a123 * b123 *
> > c113 + a124 * b124 * c114 + a125 * b125 * c115 + a126 * b126 * c116 ,
> > a121 * b121 * c121 + a122 * b122 * c122 + a123 * b123 * c123 + a124 *
> > b124 * c124 + a125 * b125 * c125 + a126 * b126 * c126 , a121 * b121 *
> > c211 + a122 * b122 * c212 + a123 * b123 * c213 + a124 * b124 * c214 +
> > a125 * b125 * c215 + a126 * b126 * c216 , a121 * b121 * c221 + a122 *
> > b122 * c222 + a123 * b123 * c223 + a124 * b124 * c224 + a125 * b125 *
> > c225 + a126 * b126 * c226 , a121 * b211 * c111 + a122 * b212 * c112 +
> > a123 * b213 * c113 + a124 * b214 * c114 + a125 * b215 * c115 + a126 *
> > b216 * c116 -1, a121 * b211 * c121 + a122 * b212 * c122 + a123 * b213
> > * c123 + a124 * b214 * c124 + a125 * b215 * c125 + a126 * b216 *
> > c126 , a121 * b211 * c211 + a122 * b212 * c212 + a123 * b213 * c213 +
> > a124 * b214 * c214 + a125 * b215 * c215 + a126 * b216 * c216 , a121 *
> > b211 * c221 + a122 * b212 * c222 + a123 * b213 * c223 + a124 * b214 *
> > c224 + a125 * b215 * c225 + a126 * b216 * c226 , a121 * b221 * c111 +
> > a122 * b222 * c112 + a123 * b223 * c113 + a124 * b224 * c114 + a125 *
> > b225 * c115 + a126 * b226 * c116 , a121 * b221 * c121 + a122 * b222 *
> > c122 + a123 * b223 * c123 + a124 * b224 * c124 + a125 * b225 * c125 +
> > a126 * b226 * c126 , a121 * b221 * c211 + a122 * b222 * c212 + a123 *
> > b223 * c213 + a124 * b224 * c214 + a125 * b225 * c215 + a126 * b226 *
> > c216 -1, a121 * b221 * c221 + a122 * b222 * c222 + a123 * b223 * c223
> > + a124 * b224 * c224 + a125 * b225 * c225 + a126 * b226 * c226 , a211
> > * b111 * c111 + a212 * b112 * c112 + a213 * b113 * c113 + a214 * b114
> > * c114 + a215 * b115 * c115 + a216 * b116 * c116 , a211 * b111 * c121
> > + a212 * b112 * c122 + a213 * b113 * c123 + a214 * b114 * c124 + a215
> > * b115 * c125 + a216 * b116 * c126 -1, a211 * b111 * c211 + a212 *
> > b112 * c212 + a213 * b113 * c213 + a214 * b114 * c214 + a215 * b115 *
> > c215 + a216 * b116 * c216 , a211 * b111 * c221 + a212 * b112 * c222 +
> > a213 * b113 * c223 + a214 * b114 * c224 + a215 * b115 * c225 + a216 *
> > b116 * c226 , a211 * b121 * c111 + a212 * b122 * c112 + a213 * b123 *
> > c113 + a214 * b124 * c114 + a215 * b125 * c115 + a216 * b126 * c116 ,
> > a211 * b121 * c121 + a212 * b122 * c122 + a213 * b123 * c123 + a214 *
> > b124 * c124 + a215 * b125 * c125 + a216 * b126 * c126 , a211 * b121 *
> > c211 + a212 * b122 * c212 + a213 * b123 * c213 + a214 * b124 * c214 +
> > a215 * b125 * c215 + a216 * b126 * c216 , a211 * b121 * c221 + a212 *
> > b122 * c222 + a213 * b123 * c223 + a214 * b124 * c224 + a215 * b125 *
> > c225 + a216 * b126 * c226 -1, a211 * b211 * c111 + a212 * b212 * c112
> > + a213 * b213 * c113 + a214 * b214 * c114 + a215 * b215 * c115 + a216
> > * b216 * c116 , a211 * b211 * c121 + a212 * b212 * c122 + a213 * b213
> > * c123 + a214 * b214 * c124 + a215 * b215 * c125 + a216 * b216 *
> > c126 , a211 * b211 * c211 + a212 * b212 * c212 + a213 * b213 * c213 +
> > a214 * b214 * c214 + a215 * b215 * c215 + a216 * b216 * c216 , a211 *
> > b211 * c221 + a212 * b212 * c222 + a213 * b213 * c223 + a214 * b214 *
> > c224 + a215 * b215 * c225 + a216 * b216 * c226 , a211 * b221 * c111 +
> > a212 * b222 * c112 + a213 * b223 * c113 + a214 * b224 * c114 + a215 *
> > b225 * c115 + a216 * b226 * c116 , a211 * b221 * c121 + a212 * b222 *
> > c122 + a213 * b223 * c123 + a214 * b224 * c124 + a215 * b225 * c125 +
> > a216 * b226 * c126 , a211 * b221 * c211 + a212 * b222 * c212 + a213 *
> > b223 * c213 + a214 * b224 * c214 + a215 * b225 * c215 + a216 * b226 *
> > c216 , a211 * b221 * c221 + a212 * b222 * c222 + a213 * b223 * c223 +
> > a214 * b224 * c224 + a215 * b225 * c225 + a216 * b226 * c226 , a221 *
> > b111 * c111 + a222 * b112 * c112 + a223 * b113 * c113 + a224 * b114 *
> > c114 + a225 * b115 * c115 + a226 * b116 * c116 , a221 * b111 * c121 +
> > a222 * b112 * c122 + a223 * b113 * c123 + a224 * b114 * c124 + a225 *
>
> ...
>
> Erfahren Sie mehr »
--~--~---------~--~----~------------~-------~--~----~
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
-~----------~----~----~----~------~----~------~--~---
