Fórmula CNF equivalente mais curta

18

Seja uma fórmula CNF satisfatória com variáveis ​​e cláusulas . Seja o espaço de solução de .F1m S F 1 F 1nmSF1F1

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 1F1F2F1SF2=SF1F1

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): F1

x 2x 3x 4 ¬ x 1x 2x 4 ¬ x 1x 2¬ x 3 ¬ x 1x 3x 5 ¬ x 1x 2¬ x 5x1x2x3
x2x3x4
¬x1x2x4
¬x1x2¬x3
¬x1x3x5
¬x1x2¬x5

e a seguinte fórmula : F2

x 2x 3x 4 ¬ x 1x 3x 5 ¬ x 1x 2x1x2x3
x2x3x4
¬x1x3x5
¬x1x2

ambos têm o mesmo espaço de solução, mas enquanto possui cláusulas, possui apenas . 6 F 2 4F16F24

Por fim, considere a seguinte fórmula : F3

¬ x 1x 3x 5 ¬ x 1x 2x2x3
¬x1x3x5
¬x1x2

O espaço da solução é novamente o mesmo, mas com apenas cláusulas.3

Giorgio Camerani
fonte
2
@tsuyoshi Acho que ele quer para obter uma fórmula cnf que é composta de número mínimo de cláusulas com o mesmo espaço de solução
Tayfun Pay
1
@TsuyoshiIto: Sim, quero minimizar o número de cláusulas. Não coloco nenhuma restrição no número de literais que cada cláusula pode ter.
Giorgio camerani
1
Para qualquer definição razoável de "pequeno", o problema é NP-difícil. Uma fórmula CNF é satisfatória se, e somente se, não for equivalente à fórmula "False", que possui zero cláusulas.
Jeffε
1
A seção 6 de citeseerx.ist.psu.edu/viewdoc/… menciona que o problema de determinar se existe uma fórmula CNF equivalente com no máximo um determinado número de literais é -complete. Não sei ao certo por que a sua versão que minimiza o número de cláusulas é interessante, pois isso está dentro de um fator do tamanho da fórmula, em que é o número de variáveis. n nΠ2pnn
András Salamon
1
Além disso, outro resultado recente é relevante: dx.doi.org/10.1016/j.dam.2011.05.013
András Salamon

Respostas:

10

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Π2pnn

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.Π2p

  • Ondřej Čepek, Petr Kučera e Petr Savický, funções booleanas com um certificado simples para complexidade da CNF , DAM 160 (4-5), 365-382, 2012. doi: 10.1016 / j.dam.2011.05.013
András Salamon
fonte
8

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.

Juho
fonte
2
Π2p
1
Σ2P
6

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.

vzn
fonte