Bài toán SAT hỏi: cho một công thức logic mệnh đề, có cách gán đúng/sai cho các biến để cả công thức đúng hay không. Kiểm một cách gán thì rất nhanh, nhưng tìm ra cách gán có thể phải thử tới 2ⁿ khả năng với n biến, và tới nay chưa ai biết thuật toán nào luôn nhanh hơn hẳn điều đó. Năm 1971 Stephen Cook chứng minh SAT là bài toán NP-đầy đủ — mọi bài toán "dễ kiểm, khó tìm" kiểu này đều quy được về SAT — nên SAT trở thành bài toán mẫu của cả một lớp bài toán khó.
Từ một câu chuyện thường ngày tới công thức
Lớp tổ chức đi dã ngoại, cô giáo cần chọn người đi trong ba bạn An, Bình, Chi với bốn điều kiện:
- An hoặc Bình phải đi (ít nhất một người).
- Nếu An đi thì Chi đi cùng.
- Bình và Chi không đi cùng nhau (hai bạn cùng trực nhật một buổi).
- Nếu Chi đi thì An cũng đi.
Đặt biến: x = "An đi", y = "Bình đi", z = "Chi đi". Ký hiệu: ∨ là "hoặc" (bao hàm), ∧ là "và", ¬ là "không". Câu "nếu p thì q" tương đương "¬p ∨ q" (chỉ sai khi p đúng mà q sai). Viết lại bốn điều kiện:
- (x ∨ y)
- (¬x ∨ z) — "nếu An đi thì Chi đi"
- (¬y ∨ ¬z) — "không phải cả Bình lẫn Chi"
- (x ∨ ¬z) — "nếu Chi đi thì An đi"
Công thức cần thoả: F = (x ∨ y) ∧ (¬x ∨ z) ∧ (¬y ∨ ¬z) ∧ (x ∨ ¬z).
Đây là dạng chuẩn mà mọi phần mềm giải SAT dùng: dạng chuẩn hội (CNF) — một chuỗi "và" của các mệnh đề, mỗi mệnh đề là một chuỗi "hoặc" của các biến hoặc phủ định của biến (gọi là literal). Muốn F đúng thì mỗi mệnh đề phải có ít nhất một literal đúng.
Hai cách giải: thử hết và suy luận
Thử hết: bảng 8 dòng
Ba biến cho 2³ = 8 cách gán (1 = đi, 0 = không đi):
| x y z | x ∨ y | ¬x ∨ z | ¬y ∨ ¬z | x ∨ ¬z | F |
|---|---|---|---|---|---|
| 0 0 0 | 0 | 1 | 1 | 1 | 0 |
| 0 0 1 | 0 | 1 | 1 | 0 | 0 |
| 0 1 0 | 1 | 1 | 1 | 1 | 1 |
| 0 1 1 | 1 | 1 | 0 | 0 | 0 |
| 1 0 0 | 1 | 0 | 1 | 1 | 0 |
| 1 0 1 | 1 | 1 | 1 | 1 | 1 |
| 1 1 0 | 1 | 0 | 1 | 1 | 0 |
| 1 1 1 | 1 | 1 | 0 | 1 | 0 |
F thoả được, và có đúng hai nghiệm: chỉ Bình đi (0 1 0), hoặc An và Chi cùng đi (1 0 1).
Suy luận: giả sử rồi lan truyền
Thử hết thì chắc, nhưng không làm nổi khi có hàng trăm biến. Các phần mềm giải SAT làm giống người giải câu đố: giả sử một biến, rồi lan truyền hệ quả bắt buộc.
Nhánh x = 1 (An đi):
- Mệnh đề 1 và 4 đã đúng nhờ x.
- Mệnh đề 2 còn (¬x ∨ z) mà ¬x = 0, nên buộc z = 1.
- Mệnh đề 3 còn (¬y ∨ ¬z) mà ¬z = 0, nên buộc y = 0.
- Được x = 1, y = 0, z = 1, không mâu thuẫn. Có nghiệm.
Nhánh x = 0 (An không đi):
- Mệnh đề 1 buộc y = 1.
- Mệnh đề 4 buộc ¬z = 1, tức z = 0.
- Mệnh đề 2 đúng nhờ ¬x; mệnh đề 3: ¬z = 1 nên đúng. Có nghiệm x = 0, y = 1, z = 0.
Mệnh đề chỉ còn đúng một literal chưa gán gọi là mệnh đề đơn vị; ép literal đó đúng gọi là lan truyền đơn vị. Đây là động tác cơ bản nhất trong mọi bộ giải SAT.
Khi không có nghiệm: chứng minh không thoả được
Cô giáo thêm hai điều kiện: "An hoặc Chi phải đi" (x ∨ z) và "nếu An đi thì Bình đi" (¬x ∨ y). Công thức mới F₂ có sáu mệnh đề. Làm lại hai nhánh:
- x = 1: mệnh đề (¬x ∨ z) buộc z = 1; mệnh đề (¬x ∨ y) buộc y = 1; nhưng (¬y ∨ ¬z) cần ít nhất một trong y, z bằng 0. Mâu thuẫn.
- x = 0: (x ∨ y) buộc y = 1; (x ∨ z) buộc z = 1; lại vấp (¬y ∨ ¬z). Mâu thuẫn.
Cả hai nhánh đều đổ vỡ, nên F₂ không thoả được: không cách chọn nào đáp ứng đủ sáu điều kiện. Có thể đối chiếu bảng 8 dòng ở trên: hai nghiệm cũ là 0 1 0 (vi phạm x ∨ z) và 1 0 1 (vi phạm ¬x ∨ y).
Chú ý sự bất đối xứng: để nói "có nghiệm", chỉ cần đưa ra một cách gán, ai cũng kiểm lại được trong chốc lát. Để nói "không có nghiệm", phải chứng minh mọi nhánh đều đổ vỡ.
Vì sao SAT khó: sức nặng của 2ⁿ
Giả sử một máy kiểm được một tỉ (10⁹) cách gán mỗi giây:
| Số biến n | Số cách gán 2ⁿ | Thời gian thử hết |
|---|---|---|
| 10 | 1.024 | khoảng 1 phần triệu giây |
| 30 | khoảng 1,07 tỉ | khoảng 1 giây |
| 60 | khoảng 1,15 × 10¹⁸ | khoảng 36 năm |
| 100 | khoảng 1,27 × 10³⁰ | khoảng 4 × 10¹³ năm, gấp vài nghìn lần tuổi vũ trụ |
Mỗi biến thêm vào làm số khả năng gấp đôi. Câu hỏi lớn là: có thuật toán nào luôn tránh được cảnh thử hết, chạy trong thời gian chỉ tăng theo luỹ thừa của n (n², n³…) chứ không theo 2ⁿ? Chưa ai biết.
Định lý Cook – Levin
Năm 1971, Stephen Cook chứng minh rằng mọi bài toán thuộc lớp NP — lớp bài toán mà lời giải, nếu có, kiểm được nhanh — đều có thể "dịch" thành một công thức SAT trong thời gian đa thức. Leonid Levin ở Liên Xô đạt kết quả tương tự một cách độc lập. Năm 1972, Richard Karp chỉ ra thêm 21 bài toán quen thuộc (tô màu đồ thị, bài toán cái túi, tìm chu trình Hamilton…) cũng khó ngang SAT. Hệ quả: ai tìm ra thuật toán nhanh cho SAT là giải được tất cả, và trả lời được câu hỏi P có bằng NP không — một trong các bài toán thiên niên kỷ có giải thưởng một triệu đô-la của Viện Toán Clay. Chuyện P và NP nói chung là một đề tài riêng; ở đây chỉ cần nhớ SAT là "bài toán đại diện".
Không phải SAT nào cũng khó
- 2-SAT (mỗi mệnh đề tối đa 2 literal, như ví dụ dã ngoại) giải được nhanh, thời gian tỉ lệ với độ dài công thức.
- 3-SAT (mỗi mệnh đề 3 literal) đã NP-đầy đủ.
- Công thức gồm toàn mệnh đề có tối đa một literal không phủ định (mệnh đề Horn) cũng giải nhanh — đây là nền của ngôn ngữ Prolog.
Bộ giải SAT ngoài đời: khó trên lý thuyết, giải được trong thực tế
Điều bất ngờ: dù SAT khó trong trường hợp xấu nhất, các bộ giải hiện đại xử lý được nhiều công thức thực tế có hàng triệu biến. Dòng phát triển chính:
| Năm | Mốc |
|---|---|
| 1960 | Martin Davis và Hilary Putnam đề xuất một thủ tục kiểm thoả được dựa trên phép giải (resolution). |
| 1962 | Davis, Logemann và Loveland đưa ra thuật toán DPLL: lan truyền đơn vị + rẽ nhánh + quay lui — đúng cách giải tay ở trên. |
| 1971 | Stephen Cook chứng minh SAT là NP-đầy đủ. |
| Cuối thập niên 1990 – đầu 2000 | Kỹ thuật "học mệnh đề từ xung đột" (CDCL): mỗi lần vấp mâu thuẫn, bộ giải rút ra một mệnh đề mới ghi lại nguyên nhân, để không bao giờ vấp lại cùng chỗ đó. |
Ứng dụng: kiểm hai mạch có tương đương không
Muốn biết mạch A (f = x·y + x·z) và mạch B (g = x·(y + z)) có làm cùng một việc, kỹ sư dựng công thức "f khác g", tức f ⊕ g = 1, rồi đưa cho bộ giải SAT. Nếu bộ giải tìm được cách gán, đó chính là đầu vào khiến hai mạch cho kết quả khác nhau — một lỗi cụ thể. Nếu bộ giải chứng minh không thoả được, hai mạch tương đương trên mọi đầu vào. Ở đây f = g theo luật phân phối nên công thức không thoả được. Cách làm này là xương sống của kiểm chứng thiết kế chip.
Ứng dụng: xếp lịch thi
Ba môn Toán, Lý, Hoá phải xếp vào hai buổi sáng/chiều. Có học sinh thi cả Toán lẫn Lý, cả Lý lẫn Hoá, cả Toán lẫn Hoá, nên mỗi cặp phải khác buổi. Đặt t, l, h = "thi buổi sáng". "Toán và Lý khác buổi" viết thành (t ∨ l) ∧ (¬t ∨ ¬l). Ba cặp cho sáu mệnh đề 2-literal. Suy luận: t khác l, l khác h, nên t cùng giá trị với h — nhưng t phải khác h. Không thoả được: ba môn đôi một xung đột thì không xếp nổi vào hai buổi (đúng tinh thần nguyên lý Dirichlet). Thêm buổi thứ ba là hết vướng.
Các bộ giải SAT còn được dùng trong xếp ca, kiểm cấu hình, tìm phiên bản tương thích trong một số trình quản lý gói phần mềm, và giải các câu đố điền số.
Bài tập
- Công thức (x) ∧ (¬x ∨ y) ∧ (¬y) có thoả được không? — Đáp án: không; x = 1 bắt buộc, kéo theo y = 1, mâu thuẫn với ¬y.
- Viết "nếu trời mưa thì mang ô" (m, o) thành một mệnh đề CNF. — Đáp án: (¬m ∨ o).
- Công thức (x ∨ y) ∧ (¬x ∨ y) ∧ (x ∨ ¬y) có bao nhiêu nghiệm? — Đáp án: một nghiệm, x = 1, y = 1 (thử bốn cách gán: 00 vi phạm mệnh đề 1, 01 vi phạm mệnh đề 3, 10 vi phạm mệnh đề 2).
- Thêm một biến vào công thức thì số cách gán tăng thế nào? — Đáp án: gấp đôi.
- Vì sao "có nghiệm" dễ chứng minh hơn "không có nghiệm"? — Đáp án: có nghiệm thì chỉ cần đưa một cách gán để người khác kiểm; không có nghiệm thì phải loại hết mọi khả năng.
Dùng vào đâu
- Sinh viên công nghệ thông tin: SAT là cửa vào môn Độ phức tạp tính toán và Trí tuệ nhân tạo (bài toán thoả ràng buộc).
- Lập trình viên: có sẵn các bộ giải SAT, SMT mã nguồn mở; nhiều bài toán xếp lịch, phân công diễn đạt thành mệnh đề rồi giao cho bộ giải thì gọn hơn tự viết thuật toán tìm kiếm.
- Học sinh thích câu đố: cách giải "giả sử – lan truyền – mâu thuẫn – quay lui" chính là cách giải câu đố ai nói thật ai nói dối, chỉ là được làm bằng máy.
Câu hỏi thường gặp
Bài toán SAT là gì?
SAT (bài toán thoả được) hỏi: với một công thức logic mệnh đề, có tồn tại cách gán đúng/sai cho các biến để công thức đúng không. Nếu có, công thức gọi là thoả được; nếu không, gọi là không thoả được.
Vì sao SAT là bài toán NP-đầy đủ?
Năm 1971 Stephen Cook chứng minh mọi bài toán trong lớp NP đều quy được về SAT trong thời gian đa thức, và bản thân SAT thuộc NP vì một nghiệm kiểm được nhanh. Leonid Levin đạt kết quả tương tự độc lập. Do đó SAT khó ít nhất bằng mọi bài toán trong NP.
Dạng chuẩn hội CNF là gì?
Là công thức viết thành chuỗi "và" của các mệnh đề, mỗi mệnh đề là chuỗi "hoặc" của các biến hoặc phủ định của biến. Ví dụ (x ∨ y) ∧ (¬x ∨ z). Các bộ giải SAT đều nhận đầu vào ở dạng này.
2-SAT và 3-SAT khác nhau thế nào?
Trong 2-SAT, mỗi mệnh đề có tối đa hai literal, và bài toán giải được nhanh. Trong 3-SAT, mỗi mệnh đề có ba literal, và bài toán đã NP-đầy đủ, chưa có thuật toán nào được biết là luôn nhanh.
Bộ giải SAT được dùng để làm gì?
Dùng để kiểm chứng thiết kế chip (hai mạch có tương đương không), tìm lỗi phần mềm, xếp lịch, phân công, kiểm cấu hình và tìm phiên bản phần mềm tương thích. Dù khó về lý thuyết, nhiều công thức thực tế có hàng triệu biến vẫn được giải.
