#include <hmcsat.h>
Inheritance diagram for HMCSAT:
Public Member Functions | |
HMCSAT (HVariableState *state, long int seed, const bool &trackClauseTrueCnts, MCSatParams *mcsatParams) | |
Constructor: Constructs unit propagation and SampleSat. | |
~HMCSAT () | |
Destructor: Instances of unit propagation and MaxWalksat are deleted. | |
void | initNumTrueTotal () |
void | init () |
Initializes MC-SAT with MaxWalksat on hard clauses. | |
void | printContSamples () |
void | infer () |
Performs MC-SAT inference. | |
void | SetContSampleFile (const char *contsamplelog) |
void | SetPrintVarsPerSample (bool pps) |
Public Attributes | |
bool | bMaxWalkSat_ |
It wraps a procedure around SampleSat, thus enabling it to sample_ nearly uniform.
Definition at line 83 of file hmcsat.h.