Difference between revisions of "Package sat/SAT.GetResult"
From ApCoCoAWiki
Andraschko (talk | contribs) (Created page with "{{Version|2|ApCoCoA-1:SAT.GetResult}} <command> <title>SAT.GetResult</title> <short_description>Looks up the configuration of the indeterminates in a file by a SAT...") |
Andraschko (talk | contribs) m (category) |
||
| Line 37: | Line 37: | ||
<key>SAT.GetResult</key> | <key>SAT.GetResult</key> | ||
<key>GetResult</key> | <key>GetResult</key> | ||
| − | <wiki-category> | + | <wiki-category>Package_sat</wiki-category> |
</command> | </command> | ||
Latest revision as of 10:29, 2 November 2020
| This article is about a function from ApCoCoA-2. If you are looking for the ApCoCoA-1 version of it, see ApCoCoA-1:SAT.GetResult. |
SAT.GetResult
Looks up the configuration of the indeterminates in a file by a SAT-Solver.
Syntax
SAT.GetResult(File: STRING, P: RING): LIST
Description
@param: The file containing the output of the SAT solver CryptoMiniSat.
@return: A solution of a polynomial system of equations as a list of values in the ring P
Example
Use S ::= ZZ/(2)[x[1..3]]; F1 := x[1]*x[2] + x[1]*x[3] + x[2]*x[3] + x[3]; F2 := x[2] + 1; F3 := x[1]*x[2] + x[3]; SPE := [F1,F2,F3]; CNFPath := SAT.ConvertToCNF(SPE,4,0,0); SolPath := SAT.LaunchCryptoMiniSat(CNFPath); SAT.GetResult(SolPath,S); --Result: [0,1,0] Test with: Eval(SPE,[0,1,0]);
See also
Package sat/SAT.LaunchCryptoMiniSat
