Ask Your Question
0

SAT Solver

asked 2013-11-03 22:44:00 +0100

pp gravatar image

From the documentation of sage.sat.boolean_polynomials.solve (here), it is not clear how to use it. Can anyone cite me any detailed example?

Say, I need to solve (in a Boolean ring) (x1 + x2 * x3 = x2)*(x2 = x3) . Can we do it?

Regards.

edit retag flag offensive close merge delete

1 Answer

Sort by ยป oldest newest most voted
2

answered 2013-11-04 04:56:50 +0100

tmonteil gravatar image

updated 2013-11-04 05:00:05 +0100

You can do:

sage: from sage.sat.boolean_polynomials import solve as solve_sat
sage: B.<x1,x2,x3> = BooleanPolynomialRing() ; B
Boolean PolynomialRing in x1, x2, x3
sage: f = (x1 + x2 * x3 - x2)*(x2 - x3) ; f
x1*x2 + x1*x3 + x2*x3 + x2
l = solve_sat([f], n=infinity) ; l
[{x3: 0, x2: 0, x1: 0},
 {x3: 1, x2: 1, x1: 1},
 {x3: 0, x2: 0, x1: 1},
 {x3: 1, x2: 1, x1: 0},
 {x3: 1, x2: 0, x1: 0},
 {x3: 0, x2: 1, x1: 1}]

It is possible that you will have to install the cryptominisat package first.

edit flag offensive delete link more

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

Stats

Asked: 2013-11-03 22:44:00 +0100

Seen: 350 times

Last updated: Nov 04 '13