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 sage-support+unsubscr...@googlegroups.com. To post to this group, send email to sage-support@googlegroups.com. Visit this group at http://groups.google.com/group/sage-support?hl=en. For more options, visit https://groups.google.com/groups/opt_out.
