Dùng MiniSat để giải các bài toán NP

MiniSat là một công cụ nguồn mở để giải bài toán SAT (boolean satisfiability problem). Nhiều bài toán NP khác có thể được đưa về SAT, từ đó sử dụng MiniSat để giải.

Trước khi sử dụng, ta cần cài MiniSat, do MiniSat chạy trên Linux nên ta cần Cygwin hoặc Bash (Windows 10) để có thể cài được.

Dùng MiniSat có thể đảm bảo kết quả ra chính xác, code chạy nhanh. Vì vậy có thể dùng MiniSat để kiểm tra xem code của mình có chạy đúng không.

SAT, MiniSat

Định nghĩa bài toán SAT

SAT có tên gốc là boolean satisfiability problem, nghĩa là tìm cách thoả mãn một biểu thức boolean.

Ví dụ: tìm \(x, y, z\) để biểu thức \((x \lor y) \land (\neg x \lor z) \land (y \lor z)\) cho giá trị đúng.

Nhập input cho MiniSat

Để nhập input cho MiniSat, ta cần biến đổi biểu thức về dạng chuẩn (Conjunctive Normal Form - CNF), nghĩa là biểu thức được viết dưới dạng các vế, trong mỗi vế gồm các biến được nối nhau bởi phép OR, và các vế được nối nhau bởi phép AND.

Ví dụ ở trên là một biểu thức chuẩn. Ngoài ra, mọi biểu thức boolean đều có thể đưa về dạng chuẩn, ví dụ như biểu thức \((x \land y) \to z\) được đưa về dạng chuẩn là \(\neg x \lor \neg y \lor z\).

Sau khi đã đưa được về dạng chuẩn, ta đánh số các biến bắt đầu từ 1, sau đó tạo input cho MiniSat. Mỗi vế trong input được viết trên một dòng kết thúc bằng số 0, và \(\neg x\) được viết thành \(-x\). Ngoài ra, ở đầu file ta ghi dòng sau:

p cnf <số biến> <số vế>

Ví dụ biểu thức \((x \lor y) \land (\neg x \lor z) \land (y \lor z)\) cho input là:

p cnf 3 3
1 2 0
-1 3 0
2 3 0

Biểu thức \(\neg x \lor \neg y \lor z\) cho input là:

p cnf 3 1
-1 -2 3 0

Output của MiniSat

Sau khi tạo được file input, ta chạy MiniSat và được file output. Ví dụ input:

p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

Có output sau:

SAT
1 2 -3 4 5 0

Với ý nghĩa biến thứ 1, 2, 4, 5 có giá trị TRUE, biến thứ 3 có giá trị FALSE.

Nếu không giải được, MiniSat sẽ xuất UNSAT.

Giải bài 8 quân hậu bằng MiniSat

Ta sẽ chuyển bài toán quân hậu về SAT để giải bằng cách gán mỗi ô trên bàn cờ với một biến boolean \(x_{ij}\).

Vì mỗi hàng cần có ít nhất một quân hậu nên ta có \(x_{i1} \lor x_{i2} \lor ... \lor x_{i8}\) với mỗi hàng \(i\).

Ta sẽ xây dựng biểu thức cho điều kiện mỗi hàng có nhiều nhất 1 quân hậu. Xét hàng 1, giả sử ô (1, 1) có quân hậu thì tất cả các ô còn lại không được có hậu. Ta có điều kiện:

Làm tương tự với các ô khác, cột khác và các đường chéo. Xem code (Python 3):

import itertools as it
import os

n = 8

clauses = []

def varnum(i, j):
    assert(i in range(n) and j in range(n))
    return i * n + j + 1

# each row contains at least one queen
for i in range(n):
    clauses.append([varnum(i, j) for j in range(n)])

# each row contains at most one queen
for i in range(n):
    for (j1, j2) in it.combinations(range(n), 2):
        clauses.append([-varnum(i, j1), -varnum(i, j2)])

# each column contains at most one queen
for j in range(n):
    for (i1, i2) in it.combinations(range(n), 2):
        clauses.append([-varnum(i1, j), -varnum(i2, j)])

# no two queens stay on the same diagonal
for (i1, i2) in it.combinations(range(n), 2):
    assert(i1 < i2)
    for (j1, j2) in it.product(range(n), repeat = 2):
        if i2 - i1 == abs(j2 - j1):
            clauses.append([-varnum(i1, j1), -varnum(i2, j2)])


with open('tmp.cnf', 'w') as f:
    f.write("p cnf {} {}\n".format(n * n, len(clauses)))
    for c in clauses:
        c.append(0);
        f.write(" ".join(map(str, c)) + "\n")

os.system("minisat tmp.cnf tmp.sat")

with open("tmp.sat", "r") as satfile:
    for line in satfile:
        if line.split()[0] == "UNSAT":
            print("There is no solution")
        elif line.split()[0] == "SAT":
            pass
        else:
            assignment = [int(x) for x in line.split()]

            #print("-" * (2 * n + 1))
            for i in range(n):
                print("|", end="")
                for j in range(n):
                    if varnum(i, j) in assignment:
                        print("x|", end="")
                    else:
                        print(" |", end="")

                print("")
                #print("-" * (2 * n + 1))

Xem thêm

• MiniSat User Guide
• Code giải quân hậu bằng MiniSat
• Code giải Sudoku bằng MiniSat