Vérification des formules avec deux quantificateurs (

Les solveurs SAT offrent un moyen puissant de vérifier la validité d'une formule booléenne avec un quantificateur.

Par exemple, pour vérifier la validité de , nous pouvons utiliser un solveur SAT pour déterminer si est satisfaisable. Pour vérifier la validité de , nous pouvons utiliser un solveur SAT pour déterminer si est satisfaisable. (Ici est un vecteur de variables booléennes, et $\exists x . \varphi(x)$ $\varphi(x)$ $\forall x . \varphi(x)$ $\neg \varphi(x)$ $x=(x_1,\dots,x_n)$ $n$ $\varphi$ est une formule booléenne.)

Les solveurs QBF sont conçus pour vérifier la validité d'une formule booléenne avec un nombre arbitraire de quantificateurs.

Et si nous avons une formule avec deux quantificateurs? Existe-t-il des algorithmes efficaces pour vérifier la validité: ceux qui sont meilleurs que de simplement utiliser des algorithmes génériques pour QBF? Pour être plus précis, j'ai une formule de la forme (ou ), et souhaitez vérifier sa validité. Existe-t-il de bons algorithmes pour cela? Edit 4/8: J'ai appris que cette classe de formules est parfois connue sous le nom de 2QBF, donc je recherche de bons algorithmes pour 2QBF. $\forall x . \exists y . \psi(x,y)$ $\exists x . \forall y . \psi(x,y)$

Spécialisation supplémentaire: dans mon cas particulier, j'ai une formule de la forme dont je veux vérifier la validité, où sont des fonctions qui produisent une sortie à bits. Existe-t-il des algorithmes pour vérifier la validité de ce type particulier de formule, plus efficacement que les algorithmes génériques pour QBF? $\forall x . \exists y . f(x)=g(y)$ $f,g$ $k$

PS Je ne demande pas la dureté du pire des cas, en théorie de la complexité. Je pose des questions sur les algorithmes pratiquement utiles (tout comme les solveurs SAT modernes sont pratiquement utiles sur de nombreux problèmes, même si SAT est NP-complet).

n'est pas essentiellement équivalent à

\forall x \exists y ψ (x, y)

$\forall x \exists y \ \psi(x,y)$

\exists x \forall y ψ (x, y)

$\exists x \forall y \ \psi(x,y)$

Huck Bennett

Je pense que l'OP signifie cela de manière informelle, en ce sens qu'ils sont tous les deux difficiles pour les solveurs SAT et qu'une solution à l'un ou l'autre serait intéressante

Suresh Venkat

@HuckBennett, je pense que les deux ont une dureté équivalente. (Preuve:

est valide si

est. Par conséquent, si nous avons un moyen de tester la validité des formules de la forme

, nous pouvons également tester la validité des formules

\exists x . \forall y . ψ (x, y)

$\exists x . \forall y . \psi(x,y)$

\neg \forall x . \exists y . \neg ψ (x, y)

$\neg \forall x . \exists y . \neg \psi(x,y)$

\forall x . \exists y . ψ (x, y)

$\forall x . \exists y . \psi(x,y)$

en laissant

et en testant la validité de

.) Mais de toute façon, je serais intéressé par les algorithmes pour les deux cas.

\exists x . \forall y . ψ (x, y)

$\exists x . \forall y . \psi(x,y)$

ψ^{'} (x, y) = \neg ψ (x, y)

$\psi'(x,y) = \neg \psi(x,y)$

\forall x . \exists y . ψ^{'} (x, y)

$\forall x . \exists y . \psi'(x,y)$

@DW, pas nécessairement, par exemple SAT et TAUT ne sont pas considérés comme ayant la même complexité.

Kaveh

@chazisop: Je pense que l'OP demande des algorithmes / solveurs

-SAT, pas des solveurs QBF généraux. Cependant, de nombreux solveurs QBF existent. Voir l'onglet "solveurs" sur qbflib.org

Π_{2} / Σ_{2}

$\Pi_2/\Sigma_2$

Huck Bennett

Réponses:

Si vous me le permettez, de manière assez flagrante, nous avons écrit un article sur l' algorithme basé sur l'abstraction pour l' an dernier pour 2QBF . J'ai une implémentation pour qdimacs, que je peux fournir si vous le souhaitez mais d'après mon expérience, on peut grandement bénéficier de la spécialisation de l'algorithme pour un problème particulier. Il existe également un article plus ancien intitulé A Comparative Study of 2QBF Algorithms , qui présente également des algorithmes assez facilement implémentables.

Mikolas
la source

Impressionnant! Merci, Mikolas, c'est exactement le genre de chose que j'espérais.

Salut @DW heureux d'avoir pu aider. J'espère que vous en trouverez une partie utile. QBF est une bête assez différente de celle de SAT, il faut donc être un peu prudent car les choses peuvent exploser très facilement :-). N'hésitez pas à m'écrire un e-mail si vous avez des questions plus détaillées sur notre travail.

Mikolas

J'ai lu deux articles à ce sujet, un spécifiquement lié au 2QBF. Les articles sont les suivants:

Détermination incrémentale , Markus N. Rabe et Sanjit Seshia, Théorie et applications des tests de satisfaction (SAT 2016).

Ils ont implémenté leur algorithme dans un outil nommé CADET . L'idée de base est d'ajouter progressivement de nouvelles contraintes à la formule jusqu'à ce que les contraintes décrivent une fonction Skolem unique ou jusqu'à ce que l'absence soit confirmée.

Le deuxième est la résolution incrémentielle du QBF , Florian Lonsing et Uwe Egly.

Implémenté dans un outil nommé DepQBF . Il n'impose aucune contrainte sur le nombre d'alternances quantifiantes. Cela commence par l'hypothèse que nous avons des formules qbf étroitement liées. Il est basé sur une résolution incrémentielle et ne renvoie pas les clauses apprises lors de la dernière résolution. Il ajoute des clauses et des cubes à la formule actuelle et s'arrête si les clauses ou les cubes sont vides, représentant insat ou sat.

Edit : Juste pour une perspective à quel point ces approches fonctionnent pour les repères 2QBF. Veuillez consulter les résultats de QBFEVal-2018 pour les résultats du concours annuel QBF QBFEVAL . En 2019, il n'y avait pas de piste 2QBF.

En 2QBF Track QBFEVAL-2018 DepQBF a été le vainqueur , CADET était le deuxième de la course.

Ces deux approches fonctionnent donc très bien en pratique (au moins sur les benchmarks QBFEVAL).

Pushpa
la source

$\exists x \forall y \phi$ $D$ $a \in D$ $\neg \phi[a/x]$ $b \in B$ $a$ $\phi [b/y]$ $\phi$

Samuel Schlesinger
la source

ϕ

$\phi$

ϕ

$\phi$

C'est assez bien, il y a une analogie avec l'apprentissage automatique contradictoire si vous plissez les yeux et en effet cela fonctionne pour tout réseau complémenté où vous avez une sorte de solveur

Samuel Schlesinger