|
Magma V2.16 contains an interface to the {minisat}
satisfiability (SAT) solver. Such a solver is given a system
of boolean expressions in conjunctive normal form and determines
whether there is an assignment in the variables such that all
the expressions are satisfied. Magma supplies a function by
which one may transform a system of boolean polynomial equations into
an equivalent boolean system, and solve this via the SAT solver.
To use the interface function, the {minisat} program must currently
be installed as a command external to Magma. At the time of writing
(November 2009), the latest version of {minisat} can be
installed as follows on most Unix/Linux systems:
- (1)
- Download http://minisat.se/downloads/minisat2-070721.zip from
the {minisat} website (minisat.se).
- (2)
- Use the command unzip minisat2-070721.zip or equivalent to unzip
the files.
- (3)
- Change directory into minisat/core and run make there.
- (4)
- Copy the produced executable minisat into a place which is
in the current path when Magma is run.
SAT(B) : [ RngMPolElt ] -> BoolElt, [ FldFinElt ]
Exclude: [ RngMPolElt ] Default: []
Verbose: BoolElt Default: true
Given a sequence B of boolean polynomials in a rank-n boolean polynomial
ring (or a rank-n polynomial ring over GF(2)), call {minisat} on
the associated boolean system and return whether the system is satisfiable,
and if so, return also a solution S as a length-n sequence of elements of
GF(2). (This assumes that {minisat} is in the executable path of
external commands; see above for instructions for installing {minisat}).
The parameter Exclude may be set to a sequence [e1, ... ek],
where each ei is a sequence of n elements of GF(2), specifying
that the potential solutions in ei are to be excluded (this is
done by adding new relations to the system to exclude the ei).
The verbose information printed by {minisat} may be controlled by
the parameter Verbose.
In Example H115E5, we solved a boolean polynomial
system via the standard Gröbner basis method (which the function
Variety uses). Here we solve the same system via the SAT solver.
Each time we obtain a solution, we can call the function again,
but excluding the solution(s) already found. We can thus find
all the solutions to the system. Of course, this is not worth doing
when there are large numbers of solutions, but it may be of interest
to find all solutions when it is expected there is a small number
of solutions.
> P<a,b,c,d,e> := BooleanPolynomialRing(5, "grevlex");
> B := [a*b + c*d + 1, a*c*e + d*e, a*b*e + c*e, b*c + c*d*e + 1];
> l, S := SAT(B);
> l;
true
> S;
[ 1, 1, 1, 0, 0 ]
> Universe(S);
Finite field of size 2
> [Evaluate(f, S): f in B];
[ 0, 0, 0, 0 ]
> l, S2 := SAT(B: Exclude := [S]);
> l;
true
> S2;
[ 0, 1, 1, 1, 0 ]
> [Evaluate(f, S2): f in B];
[ 0, 0, 0, 0 ]
> l, S3 := SAT(B: Exclude := [S, S2]);
> l;
false
[Next][Prev] [Right] [Left] [Up] [Index] [Root]
|