# 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 ]`

```magma
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 ${\bf F}_{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 ${\bf F}_{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 $[e_1, \ldots e_k]$, where each $e_i$ is a sequence of $n$ elements of ${\bf F}_{2}$, specifying that the potential solutions in $e_i$ are to be excluded (this is done by adding new relations to the system to exclude the $e_i$). The verbose information printed by MiniSat may be controlled by the parameter `Verbose`.

## `Example: SAT (ex-a37e10)`

In Example [Example: Solve Over GF2](groebner.md#example-ex-5d686d), 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.

```magma
> 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

```