3-SAT Решатель Python

Если вы инструментируете свой код с помощью некоторых стратегически размещенных операторов печати, вы увидите, что происходят некоторые повторяющиеся вычисления. Во втором тестовом примере при обработке предложения X2 v ~X3набор {'X1', 'X2'}добавляется mySetsдважды. При обработке предложения X3 v ~X1набор {'X3', 'X1', 'X2'}добавляется до mySetsтрех раз.

В больших случаях это может ускорить переход mySetsна a 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')