Difference between revisions of "Package sat"

From ApCoCoAWiki
(Essentially copied from Category:ApCoCoA-1:Package sat)
m (added version info)
 
(3 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 +
{{Version|2|[[:Category:ApCoCoA-1:Package sat]]}}
 
This page is about the SAT package. For a function list see [[:Category: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.
 
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 <math>\mathbb{Z}/2\mathbb{Z}</mathbb> by first converting the system to CNF-SAT in DIMACS format and then using a SAT solver to solve the resulting conjunctive normal form.
+
This package allows to solve polynomial systems over <math>\mathbb{Z}/2\mathbb{Z}</math> 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 [https://philipp.jovanovic.io/paper/2010/satattack/satattack.pdf Algebraic Attacks Using SAT-Solvers] by Philipp Jovanovic, the author of this package, and Martin Kreuzer.
  
 
<em>Important</em>: 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.
 
<em>Important</em>: 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.
Line 12: Line 13:
 
CryptoMiniSat [https://www.msoos.org/cryptominisat5/],   
 
CryptoMiniSat [https://www.msoos.org/cryptominisat5/],   
 
DIMACS [http://dimacs.rutgers.edu/]
 
DIMACS [http://dimacs.rutgers.edu/]
 +
 +
== Usage ==
 +
Let <code>S</code> be a list of polynomials in a polynomial ring <code>P</code> over the field <math>\mathbb{Z}/2\mathbb{Z}</math>. Then we can use this package to find a common zero of the polynomials in <code>S</code>, i.e. a list <code>b = [b1,...,bn]</code> such that <code>[eval(f,b) | f in S] = [0,...,0]</code>. This can be achieved by either using the single function <code>[[/SAT.Solve/]]</code> or with the functions <code>[[/SAT.ConvertToCNF/]]</code>, <code>[[/SAT.LaunchCryptoMiniSat/]]</code> and <code>[[/SAT.GetResult/]]</code> together.
 +
 +
In the first case, the simple call
 +
<pre>
 +
SAT.Solve(S);
 +
</pre>
 +
already yields the desired result.
 +
 +
The second method works as follows. First, the call
 +
<pre>
 +
CNFPath := SAT.ConvertToCNF(S,CuttingLength,QStrategy,CStrategy);
 +
</pre>
 +
converts the polynomial system into standard CNF form and writes it in DIMACS format to a new file in the <code>/packages/temp/</code> 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 <code>CNFPath</code>. For more informations about <code>CuttingLength</code>, <code>QStrategy</code> and <code>CStrategy</code>, see [[Package sat/SAT.ConvertToCNF]] or the paper linked above. Afterwards, the function
 +
<pre>
 +
SolPath := SAT.LaunchCryptoMiniSat(CNFPath);
 +
</pre>
 +
launches CryptoMiniSat with the file in <code>CNFPath</code> 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 <code>SolPath</code>. Then, one can use the function
 +
<pre>
 +
SAT.GetResult(SolPath,P);
 +
</pre>
 +
that converts the result back into CoCoA and returns a solution <code>[b1,...,bn]</code> of the system <code>S</code> in form of a list with entries in <code>P</code>.
 +
  
 
[[Category:Package sat]]
 
[[Category:Package sat]]
 +
[[Category:ApCoCoA Packages]]

Latest revision as of 10:23, 2 November 2020

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:

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.