The output is correct:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.boolean_polynomials import solve as solve_sat
sage: solve_sat([a*b],n=infinity)
[{b: 1, a: 0}, {b: 0, a: 0}, {b: 0, a: 1}]
i.e., the solver returns all valid solutions for a*b. In more detail:
p cnf 4 4
1 -4 0
2 -4 0
4 -1 -2 0
-4 0
means (if w == 4)
(a | -w) & (b | -w) & (w | -a | -b) <=> w == a*b
a = 0, => w = 0 (first clause)
a = 0 => w = 0 (second clause)
a = 1, b=1 => w = 1 (third clause)
On Wednesday 13 Mar 2013, 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?
Cheers,
Martin
--
name: Martin Albrecht
_pgp: http://pgp.mit.edu:11371/pks/lookup?op=get&search=0x8EF0DC99
_otr: 47F43D1A 5D68C36F 468BAEBA 640E8856 D7951CCF
_www: http://martinralbrecht.wordpress.com/
_jab: [email protected]
--
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.
