|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 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:
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
In the first case, the simple call
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
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
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