Solveur 3-SAT Python

Question

J'ai écrit un solveur 3-SAT basé sur cette invite:

Alice a récemment commencé à travailler pour une entreprise de conception de matériel et dans le cadre de son travail, elle doit identifier les défauts dans les circuits intégrés fabriqués. Une approche pour identifier ces défauts se résume à résoudre une instance de satisfiabilité. Elle a besoin de votre aide pour écrire un programme pour accomplir cette tâche.

Entrée
La première ligne d'entrée contient un seul entier, pas plus de 5, indiquant le nombre de cas de test à suivre. La première ligne de chaque cas de test contient deux entiers n et m où 1 ≤ n ≤ 20 indique le nombre de variables et 1 ≤ m ≤ 100 indique le nombre de clauses. Ensuite, m lignes suivent correspondant à chaque clause. Chaque clause est une disjonction de littéraux sous la forme Xi ou ~ Xi pour un certain 1 ≤ i ≤ n, où ~ Xi indique la négation du littéral Xi. L'opérateur «ou» est désigné par un caractère «v» et est séparé des littéraux par un seul espace.

Sortie
Pour chaque cas de test, afficher satisfiable sur une seule ligne s'il existe une affectation satisfaisable; sinon afficher insatisfaisant.

Exemple d'entrée

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 

Exemple de sortie

satisfiable
unsatisfiable

Ce code maintient essentiellement mySetsune liste d'ensembles, qui représentent tous des combinaisons possibles de littéraux qui pourraient rendre la déclaration entière vraie. Chaque fois que nous analysons une nouvelle clause, nous vérifions si sa négation existe déjà dans un ensemble, si c'est le cas, l'ensemble n'est pas inclus.

Cela fonctionne, mais cela fonctionne un peu lentement.

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

Je pense que le problème est ici, en raison des boucles for indentées. 3-SAT est censé être exponentiel, mais je voudrais l'accélérer un peu (peut-être en supprimant une boucle?)

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 vous instrumentez votre code avec des instructions d'impression placées stratégiquement, vous verrez qu'il y a des calculs répétés en cours. Dans le deuxième cas de test lors du traitement de la clause X2 v ~X3, l'ensemble {'X1', 'X2'}est ajouté mySetsdeux fois. Lors du traitement de la clause X3 v ~X1, l'ensemble {'X3', 'X1', 'X2'}est ajouté mySetstrois fois.

Pour les cas importants, cela peut accélérer les choses pour passer mySetsà set()une liste au lieu d'une liste pour éliminer les doublons. Ensuite, les ensembles intérieurs doivent l'être frozensets.

mySetsest un ensemble de solutions possibles qui satisfont toutes les clauses, je l'ai donc renommé candidates.

Si vous initialisez candidatespour contenir un seul ensemble vide, la première clause n'a pas besoin d'être gérée séparément.

Je pense que vous pouvez arrêter à tout moment candidatesest vide.

De plus, divisez le code en fonctions.

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

Appelé comme:

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)        

Answer 2

Voici une implémentation suggérée qui ne change fondamentalement rien à votre algorithme, mais

• a une indentation appropriée
• utilise un peu d'indices de type
• utilise des ensembles littéraux et des générateurs
• utilise _pour les variables "inutilisées"
• ajoute un parse_clause()car le code de la clause est répété
• utilise un StringIO, à ces fins, pour se moquer efficacement stdinet utiliser l'exemple d'entrée que vous avez montré
• utilise des noms conformes PEP8 (avec des traits de soulignement)

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