#include <mcsat.h>
Inheritance diagram for MCSAT:
Public Member Functions | |
MCSAT (VariableState *state, long int seed, const bool &trackClauseTrueCnts, MCSatParams *mcsatParams) | |
Constructor: Constructs unit propagation and SampleSat. | |
~MCSAT () | |
Destructor: Instances of unit propagation and MaxWalksat are deleted. | |
void | init () |
Initializes MC-SAT with MaxWalksat on hard clauses. | |
void | infer () |
Performs MC-SAT inference. |
It wraps a procedure around SampleSat, thus enabling it to sample nearly uniform.
Definition at line 82 of file mcsat.h.