| 6 | SAT() : n(0) { } |
| 7 | int var() { return ++n; } |
| 8 | void clause(vi vars) { |
| 9 | set<int> seen; iter(it,vars) { |
| 10 | if (seen.find(IDX(*it)^1) != seen.end()) return; |
| 11 | seen.insert(IDX(*it)); } |
| 12 | head.push_back(cl.size()); |
| 13 | iter(it,seen) cl.push_back(*it); |
| 14 | tail.push_back((int)cl.size() - 2); } |
| 15 | bool assume(int x) { |
| 16 | if (val[x^1]) return false; |
| 17 | if (val[x]) return true; |