Mr. Martin,
Thanks for replying quickly on my previous post. But we also have the fourth clause -4 0 which creates a problem when a = b= 1, because: (w ' )(a + w ' )(b + w ' )(w + a ' + b ' ) = 1 at a = b = 1, gives (w ')(w) = 1, which is an inconsistent equation. On Wednesday, March 13, 2013 3:36:09 PM UTC+5:30, akhil wrote: > > Hello, > > > I am using SAGE builtin anf2cnf.py converter, but the DIMACS output > returned is incorrect, when verified by multiplying the CNF clauses. Sample > code: > > B.<a,b,c> = BooleanPolynomialRing() > from sage.sat.converters.polybori import CNFEncoder > from sage.sat.solvers.dimacs import DIMACS > fn = tmp_filename() > solver = DIMACS(filename=fn) > e = CNFEncoder(solver, B) > e.clauses_dense(a*b) > _ = solver.write() > print open(fn).read() > > Output returned: > > p cnf 4 4 > 1 -4 0 > 2 -4 0 > 4 -1 -2 0 > -4 0 > > Here 4 is the index for the monomial a*b. On multiplying these clauses, > the answer comes as a' + b', and not a*b as required. > > Can anybody please help? > > > -- You received this message because you are subscribed to the Google Groups "sage-support" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/sage-support?hl=en. For more options, visit https://groups.google.com/groups/opt_out.
