Bài toán
Bài toán đánh giá, gọi tắt là SAT (Satisfiability), yêu cầu xác định sự tồn tại của một biểu thức logic. Một biểu thức bao gồm các biến logic (x_1,x_2,...,x_n), các phép toán logic (|-phép hội, &-phép tuyển, !-phép phủ định), và các dấu ngoặc. Một biểu thức được cho là thỏa mãn nếu đưa các giá trị logic hợp lí vào các biến và sau đó nó (biểu thức) trả lại giá trị TRUE. (Nguồn: Tin tuyển 2013).
2-SAT là bài toán với biểu thức có dạng:
S = (u_1|v_1) & (u_2|v_2) & ... & (u_m, v_m)
trong đó, u_i và v_i được thay bằng một biến x_j nào đó.
Yêu cầu của bài toán là xác định một nghiệm (x_1, x_2, ...,x_n) hoặc kết luận là vô nghiệm
Độ phức tạp
O(m+n)
Code này của Nguyễn Tiến Trung Kiên
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <stack>
#include <vector>
#include <iostream>
#include <algorithm>
using namespace std;
#define f1(i, n) for (int i = 1; i <= n; i++)
#define SetLength2(a, n, t) a = ((t *)calloc(n, sizeof(t))) + (n) / 2
int n, m, cnt;
vector<int> *a; //
int *Color, *Num, *Low; // Color 1=False, 2=True
stack<int> st;
bool Invalid = false;
bool minimize(int &a, int b) {
if (a > b)
a = b;
else
return false;
return true;
}
void init(int m, int n) {
SetLength2(a, n * 2 + 5, vector<int>);
SetLength2(Color, n * 2 + 5, int);
SetLength2(Num, n * 2 + 5, int);
SetLength2(Low, n * 2 + 5, int);
}
void set_color(int u, int x) {
if (Color[u] == (x ^ 3))
Invalid = true;
else
Color[u] = x;
if (Color[-u] == x)
Invalid = true;
else
Color[-u] = (x ^ 3);
}
void tarzan(int u) {
Num[u] = Low[u] = ++cnt;
st.push(u);
for (int i = 0, v; i < a[u].size(); i++) {
v = a[u][i];
if (Num[v])
minimize(Low[u], Num[v]);
else
tarzan(v), minimize(Low[u], Low[v]);
if (Color[v] == 1)
set_color(u, 1); // False
}
if (Low[u] == Num[u]) {
int v = 0;
if (Color[u] == 0)
set_color(u, 2); // True
do {
v = st.top();
st.pop();
set_color(v, Color[u]);
Num[v] = Low[v] = 0x33334444;
} while (u != v);
}
}
void enter() {
//srand((m+n)*1000);
for (int i = 1; i <= m; i++) {
int p, q;
cin >> p >> q;
//p=(rand()%n+1) * (rand()&1 ? 1 : -1);
//q=(rand()%n+1) * (rand()&1 ? 1 : -1);
a[-p].push_back(q);
a[-q].push_back(p);
}
}
int main() {
ios ::sync_with_stdio(false);
cin >> m >> n;
init(m, n);
enter();
for (int i = 1; i <= n; i++) if (!Num[i]) tarzan(i);
for (int i = 1; i <= n; i++) if (!Num[-i]) tarzan(-i);
if (Invalid)
cout << "NO" << endl;
else {
cout << "YES" << endl;
int Answer = 0;
for (int i = 1; i <= n; i++) if (Color[i] == 2) Answer++;
cout << Answer << endl;
for (int i = 1; i <= n; i++) if (Color[i] == 2) cout << i << " ";
cout << endl;
}
cin.ignore(2);
}
Mô tả
int Color[]
Color[x] là giá trị của đỉnh x (Color[x] thuộc 0..2, 0 tức là chưa biết giá trị, 1 là False, 2 là True).
bool Invalid
bằng True nếu vô nghiệm, False nếu ngược lại.
Tính chất
Color[x] != Color[-x], phương trình vô nghiệm khi gặp bất cứ x mà Color[x]=Color[-x].
Nếu Color[x]=True và Color[v]=False thì phương trình cũng vô nghiệm (kiểm tra trong hàm set_color)
Trên cung (u,v), u=True thì v=True.
Mệnh đề x | y tương đương với việc có cung (-x,y) và có cung (-y,x)
TPLTM S gồm các đỉnh u1, u2, ... thì Color[u1]=Color[u2]=...=Color[S].
Nhận xét
Code này đã được dùng để nộp cho một bài trên SPOJ.
Thuật toán được tiến hành như sau: trong quá trình tarzan các đỉnh, hễ lúc nào phát hiện được một thành phần liên thông mạnh S gồm các đỉnh u1, u2, ... thì kiểm tra, nếu từ S có cung tới một đỉnh v và v=False thì Color[S]=False, ngược lại thì cho Color[S]=True.
Cảm ơn anh Trần Anh Tuấn đã giúp em hoàn thành bài viết này.
Tham khảo
vn.spoj.com/problems/TWOSAT