Uma fórmula CNF monótona com m termos em n variáveis ( ) é uma fórmula da forma , em que cada é um OR de algum subconjunto das variáveis e varia de a . f ( x 1 , … , x n ) = ⋀ C i C i x 1 , … , x n i 1 m
Por exemplo, é uma fórmula CNF monótona com 2 termos em 4 variáveis.
Estou procurando a fórmula mais curta (não necessariamente monótona, não necessariamente CNF, qualquer fórmula serve!) No mesmo conjunto de variáveis que representa a mesma função que uma fórmula CNF monótona específica em n variáveis com n termos. (Observe que o número de termos e variáveis é o mesmo.)
Uma maneira óbvia de construir uma fórmula é expandir a definição de CNF fornecida, o que nos dará uma fórmula de tamanho . (Vamos definir o tamanho de uma fórmula como o comprimento da fórmula quando ela é escrita como uma string.) Quero saber se essa é a construção geral mais eficiente ou se, para cada CNF monotônico de n termos, existe uma fórmula do tamanho .o ( n 2 )
Eu só quero saber se isso é possível, não estou realmente interessado em um algoritmo. Se isso não for possível, uma função que serve como um contra-exemplo seria ótima. Ponteiros para onde eu posso encontrar uma resposta na literatura também são apreciados.
EDIT: Estou adicionando um exemplo para tornar a coisa mais clara.
Digamos que a fórmula de entrada seja . Esta é uma fórmula monótona de CNF. Uma fórmula mais curta que representa a mesma função é a seguinte: .x 1 ∨ ( x 2 ∧ x 3
fonte
Considere que, para qualquer CNF, você pode calcular o conjunto de implicados primos (dos quais qualquer mínimo deve ser um subconjunto), executando o fechamento sob resolução e aplicando a eliminação da subsunção.
No entanto, no caso de qualquer CNF monótono , o fechamento da resolução de é (como não existem literais negativos, não há resolução possível). Portanto, o CNF mínimo é o conjunto de primos implicados, que é precisamente a fórmula que você já possui.F FF F F
Claro, suponho que você não queira introduzir novas variáveis.
Se você quiser garantir que você tenha alguma fórmula que tenha termos, como você sugere, a única maneira de conseguir isso é expandir algumas das cláusulas adicionando variáveis ausentes. Qualquer CNF deve ter o mesmo número de literais (a medida tamanho que você sugere que eu acredito) para um fixo e .f nn f n
fonte