La fórmula proposicional en DNF se puede decidir en tiempo polinomial?

Question

Para una fórmula proposicional F en DNF, uno puede decidir en el tiempo polinomial, si la fórmula es satisfactoria: simplemente camine por todas las subformeras (L_1 y ... y L_K) y verifique, donde no tiene un par complementario de literales. La fórmula F es satisfactoria si existe tal subformula.

¿Es correcto mi enfoque arriba?

En caso afirmativo, me pregunto por qué todos los solucionadores SAT modernos obtienen un CNF como formato de entrada, y no solo use DNF.

Answer 1

La conversión de CNF a DNF puede tener un costo exponencial. Por ejemplo, $ (a_1 lor b_1) land cdots land (a_n lor b_n) $ se expande a $ 2^n $ muchos términos. A medida que comenta, para DNF Satisfiability es fácil, es la falsiabilidad lo que es difícil. Si el problema es trivial, no lo ingresa a un solucionador SAT, y es por eso que los solucionadores SAT aceptan CNF en lugar de DNF.

Si cree que P es diferente de NP, entonces esto implica que no hay una forma de tiempo polinómico de convertir la satisfilidad de CNF en satisfacción de DNF, ya que el primero es completado NP mientras que el segundo está en P.