Giải bài toán 2-SAT bằng thuật toán Tarjan thành phần liên thông mạnh

Mục tiêu kiến thức

• Biểu diễn biểu thức 2-CNF (x_i ∨ x_j) thành hai cung suy diễn: (neg x_i ⇒ x_j) và (neg x_j ⇒ x_i) trên Đồ thị suy diễn (Implication Graph).
• Sử dụng thuật toán Tarjan tìm các Thành phần liên thông mạnh (SCC) trong O(V + E).
• Kiểm tra điều kiện thỏa mãn: Hệ có nghiệm khi và chỉ khi với mọi biến x, x và neg x không cùng thuộc một SCC.
• Gán giá trị chân lý hợp lệ dựa trên thứ tự tô-pô ngược của các SCC.

Mô tả bài toán

Cho hệ ràng buộc gồm N biến mệnh đề x₁, x₂, …, x_N và M mệnh đề dạng (u ∨ v), trong đó u và v là các biến hoặc phủ định của biến:

• Số nguyên dương k đại diện cho biến x_k.
• Số nguyên âm -k đại diện cho phủ định neg x_k.

Hãy kiểm tra xem có tồn tại phép gán giá trị chân lý (true / false) cho tất cả N biến sao cho mọi mệnh đề đều nhận giá trị true hay không. Nếu có, in YES và một bộ giá trị chân lý cho các biến; nếu không, in NO.

Quy ước nộp bài

• Chỉ cần viết một chương trình đọc stdin và in ra stdout. Bài này không yêu cầu viết hàm.
• Không dùng cout để in lời nhắc trước khi đọc dữ liệu. Lời nhắc sẽ lọt vào stdout và làm bài sai.
• Chỉ in đúng nội dung ở mục Output. Không in thêm nhãn, dòng trống hay ký tự thừa.
• Output được so khớp từng ký tự, phân biệt chữ hoa/thường và dấu câu.

Ràng buộc

• 1 ≤ N, M ≤ 10⁵.
• Thời gian chạy: 1000ms.
• Bộ nhớ tối đa: 256MB.