Fórmulas mínimas insatisfatórias de 3-CNF

Atualmente, estou interessado em obter (ou construir) e estudar fórmulas de 3-CNF insatisfatórias e de tamanho mínimo. Ou seja, eles devem consistir no menor número possível de cláusulas (m = 8) e no menor número possível de variáveis distintas (n = 4 ou mais), de modo que a remoção de pelo menos uma cláusula torne a fórmula satisfatória.

Mais formalmente, qualquer fórmula 3-CNF F qualificada deve atender às seguintes condições:

F é insatisfatório
F tem uma quantidade mínima (4+) de variáveis distintas (ou sua negação)
F tem uma quantidade mínima de cláusulas (8+)
todo subconjunto apropriado de F é satisfatório (permitindo a remoção de qualquer cláusula ou cláusula arbitrária).
F não possui 2 cláusulas redutíveis a uma cláusula 2-CNF, por exemplo, (i, j, k) & (i, j, ~k)NÃO é permitido (elas se reduzem a (i,j))

Por exemplo, com n = 4, existem muitas fórmulas mínimas de 3-CNF de 8 cláusulas que são insatisfatórias. Por um lado, olhando o hipercubo 4 e tentando cobri-lo com bordas (2 faces), é possível construir a seguinte fórmula insatisfatória:

1. (~A,  B,  D)
2. (~B,  C,  D)
3. ( A, ~C   D)
4. ( A, ~B, ~D)
5. ( B, ~C, ~D)
6. (~A,  C, ~D)
7. ( A,  B,  C)
8. (~A, ~B, ~C)

Isso se qualifica como uma fórmula 3-CNF mínima insatisfatória porque:

É insatisfatório:
- As cláusulas 1-3 são equivalentes a: D or A=B=C
- As cláusulas 4-6 são equivalentes a: ~D or A=B=C
- Elas implicam A=B=C, mas pelas cláusulas 7 e 8, isso é uma contradição.
Existem apenas 4 variáveis distintas.
Existem apenas 8 cláusulas.
A remoção de qualquer cláusula a torna satisfatória.
Nenhuma cláusula 2 é 'redutível' a uma cláusula 2-CNF.

Então, acho que minhas perguntas gerais aqui são, em ordem de importância para mim:

Quais são algumas outras pequenas fórmulas mínimas que atendem às condições acima? (ou seja, 4,5,6 variáveis e 8,9,10 cláusulas)
Existe algum tipo de banco de dados ou "atlas" dessas fórmulas mínimas?
Quais algoritmos não aleatórios existem para construí-los totalmente, se houver?
Quais são algumas idéias sobre as características dessas fórmulas? Eles podem ser contados ou estimados, considerando n (# variáveis) e m (# cláusulas)?

Agradeço desde já pelas suas respostas. Congratulo-me com qualquer resposta ou comentário.

cc.complexity-theory sat MAF
fonte

Cada cláusula 3-CNF desaprova 1/8 das possíveis soluções. Então, claramente, você sempre precisa de pelo menos 8 cláusulas ou mais se os conjuntos de soluções não permitidas se sobrepuserem. Desde a sua condição 5 proíbe conjuntos de soluções não permitidos não sobrepostas para n = 3, você precisa de mais de 8 cláusulas para este caso: nota que o seu exemplo não condição de obedecer 5.

András Salamon

Sim, você está correto em todos os pontos András. 8 cláusulas são um requisito mínimo para uma fórmula 3-CNF insatisfatória e, portanto, a condição 5 pode ser um pouco restritiva para meus propósitos em encontrar / construir fórmulas qualificadas. Sei que para n = 3, a condição 5 deve ser necessariamente violada, mas foi incluída apenas para fins ilustrativos. Estou estritamente interessado em qualificar fórmulas de tamanho n = 4 + (ou seja, 4 ou mais variáveis, mas não muitas mais). Talvez eu arranhe a condição 5.

MAF 08/09

Eu acho que o seu “exemplo” com n = 3 é mais confuso do que ilustrativo, porque (como András apontou em seu comentário) não é realmente um exemplo do que você está perguntando nesta pergunta. O exemplo com n = 4 é perfeitamente correto e ilustrativo. Por que você simplesmente não remove o exemplo com n = 3?

Tsuyoshi Ito

Bom ponto, Tsuyoshi. Feito.

MAF

{x}

$\{x\}$

{x^{'}}

$\{x'\}$

C

$C$

C \cup {v}

$C \cup \{v\}$

C \cup {v^{'}}

$C \cup \{v'\}$

v

$v$

Respostas:

$\lnot A \lor \lnot B \lor \lnot C$ $2$

$\lnot A \lor \lnot B \lor \lnot E$
$\lnot B \lor \lnot C \lor E$

$n=5$ $m=9$

$l_1 \lor l_2 \lor l_3$ $2$

$l_1 \lor l_2 \lor v$
$l_2 \lor l_3 \lor \lnot v$

$v$ $n$ $m$ $1$ $r=\frac{m}{n}$ $1$ $n$ $r=1$

Giorgio Camerani
fonte

Obrigado pela resposta, Walter. O procedimento que você descreve é muito útil, de fato, para gerar fórmulas mínimas ainda mais ligeiramente maiores de estrutura 'semelhante', ou seja, depois de ter um conjunto principal que você acha que possui propriedades interessantes.

MAF

@ MAF: De nada. Obrigado por postar uma pergunta tão interessante.

Giorgio Camerani

Acredito que a condição número 5 não é realmente mantida no seu exemplo e nunca pode ser mantida.
Que as seguintes cláusulas sejam equivalentes:

( p, q) = (~A,B,D)(A,~B,~D)

O que nos permitirá mapear as cláusulas de A, B, C e D para novas variáveis p, q, re es como a seguinte tabela de verdade:

A B C D | p q r s
-----------------
0 0 0 0 | 0 1 0 0
0 0 0 1 | 0 1 0 1
0 0 1 0 | 0 1 1 0
0 0 1 1 | 0 1 1 1
-----------------
0 1 0 0 | 1 0 0 0
0 1 0 1 | 0 0 0 0
0 1 1 0 | 1 0 0 1
0 1 1 1 | 0 0 0 1
-----------------
1 0 0 0 | 0 0 1 0
1 0 0 1 | 1 0 1 0
1 0 1 0 | 0 0 1 1
1 0 1 1 | 1 0 1 1
-----------------
1 1 0 0 | 1 1 0 0
1 1 0 1 | 1 1 0 1
1 1 1 0 | 1 1 1 0
1 1 1 1 | 1 1 1 1
-----------------

E agora podemos expressar as cláusulas de A, B, C e D em termos de p, q, re s:

1. (~A,  B,  D) = ( p, q,~r, s)( p, q,~r,~s)
2. (~B,  C,  D) = (~p, q, r, s)(~p,~q, r, s)
3. ( A, ~C   D) = ( p,~q,~r, s)(~p, q, r,~s)
4. ( A, ~B, ~D) = ( p, q, r, s)( p, q, r,~s)
5. ( B, ~C, ~D) = ( p,~q,~r,~s)(~p, q,~r,~s)
6. (~A,  C, ~D) = (~p, q,~r, s)(~p,~q, r,~s)
7. ( A,  B,  C) = ( p,~q, r, s)( p,~q, r,~s)
8. (~A, ~B, ~C) = (~p,~q,~r, s)(~p,~q,~r,~s)

Como todas as cláusulas são mostradas e associadas às cláusulas A, B, C e D. Então, podemos afirmar que as cláusulas p, q, re es podem ser reduzidas a:

( p, q, r)
( p, q,~r)
( p,~q, r)
( p,~q,~r)
(~p, q, r)
(~p, q,~r)
(~p,~q, r)
(~p,~q,~r)

O que obviamente viola a condição número 5.

O que quero ressaltar é que mesmo o exemplo não mostra explicitamente que existem 2 cláusulas que podem ser reduzidas a 2-CNF, mas implicitamente é has (por exemplo (~ A, B, D) e (A, ~ B, ~ D)), talvez você não consiga expressar o 2-CNF com as variáveis especificadas, mas quando introduzir um mapeamento diferente para o problema, poderá expressá-las.

Khazam Alhamdan
fonte