3-SAT Solver Python

Wenn Sie Ihren Code mit strategisch platzierten Druckanweisungen instrumentieren, werden Sie feststellen, dass einige wiederholte Berechnungen durchgeführt werden. Im zweiten Testfall bei der Verarbeitung der Klausel X2 v ~X3wird die Menge zweimal {'X1', 'X2'}hinzugefügt mySets. Bei der Verarbeitung der Klausel X3 v ~X1wird die Menge dreimal {'X3', 'X1', 'X2'}hinzugefügt mySets.

In großen Fällen kann es schneller sein, Änderungen mySetsan set()einer Liste vorzunehmen, um die Duplikate zu entfernen. Dann müssen die inneren Sätze sein frozensets.

mySetsist eine Reihe möglicher Lösungen, die alle Klauseln erfüllen, daher habe ich sie in umbenannt candidates.

Wenn Sie initialisieren candidates, um eine einzelne leere Menge zu enthalten, muss die erste Klausel nicht separat behandelt werden.

Ich denke, Sie können jederzeit aufhören, wenn candidateses leer ist.

Teilen Sie den Code auch in Funktionen auf.

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

Genannt wie:

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

oder

import sys

main(sys.stdin)        

Hier ist eine vorgeschlagene Implementierung, die im Grunde nichts an Ihrem Algorithmus ändert, aber

• hat die richtige Einrückung
• verwendet ein wenig Typhinweis
• verwendet Set-Literale und Generatoren
• wird _für "nicht verwendete" Variablen verwendet
• fügt ein hinzu, parse_clause()weil der Klauselcode wiederholt wird
• verwendet a StringIOfür diese Zwecke, stdinum die von Ihnen gezeigte Beispieleingabe effektiv zu verspotten und zu verwenden
• verwendet PEP8-kompatible Namen (mit Unterstrichen)

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