View source for Package sat/SAT.LaunchCryptoMiniSat

{{Version|2|[[ApCoCoA-1:SAT.LaunchCryptoMiniSat]]}}
<command>
    <title>SAT.LaunchCryptoMiniSat</title>
    <short_description>Launches CryptoMiniSat on a given input file. The result is written to a new file.</short_description>
<syntax>
SAT.LaunchCryptoMiniSat(File: STRING): STRING
</syntax>
<description>
Make sure that the CryptoMiniSat executable is called "cryptominisat" and located in ApCoCoA-directory/sat/bin.
<itemize>
<item>@param <em>File</em>: The (absolute) path of the input file</item>
<item>@return The path of the file where the solution was written to.</item>
</itemize>
<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]);
</example>
</description>

<seealso>
  <see>Package sat/SAT.GetResult</see>
  <see>Package sat/SAT.ConvertToCNF</see>
  <see>Package sat/SAT.ConvertToXOR</see>
</seealso>

<types>
 <type>polynomial</type>
 <type>poly_system</type>
</types>

    <key>SAT.LaunchCryptoMiniSat</key>
    <key>LaunchCryptoMiniSat</key>
    <wiki-category>Package_sat</wiki-category>
</command>