Function ADS::twoSat

• Defined in File EasyCases.h

Function Documentation

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

an assignment of the n variables that satisfies F, each clause of one or two literals, or nothing

Pre:

n >= 0, each clause has one or two literals of [ 0 , n )

Post:

an assignment returned passes satCertificate()