sweetpea.core.generate.tools.cryptominisat module

This module provides functionality for calling the third-party CryptoMiniSAT tool.

CryptoMiniSAT is a an advanced incremental SAT solver. SweetPea uses CryptoMiniSAT for a few processes, including solving some CNF formulas or checking whether a CNF formula is satisfiable to begin with.

sweetpea.core.generate.tools.cryptominisat.cryptominisat_solve(input_file, docker_mode=False)

Attempts to solve a CNF formula with CryptoMiniSAT and returns the result as a list of integers.

Returns an empty list if the result was unsatisfiable, and returns None if CryptoMiniSAT encounters some unknown issue.

Parameters

  • input_file (Path) –

  • docker_mode (bool) –

Return type

Optional[List[int]]

sweetpea.core.generate.tools.cryptominisat.cryptominisat_is_satisfiable(input_file, docker_mode=False)

Determines whether the CNF formula encoded in the input file is satisfiable, according to CryptoMiniSAT.

Returns None if CryptoMiniSAT encounters an unknown issue.

Parameters

  • input_file (Path) –

  • docker_mode (bool) –

Return type

Optional[bool]