Algorithme de vérification de la satisfaction
-
29-09-2020 - |
Question
Pour prouver que SAT est dans NP, j'ai besoin de proposer un temps de polynôme verfier (un algorithme).Le théorème de Levin Cooks utilise une machine à troubles non déterministe, mais ce n'est pas ce que je cherche.
L'idée de l'algorithme pourrait être que nous mettons dans les valeurs et calculez la réponse.Ensuite, nous vérifions si la réponse est 1 ou non.Cependant, je suis incapable de comprendre comment je pourrais écrire un pseudocode pour la partie "Mettre en valeur", puis montrer qu'il est polynôme à coup sûr.
if x = 1:
accept
else:
reject
Cela pourrait être dans O (1).Mais qu'en est-il de la partie restante?
La solution
Voici comment je le ferais:
algo: Vérificateur pour le problème DNF-SAT donné comme une éventuelle de fermetures et une possible cartographie des littéraux à Booleans
Entrée:
Tableau de fermetures: [ $ C_1 $ , $ C_2 $ , ..., $ C_M $ ]
où $ C_J \ sous -teteq \ {x_1, ..., x_n, \ negn x_1, ... \ neion x_n \} $
(Certificat) Array $ M $ où $ m_i $ est la valeur booléenne de littéral $ x_i $
Sortie: vrai ou faux
for $i = 1$ to $m$:
value = true
for literal in $C_i$:
if literal == $x_i$:
value = value or $M[i]$:
else if literal == $\neg x_i$:
value = value or (not $M[i]$)
if not value:
return false
return true
Remarque: la notation mathématique est indentée et couramment utilisée dans la pseudocode tristement CS Stackexchange ne le supporte pas