Các lượt nộp
    Danh sách bài
    Trang chủ
    Báo lỗi

    solution

    Đề bài: [Giải thuật] Kiểm tra 2-SAT thoả được

    Cho công thức logic dạng 2-CNF với nnn biến boolean (đánh số 111 đến nnn) và mmm mệnh đề. Mỗi mệnh đề có dạng (ℓa∨ℓb)(\ell_a \lor \ell_b)(ℓa​∨ℓb​) trong đó mỗi literal là một biến hoặc phủ định của nó. Ta ký hiệu literal bằng số nguyên khác 000: số dương xxx là biến xxx, số âm −x-x−x là phủ định biến xxx.

    Hãy xác định công thức có thoả được hay không (tồn tại phép gán giá trị đúng/sai cho các biến làm mọi mệnh đề đúng).

    Ví dụ: Hai mệnh đề (x1∨x2)(x_1 \lor x_2)(x1​∨x2​) và (¬x1∨x2)(\lnot x_1 \lor x_2)(¬x1​∨x2​) thoả được bằng cách đặt x2x_2x2​ = đúng.

    • Định dạng đầu vào:

      Dòng đầu chứa nnn và mmm. mmm dòng tiếp theo, mỗi dòng hai số nguyên khác 000 biểu diễn hai literal của một mệnh đề.

    • Ràng buộc đầu vào:

      1≤n≤1051 \le n \le 10^51≤n≤105, 0≤m≤2⋅1050 \le m \le 2\cdot10^50≤m≤2⋅105. Mỗi literal có trị tuyệt đối trong [1,n][1, n][1,n].

    • Định dạng đầu ra:

      In ra SATISFIABLE nếu thoả được, ngược lại in UNSATISFIABLE.

    Ví dụ:

    Đầu vào:

    2 2
1 2
-1 2

    Đầu ra:

    SATISFIABLE

    Giải thích:

    Hai mệnh đề (x1 OR x2) và (NOT x1 OR x2). Đặt x2 = đúng làm cả hai mệnh đề đúng, do đó công thức thoả được.

    Đang tải editor...