SAT solver

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) : [ RngMPolBoolElt ] -> BoolElt, [ FldFinElt ]
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.

Example GB_SAT (H112E15)

In Example H112E5, 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
V2.28, 13 July 2023