Difference between revisions of "Package sat"
From ApCoCoAWiki
Andraschko (talk | contribs) (Created page with "This page is about the SAT package. For a function list see Category:Package sat. Category:Package sat") |
Andraschko (talk | contribs) (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: