# Difference between revisions of "Package sat"

The basic idea behind this package is to make SAT solver, like CryptoMiniSat, usable in/with ApCoCoA.

This package allows to solve polynomial systems over ${\displaystyle \mathbb {Z} /2\mathbb {Z} }$ by first converting the system to CNF-SAT in DIMACS format and then using a SAT solver to solve the resulting conjunctive normal form. More informations about the conversion can be found in the paper Algebraic Attacks Using SAT-Solvers by Philipp Jovanovic, the author of this package, and Martin Kreuzer.

Important: The SAT executable must be in packages/binaries and you must have the permissions to read and write in the directory packages/temp in the CoCoA plugin folder.

For further informations about SAT-Solver and the DIMACS format see the following links:

MiniSat [1], CryptoMiniSat [2], DIMACS [3]

## Usage

Let `S` be a list of polynomials in a polynomial ring `P` over the field ${\displaystyle \mathbb {Z} /2\mathbb {Z} }$. Then we can use this package to find a common zero of the polynomials in `S`, i.e. a list `b = [b1,...,bn]` such that `[eval(f,b) | f in S] = [0,...,0]`. This can be achieved by either using the single function `SAT.Solve` or with the functions `SAT.ConvertToCNF`, `SAT.LaunchCryptoMiniSat` and `SAT.GetResult` together.

In the first case, the simple call

```SAT.Solve(S);
```

The second method works as follows. First, the call

```CNFPath := SAT.ConvertToCNF(S,CuttingLength,QStrategy,CStrategy);
```

converts the polynomial system into standard CNF form and writes it in DIMACS format to a new file in the `/packages/temp/` directory whose name is not assigned yet. The (absolute) path of the file is returned by the function and in this example stored in the variable `CNFPath`. For more informations about `CuttingLength`, `QStrategy` and `CStrategy`, see Package sat/SAT.ConvertToCNF or the paper linked above. Afterwards, the function

```SolPath := SAT.LaunchCryptoMiniSat(CNFPath);
```

launches CryptoMiniSat with the file in `CNFPath` as input and stores the solution in a new file. As above, the (absolute) path of the solution file is returned and in this example stored in the variable `SolPath`. Then, one can use the function

```SAT.GetResult(SolPath,P);
```

that converts the result back into CoCoA and returns a solution `[b1,...,bn]` of the system `S` in form of a list with entries in `P`.