Difference between revisions of "Package sat"

From ApCoCoAWiki
(Created page with "This page is about the SAT package. For a function list see Category:Package sat. Category:Package sat")
 
(Essentially copied from Category:ApCoCoA-1:Package sat)
Line 1: Line 1:
 
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.
 +
 +
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.
 +
 +
<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.
 +
 +
For further informations about SAT-Solver and the DIMACS format see the following links:
 +
 +
MiniSat [http://www.minisat.se], 
 +
CryptoMiniSat [https://www.msoos.org/cryptominisat5/], 
 +
DIMACS [http://dimacs.rutgers.edu/]
  
 
[[Category:Package sat]]
 
[[Category:Package sat]]

Revision as of 14:00, 31 October 2020

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 <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.

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]