Algoritmo para verificar la satisfacción

Question

Para demostrar que SAT está en NP, necesito crear un verfier de tiempo polinomial (un algoritmo).El teorema de los cocineros Levin utiliza una máquina de Turing no determinista, pero eso no es lo que estoy buscando.

La idea del algoritmo podría ser que ponemos en los valores y calculamos la respuesta.Luego, verificamos si la respuesta es 1 o no.Sin embargo, no puedo entender cómo pude escribir un PSUEDOCODE para la parte 'Poner en valores' y luego demostrar que es polinomio seguro.

if x = 1:
 accept
else:
 reject

Esto podría estar en O (1).Pero ¿qué pasa con la parte restante?

Answer 1

Aquí es cómo lo haría:

Algo: verificador para el problema de DNF-SAT dado como una matriz de cierres y un posible mapeo de literales a Booleans
entrada:
Arreglo de cierres: [ $ c_1 $ , $ c_2 $ , ..., $ c_m $ ]

donde $ c_j \ subestesteq \ {x_1, ..., x_n, \ neg x_1, ... \ neg x_n \} $
(Certificado) Array $ m $ donde $ M_I $ es el valor booleano de literal $ X_I $
salida: verdadero o falso

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 

NOTA: La notación matemática está sangrada y se usa comúnmente en Pseudocódigo, tristemente CS StackExchange, no lo admite