Function ADS::dpll

• Defined in File SatSolvers.h

Function Documentation

inline std::optional<std::vector<bool>> ADS::dpll(const Cnf &F, int n)

a model of F by DPLL, or nothing if F is unsatisfiable

Pre:

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

Post:

a model returned passes satCertificate()