Por que o CNF é usado para SAT e não DNF?

Não entendo muito bem por que quase todos os solucionadores de SAT usam CNF em vez de DNF. Parece-me que resolver o SAT é mais fácil usando DNF. Afinal, você só precisa verificar o conjunto de implicantes e verificar se um deles não contém uma variável e sua negação. Para a CNF, não existe um procedimento simples como este.

A redução do livro didático de SAT para 3SAT, devido a Karp, transforma uma fórmula booleana arbitrária em uma fórmula booleana CNF "equivalente" de tamanho polinomial , de modo que seja satisfatório se e somente se for satisfatório. (Estritamente falando, essas duas fórmulas não são equivalentes, porque possui variáveis ​​adicionais, mas o valor de na verdade não depende dessas novas variáveis.)Φ $\Phi$$\Phi'$ Φ ' Φ ' Φ $\Phi$$\Phi'$$\Phi'$$\Phi'$

Nenhuma redução semelhante de fórmulas booleanas arbitrárias para fórmulas DNF é conhecida; todas as transformações conhecidas aumentam exponencialmente o tamanho da fórmula. Além disso, a menos que P = NP, essa redução não seja possível!

A maioria das coisas importantes foi dita, mas eu gostaria de enfatizar alguns pontos.

1. a satisfação de uma fórmula DNF é P
2. satisfação de uma fórmula CNF é NP
3. testar se uma fórmula CNF é uma tautologia é P
4. testar se uma fórmula DNF é uma tautologia é coNP
5. negar DNF produz CNF e vice-versa

Portanto, os solucionadores de SAT usam CNF porque têm como alvo a satisfação e qualquer fórmula pode ser convertida em CNF, preservando a satisfação em tempo linear.

Os solucionadores de SAT não "usam" a CNF - eles (frequentemente) recebem a CNF como insumo e fazem o possível para resolver a CNF que recebem. Como sua pergunta ressalta, a representação é tudo - é muito mais fácil saber se um DNF é satisfatório do que um CNF do mesmo tamanho.

Isso leva à questão de por que os solucionadores de SAT não podem simplesmente transformar seu CNF em DNF e resolver o DNF resultante, e tentar este é um bom exercício para entender as questões de representação.

7 ^th setembro 2013: Além disso resposta acrescentou, verificação inferior da página

---

Basicamente, uma fórmula DNF é uma disjunção das cláusulas , em que cada cláusula é uma conjunção de literais. Vamos chamar uma cláusula conflitante se e somente se ela contiver um literal e sua negação . É fácil ver que cada cláusula não conflitante apenas codifica soluções da fórmula. Portanto, todo o DNF é apenas uma enumeração de soluções. Uma fórmula pode ter muitas soluções exponencialmente, portanto, a fórmula DNF correspondente pode ter muitas cláusulas exponencialmente. Tente converter esta fórmula CNF:c i = l i , 1 ∧ . . . ∧ l i , k c i$c_1 \lor ... \lor c_m$$c_i = l_{i,1} \land ... \land l_{i,k}$$c_i$$l$$\lnot l$$2^{n-k}$

$l_1 \lor l_2 \lor l_3 \lor l_4$

$l_5 \lor l_6 \lor l_7 \lor l_8$

$l_9 \lor l_{10} \lor l_{11} \lor l_{12}$

$l_{13} \lor l_{14} \lor l_{15} \lor l_{16}$

$l_{17} \lor l_{18} \lor l_{19} \lor l_{20}$

à sua fórmula DNF correspondente: você receberá muitas cláusulas. Em uma palavra: CNF é compacto, enquanto DNF não; CNF está implícito, enquanto DNF é explícito.

O seguinte problema é NP-complete: dada uma instância DNF, existe uma atribuição de variáveis ​​que falsifica todas as cláusulas?

Acabei de perceber mais uma coisa, que espero merecer uma resposta separada. A presunção da pergunta não é inteiramente verdadeira. Um diagrama de decisão binária (BDD) pode ser visto como uma representação compacta / refinada do DNF. Houve alguns solucionadores SAT usando BDDs, mas acredito que eles não aparecem mais.

Há um belo artigo de Darwiche e Marquis estudando diferentes propriedades de várias representações de funções booleanas.

Essa resposta adicional é um feedback do comentário do dividebyzero à minha resposta anterior.

Como o dividebyzero diz, certamente é verdade que CNF e DNF são dois lados da mesma moeda.

Quando você precisa encontrar uma tarefa satisfatória, o DNF é explícito, pois mostra manifestamente suas tarefas satisfatórias (a DNF Satisfability pertence a ), enquanto a CNF está implícita à medida que envolve e vira para ocultar suas tarefas satisfatórias dos seus olhos ( CNF Satisfability é ). Não conhecemos nenhum procedimento que seja capaz de desembrulhar e desenrolar qualquer fórmula CNF em alguma fórmula DNF equisatisfatória que não seja exponencialmente dimensionada. Esse foi o ponto da minha resposta anterior (cujo exemplo pretendia mostrar a explosão exponencial, embora, sem dúvida, esse exemplo não tenha sido a melhor escolha possível).N P - c o m p l e t $\mathbf{P}$$\mathbf{NP-complete}$

Por outro lado, quando você precisa encontrar uma atribuição falsificada, o CNF é explícito, pois mostra manifestamente suas atribuições falsas (a falsificação de CNF pertence a ), enquanto o DNF está implícito à medida que envolve e tenta ocultar suas atribuições falsas do seu olhos (a falsificação de DNF é ). Não conhecemos nenhum procedimento que seja capaz de desembrulhar e desenrolar qualquer fórmula DNF em alguma fórmula CNF equifalsificável que não seja exponencialmente dimensionada.N P - c o m p l e t $\mathbf{P}$$\mathbf{NP-complete}$

Em uma extremidade, temos contradições, ou seja, fórmulas insatisfatórias. Na extremidade oposta, temos Tautologias, ou seja, fórmulas não falsificáveis. No meio, temos fórmulas que são satisfatórias e falsificáveis.

Em qualquer fórmula CNF com variáveis, toda cláusula de comprimento codifica manifestamente atribuições falsas.k 2 n - $n$$k$$2^{n-k}$

Em qualquer fórmula DNF com variáveis, todo termo de comprimento codifica manifestamente atribuições satisfatórias.k 2 n - $n$$k$$2^{n-k}$

Uma fórmula CNF sem cláusulas é uma Tautologia, porque não possui nenhuma atribuição falsificada. Uma fórmula CNF que contém a cláusula vazia (que inclui todas as outras cláusulas) é uma contradição, porque a cláusula vazia (que tem ) indica que todas as atribuições estão falsificando. Qualquer outra fórmula CNF é uma contradição ou uma dessas fórmulas no meio (e é distinguir entre esses dois casos).2 n N P - c o m p L e T $k = 0$$2^n$$\mathbf{NP-complete}$

Uma fórmula DNF sem termos é uma contradição, porque não possui nenhuma atribuição satisfatória. Uma fórmula DNF que contém o termo vazio (que inclui todos os outros termos) é uma Tautologia, porque o termo vazio (que tem ) indica que todas as atribuições são satisfatórias. Qualquer outra fórmula DNF é uma Tautologia ou uma dessas fórmulas no meio (e é distinguir entre esses dois casos).2 n N P - c o m p L e T $k = 0$$2^n$$\mathbf{NP-complete}$

Com uma fórmula CNF, distinguir entre os dois casos acima significa ser capaz de dizer se todas as atribuições falsas coletivamente trazidas pela presença de cláusulas se sobrepõem de maneira a cobrir todas as atribuições (nesse caso, a fórmula é uma contradição) caso contrário, é satisfatório).$2^n$

Com uma fórmula DNF, distinguir entre os dois casos acima significa ser capaz de dizer se todas as tarefas satisfatórias coletivamente trazidas pela presença de termos se sobrepõem de forma a cobrir todas as tarefas (nesse caso, a fórmula é uma Tautologia , caso contrário, é falsificável).$2^n$

Sob essa luz, fica mais claro por que CNF Satisfability e DNF Falsifiability são equivalentes em termos de dureza computacional. Porque eles realmente são o mesmo problema, pois a tarefa subjacente é exatamente a mesma: dizer se a união de vários conjuntos é igual ao espaço de todas as possibilidades . Tal tarefa nos leva ao campo mais amplo da contagem, que é, na minha humilde opinião, um daqueles caminhos a serem fervorosamente explorados, a fim de esperar um progresso não negligenciável sobre esses problemas (duvido que mais pesquisas sobre solucionadores baseados em resolução pode eventualmente trazer avanços teóricos inovadores, enquanto certamente continua a trazer avanços práticos surpreendentes).

A dificuldade de tal tarefa é que esses conjuntos se sobrepõem descontroladamente, de maneira inclusão-exclusão.

A presença de tal sobreposição é precisamente onde reside a dureza da contagem. Além disso, o fato de permitirmos a sobreposição desses conjuntos é o próprio motivo que nos permite ter fórmulas compactas cujo espaço de solução é, no entanto, exponencialmente grande.

Decidi transformar todas essas respostas neste tópico (especialmente a resposta de Giorgio Camerani) em uma boa tabela para que a dualidade seja visível de uma só vez:

$$\begin{array} {r|c|c} &\text{DNF} & \text{CNF} \\\hline \text{tautology/unfalsifiability} & \textsf{coNP-complete} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} \\\hline \text{satisfiability} & \textsf{P} \; \tiny\text{(sat. assignments are explicit)} & \textsf{NP-complete}\\\hline \text{falsifiability} & \textsf{NP-complete} & \textsf{P} \; \tiny\text{(fals. assignments are explicit)} \\\hline \text{unsatisfiability} & \textsf{P} \; \tiny\text{(each clause has a pair of P and ¬P)} & \textsf{coNP-complete} \\\hline \tiny{\text{conversion to normal form, retaining equivalence}} & (*) & (*) \\\hline \tiny{\text{conversion to normal form, retaining satisfiability}} & (**) & \textsf{FP} \\\hline \tiny{\text{conversion to normal form, retaining falsiability}} & \textsf{FP} & (**) \end{array}$$

$(*)$

$(**)$$(*)$$\mathrm{FP}^{\mathrm{NP}[1]}$

Resposta mais curta à pergunta: mostrar satisfação (resolvendo SAT) via DNF só pode ser feito em tempo exponencial, de acordo com a tabela acima.