3-SATソルバーPython

戦略的に配置されたprintステートメントを使用してコードをインストルメント化すると、計算が繰り返されていることがわかります。句を処理するときの2番目のテストケースX2 v ~X3では、セット{'X1', 'X2'}がmySets2回追加されます。句を処理するときX3 v ~X1、セット{'X3', 'X1', 'X2'}はmySets3回追加されます。

大規模なケースでは、重複を排除するためにリストでmySetsは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')