3-SAT Solver Python

Se você instrumentar seu código com algumas instruções de impressão colocadas estrategicamente, verá que há alguns cálculos repetidos em andamento. No segundo caso de teste, ao processar a cláusula X2 v ~X3, o conjunto {'X1', 'X2'}é adicionado mySetsduas vezes. Ao processar a cláusula X3 v ~X1, o conjunto {'X3', 'X1', 'X2'}é adicionado mySetstrês vezes.

Para casos grandes, pode acelerar as coisas mudar mySetspara um em set()vez de uma lista para eliminar as duplicatas. Então, os conjuntos internos precisam ser frozensets.

mySetsé um conjunto de soluções possíveis que satisfazem todas as cláusulas, por isso mudei o nome para candidates.

Se você inicializar candidatespara conter um único conjunto vazio, a primeira cláusula não precisará ser tratada separadamente.

Eu acho que você pode parar quando candidatesestiver vazio.

Além disso, divida o código em funções.

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

Chamado como:

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

ou

import sys

main(sys.stdin)        

Aqui está uma implementação sugerida que não muda basicamente nada em seu algoritmo, mas

• tem indentação adequada
• usa um pouco de sugestão de tipo
• usa conjuntos literais e geradores
• usa _para variáveis ​​"não utilizadas"
• adiciona um parse_clause()porque o código da cláusula é repetido
• usa um StringIO, para esses fins, para efetivamente zombar stdine usar o exemplo de entrada que você mostrou
• usa nomes compatíveis com PEP8 (com sublinhados)

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