Package sat

This article is about a function from ApCoCoA-2. If you are looking for the ApCoCoA-1 version of it, see Category:ApCoCoA-1: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 $\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 $\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);

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.