2-SAT
It solves 2-SAT.
For variables $x_0, x_1, \cdots, x_{N - 1}$ and clauses with form
- $(x_i = f) \lor (x_j = g)$,
it decides whether there is a truth assignment that satisfies all clauses.
Constructor
two_sat ts(int n)
It creates a 2-SAT of $n$ variables and $0$ clauses.
Constraints
Complexity
add_clause
void ts.add_clause(int i, bool f, int j, bool g)
It adds a clause $(x_i = f) \lor (x_j = g)$.
Constraints
- $0 \leq i \lt n$
- $0 \leq j \lt n$
Complexity
satisfiable
bool ts.satisfiable()
If there is a truth assignment that satisfies all clauses, it returns true. Otherwise, it returns false.
Constraints
- You may call it multiple times.
Complexity
- $O(n + m)$, where $m$ is the number of added clauses.
answer
vector<bool> ts.answer()
It returns a truth assignment that satisfies all clauses of the last call of satisfiable.
If we call it before calling satisfiable or when the last call of satisfiable returns false, it returns the vector of length $n$ with undefined elements.
Complexity
Examples
#include <atcoder/twosat>
#include <iostream>
#include <vector>
using namespace std;
using namespace atcoder;
int main() {
int n, d;
cin >> n >> d;
vector<int> x(n), y(n);
for (int i = 0; i < n; i++) {
cin >> x[i] >> y[i];
}
// ts[i] = (i-th flag is located on x[i])
two_sat ts(n);
for (int i = 0; i < n; i++) {
for (int j = i + 1; j < n; j++) {
if (abs(x[i] - x[j]) < d) {
// cannot use both of x[i] and x[j]
ts.add_clause(i, false, j, false);
}
if (abs(x[i] - y[j]) < d) {
ts.add_clause(i, false, j, true);
}
if (abs(y[i] - x[j]) < d) {
ts.add_clause(i, true, j, false);
}
if (abs(y[i] - y[j]) < d) {
ts.add_clause(i, true, j, true);
}
}
}
if (!ts.satisfiable()) {
cout << "No" << endl;
return 0;
}
cout << "Yes" << endl;
auto answer = ts.answer();
for (int i = 0; i < n; i++) {
if (answer[i])
cout << x[i] << endl;
else
cout << y[i] << endl;
}
return 0;
}