Difference between revisions of "Package sat/SAT.GetResult"

From ApCoCoAWiki
(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...")
 
m (category)
 
Line 37: Line 37:
 
     <key>SAT.GetResult</key>
 
     <key>SAT.GetResult</key>
 
     <key>GetResult</key>
 
     <key>GetResult</key>
     <wiki-category>ApCoCoA-1:Package_sat</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.ConvertToCNF

Package sat/SAT.ConvertToXOR

Package sat/SAT.LaunchCryptoMiniSat