3-SAT Solver Python

หากคุณใช้รหัสของคุณด้วยคำสั่งพิมพ์ที่วางกลยุทธ์คุณจะเห็นว่ามีการคำนวณซ้ำ ๆ เกิดขึ้น ในกรณีทดสอบที่สองเมื่อประมวลผลอนุประโยคX2 v ~X3เซต{'X1', 'X2'}จะถูกเพิ่มเป็นmySetsสองครั้ง เมื่อประมวลผลประโยคX3 v ~X1ชุด{'X3', 'X1', 'X2'}จะถูกเพิ่มเป็นmySetsสามครั้ง

สำหรับกรณีที่มีขนาดใหญ่ก็อาจจะเร็วขึ้นจะเปลี่ยนmySetsไปset()แทนของรายการที่จะกำจัดรายการที่ซ้ำกัน frozensetsจากนั้นชุดชั้นในจะต้อง

mySetscandidatesเป็นชุดของการแก้ปัญหาไปได้ว่าตอบสนองคำสั่งทั้งหมดดังนั้นฉันมันเปลี่ยนไป

หากคุณเริ่มต้นcandidatesให้มีชุดว่างชุดเดียวประโยคแรกไม่จำเป็นต้องจัดการแยกกัน

ฉันคิดว่าคุณสามารถหยุดได้ทุกเมื่อที่candidatesว่างเปล่า

แยกโค้ดออกเป็นฟังก์ชัน

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'}")

เรียกว่า:

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))

หรือ

import sys

main(sys.stdin)        

นี่คือการใช้งานที่แนะนำซึ่งโดยพื้นฐานแล้วไม่มีอะไรเปลี่ยนแปลงเกี่ยวกับอัลกอริทึมของคุณ แต่

• มีการเยื้องที่เหมาะสม
• ใช้การบอกใบ้ประเภทเล็กน้อย
• ใช้ชุดตัวอักษรและเครื่องกำเนิดไฟฟ้า
• ใช้_สำหรับตัวแปร "ไม่ได้ใช้"
• เพิ่มparse_clause()เนื่องจากรหัสประโยคซ้ำ
• ใช้ a StringIOเพื่อวัตถุประสงค์เหล่านี้เพื่อล้อเลียนอย่างมีประสิทธิภาพstdinและใช้ข้อมูลตัวอย่างที่คุณแสดง
• ใช้ชื่อที่สอดคล้องกับ PEP8 (มีขีดล่าง)

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')