Difference between revisions of "Category:ApCoCoA-1:Package sat"
From ApCoCoAWiki
(New page: 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...) |
Andraschko (talk | contribs) m (added version info) |
||
| (8 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 | + | <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 about | + | 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: | + | [[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:
Pages in category "ApCoCoA-1:Package sat"
The following 6 pages are in this category, out of 6 total.
