Risolutore 3-SAT Python

Question

Ho scritto un risolutore 3-SAT basato su questo prompt:

Alice ha recentemente iniziato a lavorare per una società di progettazione hardware e come parte del suo lavoro, ha bisogno di identificare i difetti nei circuiti integrati fabbricati. Un approccio per identificare questi difetti si riduce alla risoluzione di un'istanza di soddisfacibilità. Ha bisogno del tuo aiuto per scrivere un programma per svolgere questo compito.

Input
La prima riga di input contiene un singolo numero intero, non più di 5, che indica il numero di casi di test da seguire. La prima riga di ogni test case contiene due numeri interi n e m dove 1 ≤ n ≤ 20 indica il numero di variabili e 1 ≤ m ≤ 100 indica il numero di clausole. Quindi, seguono m righe corrispondenti a ciascuna clausola. Ogni clausola è una disgiunzione di letterali nella forma Xi o ~ Xi per 1 ≤ i ≤ n, dove ~ Xi indica la negazione del letterale Xi. L'operatore "or" è indicato da un carattere "v" ed è separato dai letterali con un unico spazio.

Output
Per ogni test case, visualizza soddisfacente su una singola riga se c'è un'assegnazione soddisfacente; altrimenti visualizzare insoddisfacente.

Input di esempio

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 

Output di esempio

satisfiable
unsatisfiable

Questo codice fondamentalmente mantiene mySetsche è un elenco di insiemi, che rappresentano tutti possibili combinazioni di letterali che potrebbero rendere vera l'intera affermazione. Ogni volta che analizziamo una nuova clausola, controlliamo se la sua negazione esiste già in un insieme, se lo fa, l'insieme non è incluso.

Funziona, ma è un po '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")

Penso che il problema sia qui, a causa dei for-loop rientrati. 3-SAT dovrebbe essere esponenziale, ma vorrei velocizzarlo un po '(forse rimuovendo un loop?)

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

Se strumentate il vostro codice con alcune istruzioni print posizionate strategicamente, vedrete che ci sono dei calcoli ripetuti in corso. Nel secondo caso di test durante l'elaborazione della clausola X2 v ~X3, l'insieme {'X1', 'X2'}viene aggiunto mySetsdue volte. Durante l'elaborazione della clausola X3 v ~X1, il set {'X3', 'X1', 'X2'}viene aggiunto mySetstre volte.

Per casi di grandi dimensioni, potrebbe accelerare le cose per passare mySetsa un set()invece di un elenco per eliminare i duplicati. Quindi i set interni devono essere frozensets.

mySetsè un insieme di possibili soluzioni che soddisfano tutte le clausole, quindi l'ho rinominato in candidates.

Se si inizializza candidatesper contenere un singolo set vuoto, la prima clausola non deve essere gestita separatamente.

Penso che puoi fermarti in qualsiasi momento candidatesè vuoto.

Inoltre, suddividere il codice in funzioni.

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

Chiamato come:

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

Ecco un'implementazione suggerita che non cambia praticamente nulla del tuo algoritmo, ma

• ha una rientranza adeguata
• usa un po 'di suggerimenti sul tipo
• usa set letterali e generatori
• utilizza _per variabili "non utilizzate"
• aggiunge un parse_clause()perché il codice della clausola viene ripetuto
• utilizza a StringIO, per questi scopi, per deridere efficacemente stdine utilizzare l'input di esempio che hai mostrato
• utilizza nomi conformi a PEP8 (con trattini bassi)

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