Template Class BasicCdcl

• Defined in File SatSolvers.h

Class Documentation

template<class Heap = std::priority_queue<std::pair<double, int>>>
class BasicCdcl

conflict-driven clause learning with two watched literals; the free variables by activity in a Heap of pairs ( activity , variable ), the largest on top: std::priority_queue by default, or a heap of Boost or of ADS [see DaryHeap.h], with the same decisions and conflicts, since the pairs are ordered totally

Public Types

enum class Result

Values:

enumerator SAT

enumerator UNSAT

enumerator UNKNOWN

Public Functions

BasicCdcl(const Cnf &F, int n)

Pre:

n >= 0 and the literals of F are variables of [ 0 , n )

Result solve(long maxConflicts = -1)

the search, UNKNOWN after maxConflicts conflicts if that is >= 0

Post:

SAT means that model() passes satCertificate()

const std::vector<bool> &model(void) const

the model found by solve()

inline long conflicts(void) const

inline long decisions(void) const