Function ADS::dominoToSat

• Defined in File Reductions.h

Function Documentation

inline Cnf ADS::dominoToSat(const std::vector<Tile> &D, int n)

DOMINO LIMITATO to SODDISFATTIBILITA’, on the m n^2 variables of tileVar()

Pre:

n >= 1 and D is not empty

Post:

the literals are variables of [ 0 , m n^2 )