Seja uma fórmula CNF satisfatória com variáveis e cláusulas . Seja o espaço de solução de .m S F 1 F 1
Considere o problema de determinar, dada a , outra Fórmula CNF com o mesmo conjunto de variáveis que , com (o mesmo espaço de solução que ), mas com o mínimo de cláusulas possível (a única O objetivo é minimizar o número de cláusulas, portanto, quantos literais cada cláusula pode ter não é relevante).F 2 F 1 S F 2 = S F 1 F 1
Questão
Alguém já investigou esse problema? Existem resultados na literatura sobre isso?
Como exemplo, considere a seguinte fórmula CNF (cada linha é uma cláusula):
x 2 ∨ x 3 ∨ x 4 ¬ x 1 ∨ x 2 ∨ x 4 ¬ x 1 ∨ x 2 ∨ ¬ x 3 ¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2 ∨ ¬ x 5
e a seguinte fórmula :
x 2 ∨ x 3 ∨ x 4 ¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2
ambos têm o mesmo espaço de solução, mas enquanto possui cláusulas, possui apenas . 6 F 2 4
Por fim, considere a seguinte fórmula :
¬ x 1 ∨ x 3 ∨ x 5 ¬ x 1 ∨ x 2
O espaço da solução é novamente o mesmo, mas com apenas cláusulas.
fonte
Respostas:
O problema de determinar se existe uma fórmula CNF equivalente com no máximo um determinado número de literais é -complete. A versão que minimiza o número de cláusulas está dentro de um fator de do tamanho da fórmula, em que é o número de variáveis. Veja a seção 6 de: n nΠp2 n n
Um resultado recente mostra que a computação de um limite inferior específico para o tamanho da fórmula CNF equivalente mais curta (medida pelo número de cláusulas, conforme você especificar) é NP-complete. Este artigo também afirma que seu problema de minimizar o número de cláusulas também é , citando o artigo de Umans acima, embora o motivo a seguir não seja imediatamente óbvio para mim.Πp2
fonte
O problema de minimização do circuito é intratável (veja os comentários abaixo). Também acho que você pode estar interessado na técnica que alguns solucionadores de SAT aplicam (pelo menos até certo ponto) que é chamada de pré-processamento de SAT. Por exemplo, o conhecido solucionador MiniSAT usa um minimizador de CNF SatELite para pré-processar uma instância. O Google Scholar fornece muitos resultados para o "pré-processamento por satélite" também.
fonte
a principal solução std / conhecida para minimização de CNF no EE é o algoritmo Quine-McCluskey, com muitas implementações, algumas de domínio público. no entanto, meu entendimento é que (não mencionado no artigo atual da wikipedia) mais reverte para heurísticas e algoritmos gananciosos para encontrar soluções especialmente para fórmulas grandes, ou seja, elas não precisam. encontre a solução ideal esp. para grandes instâncias de entrada.
Quine-MCluskey é uma generalização do trabalho com mapas de Karnough cujos diagramas podem ser bem-sucedidos para pequenas instâncias.
e observe que pode haver várias soluções ótimas em termos de fórmulas equivalentes com o mesmo tamanho de cláusula (mínimo), isso será apontado em uma boa referência sobre o assunto. encontrar o mínimo parece reduzir a lista de todos os principais implicados, o que pode envolver uma explosão exponencial maciça na memória / "espaço" em comparação com o tamanho da fórmula original.
fonte