Python solucionador 3-SAT

Question

Escribí un solucionador de 3-SAT basado en este mensaje:

Alice comenzó recientemente a trabajar para una empresa de diseño de hardware y, como parte de su trabajo, necesita identificar defectos en circuitos integrados fabricados. Un enfoque para identificar estos defectos se reduce a resolver una instancia de satisfacibilidad. Ella necesita su ayuda para escribir un programa para realizar esta tarea.

Entrada
La primera línea de entrada contiene un solo número entero, no más de 5, que indica el número de casos de prueba a seguir. La primera línea de cada caso de prueba contiene dos números enteros nym donde 1 ≤ n ≤ 20 indica el número de variables y 1 ≤ m ≤ 100 indica el número de cláusulas. Luego, siguen m líneas correspondientes a cada cláusula. Cada cláusula es una disyunción de literales en la forma Xi o ~ Xi para algunos 1 ≤ i ≤ n, donde ~ Xi indica la negación del literal Xi. El operador "o" se indica con un carácter 'v' y se separa de los literales con un solo espacio.

Salida
Para cada caso de prueba, muestre satisfactoria en una sola línea si hay una asignación satisfactoria; de lo contrario, mostrar insatisfactorio.

Entrada de muestra

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 

Salida de muestra

satisfiable
unsatisfiable

Este código básicamente mantiene mySetscuál es una lista de conjuntos, los cuales representan posibles combinaciones de literales que podrían hacer que toda la declaración sea verdadera. Cada vez que analizamos una nueva cláusula, verificamos si su negación ya existe en un conjunto, si es así, el conjunto no está incluido.

Esto funciona, pero funciona un poco lento.

import sys

cases = int(sys.stdin.readline())


def GetReverse(literal):
    if literal[0] == '~':
    return literal[1:]
    else:
        return '~' + literal


for i in range(cases):
    vars, clauses = map(int, sys.stdin.readline().split())

mySets = []

firstClause = sys.stdin.readline().strip().split(" v ")

for c in firstClause:
    this = set()
    this.add(c)
    mySets.append(this)


for i in range(clauses-1):
    tempSets = []
    currentClause = sys.stdin.readline().strip().split(" v ")

    for s in mySets:
        for literal in currentClause:

            if not s.__contains__(GetReverse(literal)):


                newset = s.copy()
                newset.add(literal)

                tempSets.append(newset)
    mySets = tempSets


if mySets:
    print("satisfiable")
else:
    print("unsatisfiable")

Creo que el problema está aquí, debido a los bucles for con sangría. Se supone que 3-SAT es exponencial, pero me gustaría acelerarlo un poco (¿quizás eliminando un bucle?)

for i in range(clauses-1):
    tempSets = []
    currentClause = sys.stdin.readline().strip().split(" v ")

    for s in mySets:
        for literal in currentClause:

            if not s.__contains__(GetReverse(literal)):


                newset = s.copy()
                newset.add(literal)

                tempSets.append(newset)
    mySets = tempSets

Answer 1

Si instrumenta su código con algunas declaraciones de impresión ubicadas estratégicamente, verá que se están realizando algunos cálculos repetidos. En el segundo caso de prueba, al procesar la cláusula X2 v ~X3, el conjunto {'X1', 'X2'}se agrega mySetsdos veces. Al procesar la cláusula X3 v ~X1, el conjunto {'X3', 'X1', 'X2'}se agrega mySetstres veces.

Para casos grandes, podría acelerar el cambio mySetsa set()una lista en lugar de a una para eliminar los duplicados. Entonces los conjuntos internos deben serlo frozensets.

mySetses un conjunto de posibles soluciones que satisfacen todas las cláusulas, así que le cambié el nombre a candidates.

Si inicializa candidatespara contener un solo conjunto vacío, entonces la primera cláusula no necesita manejarse por separado.

Creo que puedes parar en cualquier momento que candidatesesté vacío.

Además, divida el código en funciones.

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

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

o

import sys

main(sys.stdin)        

Answer 2

Aquí hay una implementación sugerida que básicamente no cambia nada sobre su algoritmo, pero

• tiene la sangría adecuada
• usa un poco de sugerencia de tipo
• usa conjuntos literales y generadores
• usos _de variables "no utilizadas"
• agrega un parse_clause()porque el código de la cláusula se repite
• utiliza a StringIO, para estos fines, para simular stdiny usar de manera efectiva la entrada de ejemplo que mostró
• utiliza nombres que cumplen con PEP8 (con guiones bajos)

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