|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*x + x*x + x*x + x; F2 := x + 1; F3 := x*x + x; 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]);