algorithme de vérification de la satisfiabilité

Question

Afin de prouver que SAT est dans NP, je dois trouver un verfier temporel polynomial (un algorithme). Le théorème de Cooks Levin utilise une machine de Turing non déterministe mais ce n'est pas ce que je recherche.

L'idée de l'algorithme pourrait être que nous introduisions les valeurs et calculions 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 psuedocode pour la partie «mettre en valeurs» et montrer ensuite que c'est un polynôme à coup sûr.

if x = 1:
 accept
else:
 reject

Cela pourrait être en O (1). Mais qu'en est-il de la partie restante?

Answer 1

Voici comment je le ferais:

Algo: Vérificateur pour le problème DNF-SAT donné sous forme de tableau de fermetures et d'un possible mappage de littéraux en booléens
Entrée:
Tableau de fermetures: [$C_1$,$C_2$, ...,$C_m$]
où$C_j \subseteq \{x_1,...,x_n,\neg x_1, ... \neg x_n\}$
(Certificat) Tableau $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 le pseudocode, malheureusement cs stackexchange ne la prend pas en charge