TwoSat

1 // Solve (x0 v x1) ^ (~x0 v x2) ^ (~x1 v ~x2)
2 auto sat = TwoSat(3);
3 sat.addClause(0, true,  1, true);  // (vars[0] == true  || vars[1] == true)
4 sat.addClause(0, false, 2, true);  // (vars[0] == false || vars[2] == true)
5 sat.addClause(1, false, 2, false); // (vars[1] == false || vars[2] == false)
6 assert(sat.solve() == true);
7 auto vars = sat.vars;
8 assert(vars[0] == true  || vars[1] == true);
9 assert(vars[0] == false || vars[2] == true);
10 assert(vars[1] == false || vars[2] == false);