Python 3-SAT Solver

Question

Tôi đã viết một trình giải 3 SAT dựa trên lời nhắc này :

Alice gần đây bắt đầu làm việc cho một công ty thiết kế phần cứng và là một phần công việc của mình, cô ấy cần xác định các khiếm khuyết trong các mạch tích hợp được chế tạo. Một cách tiếp cận để xác định những khiếm khuyết này tập trung vào việc giải quyết một trường hợp thỏa đáng. Cô ấy cần sự giúp đỡ của bạn để viết một chương trình để thực hiện nhiệm vụ này.

Đầu vào
Dòng đầu tiên chứa một số nguyên duy nhất, không quá 5, cho biết số lượng trường hợp thử nghiệm cần tuân theo. Dòng đầu tiên của mỗi test case chứa hai số nguyên n và m trong đó 1 ≤ n ≤ 20 cho biết số biến và 1 ≤ m ≤ 100 cho biết số mệnh đề. Sau đó, m dòng tiếp theo tương ứng với mỗi mệnh đề. Mỗi mệnh đề là một tổ hợp của các từ ở dạng Xi hoặc ~ Xi với một số 1 ≤ i ≤ n, trong đó ~ Xi biểu thị sự phủ định của từ Xi. Toán tử “hoặc” được biểu thị bằng ký tự 'v' và được phân tách khỏi các ký tự bằng một khoảng trắng.

Kết quả
Đối với mỗi trường hợp thử nghiệm, hiển thị thỏa mãn trên một dòng duy nhất nếu có nhiệm vụ thỏa mãn; nếu không thì hiển thị không đạt yêu cầu.

Đầu vào mẫu

2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3 

Đầu ra mẫu

satisfiable
unsatisfiable

Mã này về cơ bản duy trì mySetsđó là một danh sách các tập hợp, tất cả đều đại diện cho các kết hợp có thể có của các ký tự có thể làm cho toàn bộ câu lệnh đúng. Mỗi khi chúng tôi phân tích cú pháp một mệnh đề mới, chúng tôi kiểm tra xem nó có tồn tại phủ định trong một tập hợp hay không, nếu có thì tập hợp đó không được bao gồm.

Điều này hoạt động, nhưng nó chạy hơi chậm.

import sys

cases = int(sys.stdin.readline())


def GetReverse(literal):
    if literal[0] == '~':
    return literal[1:]
    else:
        return '~' + literal


for i in range(cases):
    vars, clauses = map(int, sys.stdin.readline().split())

mySets = []

firstClause = sys.stdin.readline().strip().split(" v ")

for c in firstClause:
    this = set()
    this.add(c)
    mySets.append(this)


for i in range(clauses-1):
    tempSets = []
    currentClause = sys.stdin.readline().strip().split(" v ")

    for s in mySets:
        for literal in currentClause:

            if not s.__contains__(GetReverse(literal)):


                newset = s.copy()
                newset.add(literal)

                tempSets.append(newset)
    mySets = tempSets


if mySets:
    print("satisfiable")
else:
    print("unsatisfiable")

Tôi nghĩ rằng vấn đề là ở đây, do các vòng lặp for bị thụt vào. 3-SAT được cho là theo cấp số nhân, nhưng tôi muốn tăng tốc độ nó lên một chút (có lẽ bằng cách loại bỏ một vòng lặp?)

for i in range(clauses-1):
    tempSets = []
    currentClause = sys.stdin.readline().strip().split(" v ")

    for s in mySets:
        for literal in currentClause:

            if not s.__contains__(GetReverse(literal)):


                newset = s.copy()
                newset.add(literal)

                tempSets.append(newset)
    mySets = tempSets

Answer 1

Nếu bạn thiết lập mã của mình bằng một số câu lệnh in được đặt một cách chiến lược, bạn sẽ thấy rằng có một số tính toán lặp lại đang diễn ra. Trong trường hợp thử nghiệm thứ hai khi xử lý mệnh đề X2 v ~X3, tập hợp {'X1', 'X2'}được thêm vào mySetshai lần. Khi xử lý mệnh đề X3 v ~X1, tập hợp {'X3', 'X1', 'X2'}được thêm vào mySetsba lần.

Đối với các trường hợp lớn, có thể tăng tốc độ thay đổi mySetsthành set()một danh sách thay vì một danh sách để loại bỏ các bản sao. Sau đó, các bộ bên trong cần phải được frozensets.

mySetslà một tập hợp các giải pháp có thể thỏa mãn tất cả các mệnh đề, vì vậy tôi đã đổi tên nó thành candidates.

Nếu bạn khởi tạo candidatesđể chứa một tập hợp trống, thì mệnh đề đầu tiên không cần phải được xử lý riêng.

Tôi nghĩ rằng bạn có thể dừng lại bất cứ lúc nào candidatestrống rỗng.

Ngoài ra, hãy chia mã thành các chức năng.

def is_satisfiable(n_vars, clauses):
    candidates = {frozenset()}

    for clause in clauses:
        temp = set()

        for s in candidates:
            for literal in clause:

                if GetReverse(literal) not in s:

                    temp.add(s | {literal})

        candidates = temp
        
        if len(candidates) == 0:
            return False

    return True
        
        
def load_case(f):
    n_vars, n_clauses = f.readline().split()
    clauses = [f.readline().strip().split(' v ') for _ in range(int(n_clauses))]
    return int(n_vars), clauses
    
    
def main(f=sys.stdin):
    num_cases = int(f.readline())

    for i in range(num_cases):
        n_vars, clauses = load_case(f)
        result = is_satisfiable(n_vars, clauses)
        
        print(f"{'satisfiable' if result else 'unsatisfiable'}")

Được gọi là:

import io

data = """
2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3 
""".strip()

main(io.StringIO(data))

hoặc là

import sys

main(sys.stdin)        

Answer 2

Đây là cách triển khai được đề xuất về cơ bản không thay đổi gì về thuật toán của bạn, nhưng

• có thụt lề thích hợp
• sử dụng một chút gợi ý về kiểu
• sử dụng tập hợp các ký tự và trình tạo
• sử dụng _cho các biến "không sử dụng"
• thêm a parse_clause()vì mã mệnh đề được lặp lại
• sử dụng a StringIO, cho những mục đích này, để mô phỏng một cách hiệu quả stdinvà sử dụng đầu vào ví dụ mà bạn đã hiển thị
• sử dụng các tên tuân thủ PEP8 (có dấu gạch dưới)

from io import StringIO
from typing import List

stdin = StringIO('''2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3
'''
)


def get_reverse(literal: str) -> str:
    if literal[0] == '~':
        return literal[1:]
    return '~' + literal


def parse_clause() -> List[str]:
    return stdin.readline().strip().split(' v ')


n_cases = int(stdin.readline())
for _ in range(n_cases):
    n_vars, n_clauses = (int(s) for s in stdin.readline().split())
    my_sets = [{c} for c in parse_clause()]

    for _ in range(n_clauses - 1):
        temp_sets = []
        current_clause = parse_clause()

        for s in my_sets:
            for literal in current_clause:
                if get_reverse(literal) not in s:
                    new_set = s.copy()
                    new_set.add(literal)
                    temp_sets.append(new_set)

        my_sets = temp_sets

    if my_sets:
        print('satisfiable')
    else:
        print('unsatisfiable')