Function ADS::satisfiable

• Defined in File Problems.h

Function Documentation

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

an assignment of the n variables that satisfies F, by backtrack with a clause checked as soon as its variables are set, or nothing

Pre:

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

Post:

an assignment returned passes satCertificate()