# Package sat

This page is about the SAT package. For a function list see Category: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 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 . 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);

already yields the desired result.

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`

.