3-SAT 솔버 Python

전략적으로 배치하는 print 문을 사용하여 코드를 계측하면 반복되는 계산이 진행되고 있음을 알 수 있습니다. 두 번째 테스트 케이스에서 절을 처리 할 때 X2 v ~X3세트 {'X1', 'X2'}가 mySets두 번 추가됩니다 . 절을 처리 할 때 X3 v ~X1집합 {'X3', 'X1', 'X2'}이 mySets세 번 추가됩니다 .

큰 경우 에는 중복을 제거하기 위해 목록 대신 mySetsa 로 변경 하는 속도를 높일 수 있습니다 set(). 그런 다음 내부 세트는 frozensets.

mySets모든 절을 충족하는 가능한 솔루션 집합이므로 이름을 candidates.

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()절 코드가 반복되기 때문에 추가
• 사용 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')