Un algorithme de satisfiabilité provisoire

La satisfiabilité générale (à quelques exceptions telles que les clauses de Horn) ne semble pas avoir de solution algorithmique. Cependant, l'algorithme suivant semble être une solution pour la satisfiabilité générale. Quel est exactement le défaut de l'algorithme suivant?

Laisser $W$ être un ensemble vide qui contiendra toutes les variables qui doivent nécessairement être vraies ou fausses.
Laisser $L$ être l'ensemble des clauses.
Boucle à travers $L$ .
Chaque fois qu'une variable non conditionnelle ^† est trouvée, supprimez-la de $L$ et l'insérer dans $W$ .
Si ce qui laisse un vide et l' implication ^‡ , supprimer toutes les variables de cette implication vide de et l' insérer dans . $L$ $W$
Si cela laisse une implication OU vide ^‡ , créez de nouvelles instances de l'algorithme, où chaque instance traite une variable dans l'implication (c'est-à-dire si l'implication est: , créez une instance où est inséré dans , un où est inséré dans et un où et sont insérés dans ). $x V \implies y$ $x$ $W$ $y$ $W$ $x$ $y$ $W$
Définissez toutes les variables dans $W$ à la valeur qu'ils doivent nécessairement être.
Réinsérez les variables dans $W$ dans $L$ avec leurs valeurs modifiées et vérifiez si toutes les clauses sont satisfaites.
Si la satisfiabilité est satisfaite, retournez $L$ , sinon retournez "Not Satisfiable".

^† Une variable non conditionnelle est définie comme une variable nécessaire vraie ou fausse, par exemple $\implies x$ ou $\implies \neg y$ .

^‡ Une implication vide est définie comme une implication où un côté est vide (par ex. $\implies x \wedge y$ ) ou l'autre côté est nécessairement vrai (par exemple . $\mathrm{true} \vee a \implies b$

Pour obtenir une compréhension plus intuitive de l'algorithme, considérez l'ensemble de clauses suivant $L$ :

\begin{aligned} une \land b & ⟹ c & (je) \\ ⟹ F \land g & (ii) \\ F & ⟹ \neg une & (iii) \\ F \lor une & ⟹ b & (iv) \\ ⟹ c & (v) \end{aligned}

$\begin{align} a \wedge b &\implies c & \text{(i)} \\ &\implies f \wedge g & \text{(ii)} \\ f &\implies \neg a & \text{(iii)} \\ f \vee a &\implies b & \text{(iv)} \\ &\implies c & \text{(v)} \\ \end{align}$

L'algorithme fera ce qui suit:

1) Depuis $c$ , $f$ , $g$ sont des variables non conditionnelles, l'algorithme les insérera dans $W$ . $W = \{c, f, g\}$ .

2) Suppression $c$ , $f$ et $g$ laissera les clauses vides: $\implies \neg a, a \wedge b, b$ . Ceux-ci seront ajoutés à $W$ . $W = \{c, f, g, b, \neg a\}$ .

3) Réinsérer les variables dans $L$ entraînera la violation des premières clauses: $a \wedge b \implies c$ . Depuis $a$ c'est faux, $c$ est faux, ce qui signifie que la clause (v) est violée. L'algorithme renverra "Non satisfaisant"

Je suis conscient que l'algorithme semble déroutant. N'hésitez pas à demander des éclaircissements.

D'après les commentaires, je me rends compte maintenant qu'il n'y a pas d' algorithme de satisfiabilité générale efficace connu . Je suis toujours intéressé par les commentaires sur mon algorithme. Est-ce que ça marche? Comment se compare-t-il aux algorithmes courants?

algorithms logic satisfiability constraint-programming Gilles 'SO- arrête d'être méchant'
la source

Qu'est-ce qui vous fait penser qu'il n'y a pas de solution algorithmique à la satisfiabilité générale? Il existe absolument des algorithmes pour ce faire; aucun d'entre eux n'est connu pour avoir les temps d'exécution polynomiaux les plus défavorables, cependant. Ce que vous décrivez semble être un algorithme de satisfiabilité basé sur la résolution bien connu.

templatetypedef

@templatetypedef L'article de Wikipedia semble suggérer qu'aucune solution n'existe. Par hasard, pourriez-vous me référer à l'algorithme bien connu?

@Riddler ce que l'article de Wikipédia dit en fait est "SAT a été le premier exemple connu d'un problème NP-complet. Cela signifie brièvement qu'il n'y a pas d'algorithme connu qui résout efficacement toutes les instances de SAT" Il a également un "Algorithmes pour résoudre SAT" section.

Il existe certainement des solutions algorithmiques à la satisfiabilité générale car il existe des solutions de force brute (affectant toutes les combinaisons de valeurs Vrai / Faux aux variables et voyant si l'une des expressions résultantes est évaluée à Vrai).

Le problème est que vous générez un nombre exponentiel de nouvelles instances à partir des OR vides dans le pire des cas.

Elliot Gorokhovsky

Réponses:

Problème 1

L'affaire de $(x\rightarrow y \vee \overline y)$ devrait être une "variable non conditionnelle" en ce qui concerne $x$ (c'est-à-dire que $\overline x$ devrait maintenant être inséré dans $W$ ). Si ce n'est pas vrai, votre algorithme a besoin d'une étape supplémentaire pour en déduire. En supposant $(x\rightarrow y \vee \overline y)$ est une " variable non conditionnelle ", continuons-nous.

Problème 2

REMARQUE: c'est un problème que j'ai remarqué; il peut très bien y avoir d'autres problèmes.

Le problème est avec la " implication OR vide " divisée en deux algorithmes, c'est que dans sa forme actuelle, la division ne couvre pas tous les cas. En particulier:

Vous commencez avec $(x \vee c \rightarrow y)$ , puis $c$ est supprimé et nous nous retrouvons avec une implication OU vide de $(x \vee [] \rightarrow y)$ . Vous suggérez maintenant de le diviser en deux nouveaux problèmes et de résoudre chacun d'eux; un avec $x=T\wedge y=T$ et un où $y=T$ . Mais cela ne couvre pas tous les cas. Et le cas quand $x=F\vee y=F$ . Cependant, votre algorithme ne considère jamais la possibilité que $y$ c'est faux.

Je pense que vous pourriez être en mesure de résoudre ce problème en formulant les deux nouveaux problèmes en un seul avec $y$ et un avec $\overline x$ .

Problème 3

Que se passe-t-il lorsque vous vous retrouvez avec un tas de clauses sous la forme:

(une \land b \to c)

$(a\wedge b \rightarrow c)$

(une \to b \lor c)

$(a \rightarrow b \vee c)$

Après avoir tout réduit, ces clauses resteront et vous ne pourrez pas tester facilement leur satisfiabilité.

Une analyse

Remarque : Cette notation "O", $\mathcal{O}(something)$ etc., que l' on appelle la notation Big O . $\Omega(something)$ s'appelle Big-omega.

En supposant que l'algorithme fonctionnait en général, il fonctionnerait en temps de $\Omega(2^m)$ pire cas, $m$ étant le nombre de variables. La raison en est que chaque division d'un problème en problèmes de taille similaire signifie que l'algorithme s'exécute en temps exponentiel. Pour visualiser ce concept, regardez l'image suivante d'un arbre binaire complet (image d' ici ):

diagramme d'arbre binaire complet

Imaginez maintenant que le problème d'origine est le nœud en haut. Nous avons divisé le problème en deux problèmes au deuxième niveau, mais ils sont de taille similaire (nous nous débarrassons d'une seule variable, $x$ ou $y$ à partir de l' implication OR vide , nous aurons donc encore beaucoup d' implications OR vides pour chaque niveau). Nous devrons potentiellement diviser le problème $\mathcal{O}(m)$ fois pour se débarrasser de $m$ variables. Cela signifie que nous devrons faire face à un arbre avec $m$ niveaux. Un arbre avec $m$ niveaux a $2^m$ nœuds foliaires (nœuds en bas). C'est ce qu'on appelle le temps exponentiel, et est officieusement quelque peu comparable à tous les algorithmes de satisfiabilité booléenne connus. Mais la force brute aussi: il y a $2^m$ affectations possibles des variables, donc par force brute, vous pouvez deviner chaque affectation et vérifier la satisfiabilité avec des performances similaires!

Realz Slaw
la source

Je suppose que tu veux dire

Ω (.)

$\Omega(.)$ ?

Raphael

TBH je ne sais pas si

Ω

$\Omega$ est approprié, car dans le meilleur des cas, l'algorithme peut être résolu rapidement. Je voulais dire que la limite supérieure était pire (ou au moins aussi mauvaise que)

O (2^{m})

$\mathcal{O}(2^m)$ . Je ne sais pas comment le dire correctement. Le point principal de la notation O est cependant de nous débarrasser des constantes. S'il existe une meilleure façon de l'exprimer, n'hésitez pas à l'éditer.

Realz Slaw

Peut-on dire que "le pire des cas est

Ω (2^{m})

$\Omega(2^m)$ "?

Realz Slaw

Une fois que vous êtes qualifié de «pire des cas», c'est ce dont nous parlons, pas de meilleur cas en cause. "pire que

O (.)

$O(.)$ "(quoi que" pire que cette limite supérieure "signifie) est en effet ce que

Ω (.)

$\Omega(.)$ (une borne inférieure) dit; voir aussi ici . Dans ce cas, le pire cas d'exécution dans

Ω (2^{m})

$\Omega(2^m)$ semble être ce que vous voulez dire. De même, vous voulez

Θ (m)

$\Theta(m)$ ou

Ω (m)

$\Omega(m)$ dans le dernier paragraphe.

Raphael

-5

Avant de vous sentir que vous avez un "nouvel" algorithme SAT, veuillez consulter l'algorithme de recherche / retour en arrière standard / classique dans la littérature pour le problème datant de ~ 1962, l' algorithme Davis – Putnam – Logemann – Loveland . la plupart des algorithmes de retour en arrière / récursifs pour le problème finiront probablement par ressembler quelque peu à cet algorithme, bien qu'il puisse falloir un certain temps pour démontrer cette équivalence.

Une analyse sérieuse impliquerait de comparer votre algorithme à des exemples (ou instances aléatoires) par rapport à DPLL.

Il est donc utile de résumer simplement en quoi votre algorithme en diffère. sans revoir votre code, les chances sont les suivantes:

L'algorithme contient un bogue. soit renvoyer des faux positifs ou des négatifs (c'est-à-dire que l'algorithme renvoie "la formule est satisfiable" lorsqu'elle ne l'est pas ou vice versa, respectivement). cela peut généralement être détecté par des tests très approfondis d'une large gamme de formules générées de manière aléatoire et par la comparaison avec un autre algorithme / implémentation correcte connue, par exemple DPLL.
Votre algorithme n'est pas aussi bon que DPLL.
Si elle est aussi bonne que DPLL ou "meilleure", elle est généralement due aux branchements et aux heuristiques / stratégies de sélection de variables et à la distribution des instances sous test.

L'algorithme peut être facilement compris par un étudiant de premier cycle intelligent, mais il semble rarement enseigné au niveau du premier cycle ou dans les manuels de premier cycle, ou peut-être même pas souvent référencé, ce qui peut conduire à une vision erronée ou à une impression que les algorithmes SAT de base ne sont pas bien compris, etc.

Récemment, nous venons de parcourir ce site "en direct" appelé ToughSat par Yuen et Bebel pour générer des instances matérielles à utiliser avec l'analyse comparative, certaines basées sur la factorisation [l'une des méthodes classiques de génération d'instances matérielles SAT]. il y en a d'autres, par exemple les DIMAC qui stockent les archives des instances matérielles bien qu'il ne soit plus en ligne.

vzn
la source