Package sat/SAT.LaunchCryptoMiniSat

From ApCoCoAWiki
This article is about a function from ApCoCoA-2. If you are looking for the ApCoCoA-1 version of it, see ApCoCoA-1:SAT.LaunchCryptoMiniSat.


Launches CryptoMiniSat on a given input file. The result is written to a new file.


SAT.LaunchCryptoMiniSat(File: STRING): STRING


Make sure that the CryptoMiniSat executable is called "cryptominisat" and located in ApCoCoA-directory/sat/bin.

  • @param File: The (absolute) path of the input file

  • @return The path of the file where the solution was written to.


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);
--Result: [0,1,0] Test with: Eval(SPE,[0,1,0]);

See also

Package sat/SAT.GetResult

Package sat/SAT.ConvertToCNF

Package sat/SAT.ConvertToXOR