Mạng Phép Toán · canuc80k7703 · Thuật toán Canuc80k

Có $N$ biến Boolean $X_{0}, X_{1}, \dots, X_{N - 1}$ . Mỗi ràng buộc chọn hai biến, một phép toán trong $AND, OR, XOR$ và một bit kết quả $c$ ; ràng buộc được thỏa khi $X_{a} o p X_{b} = c$ . Hãy quyết định liệu có phép gán thỏa tất cả ràng buộc hay không.

Input

Dòng đầu chứa hai số nguyên $N$ và $M$ .
Mỗi trong $M$ dòng tiếp theo chứa $a$ $b$ $c$ $o p$ , mô tả phương trình Boolean $X_{a} o p X_{b} = c$ .

Output

In YES nếu tồn tại phép gán thỏa mọi ràng buộc; ngược lại in NO.

Constraints

$1 \leq N \leq 1000.$
$0 \leq M \leq 1 0^{6} .$
$0 \leq a, b < N$ ; $c \in {0, 1}$ ; $o p$ là $AND, OR$ hoặc $XOR$ .

Scoring

Subtask $1$ ( $50%$ số điểm): $N \leq 20$ và $M \leq 60$ .
Subtask $2$ ( $50%$ số điểm): Không có giới hạn bổ sung.

Example

Test 1

Input

3 3
0 1 1 XOR
1 2 1 AND
0 2 1 OR

Output

YES

Giải thích: Ràng buộc AND ép $X_{1} = X_{2} = 1$ ; khi đó XOR ép $X_{0} = 0$ , và ràng buộc OR vẫn cho kết quả $1$ .

Test 2

Input

1 2
0 0 0 OR
0 0 1 AND

Output

NO

Giải thích: Ràng buộc đầu ép $X_{0} = 0$ , còn ràng buộc sau ép $X_{0} = 1$ , nên hệ vô nghiệm.

Phân tích: Mỗi đối tượng có đúng hai trạng thái, vì vậy ta tạo một biến Boolean cho nó. Sáu trường hợp AND/OR/XOR với kết quả 0/1 được viết thành unit clause hoặc hai clause tương đương.
Phân tích: Với một clause (A OR B), nếu A sai thì B buộc phải đúng, và ngược lại. Ta thêm hai cung kéo theo NOT A -> B và NOT B -> A.
Thuật toán: 1. Tạo hai đỉnh cho mỗi biến, tương ứng với hai literal đối nhau. 2. Chuyển từng ràng buộc của đề thành các clause hai literal rồi thêm các cung kéo theo. 3. Tìm các thành phần liên thông mạnh của đồ thị. 4. Nếu một literal và phủ định của nó nằm cùng thành phần, công thức vô nghiệm. Ngược lại, dùng thứ tự các thành phần để lấy phép gán. 5. Bài chỉ hỏi khả thi, nên sau khi kiểm tra SCC chỉ cần in YES hoặc NO.
Chứng minh đúng: Mỗi phép biến đổi ràng buộc ở bước 2 là một tương đương logic, nên phép gán thỏa công thức 2-CNF khi và chỉ khi nó thỏa đề bài. Trong đồ thị kéo theo, nếu một literal và phủ định của nó cùng thành phần liên thông mạnh thì chúng kéo theo lẫn nhau, không thể gán nhất quán. Khi mọi cặp đối nhau thuộc hai thành phần khác nhau, thứ tự tô SCC tạo một phép gán thỏa mọi cung kéo theo, do đó thỏa mọi clause và mọi ràng buộc gốc. Vì vậy thuật toán báo vô nghiệm chính xác và mọi cấu hình được in đều hợp lệ.
Độ phức tạp: Thời gian O(V+E) và bộ nhớ O(V+E), trong đó V là số literal và E là số cung kéo theo; với bài này đều tuyến tính theo kích thước input.