Affectation pour rendre la formule insatisfaisante

8

Imaginons que nous ayons une formule satisfaisante Le problème à résoudre est "Y a-t-il une affectation pour les variables qui fera F insatisfaisant? ". Une façon de résoudre est de trouver toutes les solutions pour F en termes de variables et si le nombre est < , la solution manquante sera la réponse, mais la complexité de cet algorithme est énorme, si le nombre de ces affectations est faible.F(UNE0,UNE1,...UNEk,S0,...,Sn)(S0,...,Sn)S0,...,Sn2n

Mes questions sont:

  • Existe-t-il un moyen de résoudre le problème avec moins d'appels au solveur SAT?
  • Est-ce un problème bien connu en théorie (que dois-je google pour en savoir plus)?
Grigor Aghanyan
la source
1
"ce qui rendra F insatisfaisant" - cela n'a pas de sens. Voulez-vous simplement dire "ne satisfait pas F"? Ensuite, vous parlez du problème TAUTOLOGIE (resp. C'est le complément).
Raphael
Ignorant le fait que la question n'a pas de sens, je pense qu'essayer de trouver une solution à pourrait être ce que vous recherchez. ¬F(UNE0,UNE1,,UNEk,S0,,Sn)
Dave Clarke
Peut-être que je n'étais pas clair. Après avoir appliqué les affectations pour nous aurons une autre formule et celle-ci doit être insatisfaisante. (S0,...,Sn)g(UNE0,...,UNEk)
Grigor Aghanyan

Réponses:

6

Votre problème est le problème canonique -complet: En tant que tel, il est considéré comme plus difficile que SAT (qui est ). Le résoudre avec quelques appels SAT-oracle revient à résoudre SAT lui-même efficacement (la question P vs. NP), bien qu'il puisse être que tandis que , donc dans un certain sens, il est plus d'espoir pour votre problème que pour SAT lui-même.Σ2P

SUNE¬F(UNE,S).
Σ1PΣ2P=Σ1PPNP
Yuval Filmus
la source
Exactement. Merci pour la réponse. Donc, la solution avec appels de solveur n'est "pas une mauvaise solution" pour cela? Un lien pour des articles sur ce problème m'aidera beaucoup. 2n
Grigor Aghanyan
Pratiquement parlant, il pourrait y avoir des heuristiques qui fonctionnent bien pour certains problèmes, mais je n'en connais aucun. La hiérarchie polynomiale (qui contient ) devrait être couverte dans tout manuel sur la complexité de calcul. Σ2P
Yuval Filmus
4

C'est un problème bien connu: c'est le problème 2QBF. Malheureusement, c'est beaucoup plus difficile que SAT. Il existe des solveurs QBF. Vous pouvez essayer de trouver un solveur QBF (ou, mieux encore, un solveur 2QBF) et voir s'il peut résoudre votre formule. Cependant, les solveurs QBF n'évoluent pas aussi bien que les solveurs SAT; QBF est beaucoup plus difficile que SAT.

Voir https://cstheory.stackexchange.com/q/11022/5038 et http://www.qbflib.org/ pour quelques ressources qui pourraient être utiles.

DW
la source