Difference between revisions of "Category:ApCoCoA-1:Package sat"

From ApCoCoAWiki
m (added version info)
 
(7 intermediate revisions by 4 users not shown)
Line 1: Line 1:
 +
{{Version|1|[[Package sat]]}}
 
The basic idea behind this package is to make SAT-Solver, like (Crypto-)MiniSat, usable in/with ApCoCoA.
 
The basic idea behind this package is to make SAT-Solver, like (Crypto-)MiniSat, usable in/with ApCoCoA.
  
This package allows to solve polynomial systems over GF(2) 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 GF(2) by first converting the system to CNF-SAT in DIMACS format and then using a SAT-Solver to solve the resulting conjunctive normal form.
  
 
{{ApCoCoAServer}}
 
{{ApCoCoAServer}}
  
<em>Important</em>: The MiniSat executable must be in the ApCoCoA directory/sat/bin and you must have the permissions to read and write in this directory.
+
<em>Important</em>: The MiniSat executable must be in ApCoCoA_directory/sat/bin and you must have the permissions to read and write in this directory.
  
For further informations see the following links:  
+
For further informations about SAT-Solver and the DIMACS format see the following links:
MiniSat [http://www.minisat.se]
 
  
CryptoMiniSat [http://planete.inrialpes.fr/~soos/CryptoMiniSat/index.html]
+
MiniSat [http://www.minisat.se], 
 +
CryptoMiniSat [https://www.msoos.org/cryptominisat5/], 
 +
DIMACS [http://dimacs.rutgers.edu/]
  
[[Category:ApCoCoA_Manual]]
+
[[Category:ApCoCoA-1 Manual]]

Latest revision as of 10:22, 2 November 2020

This article is about a function from ApCoCoA-1. If you are looking for the ApCoCoA-2 version of it, see Package sat.

The basic idea behind this package is to make SAT-Solver, like (Crypto-)MiniSat, usable in/with ApCoCoA.

This package allows to solve polynomial systems over GF(2) by first converting the system to CNF-SAT in DIMACS format and then using a SAT-Solver to solve the resulting conjunctive normal form.

Please note: The function(s) explained on this page is/are using the ApCoCoAServer. You will have to start the ApCoCoAServer in order to use it/them.

Important: The MiniSat executable must be in ApCoCoA_directory/sat/bin and you must have the permissions to read and write in this directory.

For further informations about SAT-Solver and the DIMACS format see the following links:

MiniSat [1], CryptoMiniSat [2], DIMACS [3]

Pages in category "ApCoCoA-1:Package sat"

The following 6 pages are in this category, out of 6 total.