Une formule CNF monotone avec m termes sur n variables ( ) est une formule de la forme , où chaque est un OU d'un sous-ensemble du les variables et vont de à .C i x 1 , … , x n i 1 m
Par exemple, est une formule CNF monotone avec 2 termes sur 4 variables.
Je recherche la formule la plus courte (pas nécessairement monotone, pas nécessairement CNF, n'importe quelle formule fera l'affaire!) Sur le même ensemble de variables qui représente la même fonction qu'une formule CNF monotone donnée sur n variables avec n termes. (Notez que le nombre de termes et de variables est le même.)
Une façon évidente de construire une formule est d'élargir la définition CNF donnée, ce qui nous donnera une formule de taille . (Définissons la taille d'une formule comme étant la longueur de la formule lorsqu'elle est écrite sous forme de chaîne.) Je veux savoir si c'est la construction générale la plus efficace ou si pour chaque CNF monotone à n termes, il existe une formule de taille .o ( n 2 )
Je veux juste savoir si c'est possible, je ne suis pas vraiment intéressé par un algorithme. Si ce n'est pas possible, une fonction qui sert de contre-exemple serait formidable. Les pointeurs vers lesquels je peux trouver une réponse dans la littérature sont également appréciés.
EDIT: J'ajoute un exemple pour rendre les choses plus claires.
Supposons que la formule d'entrée soit . Il s'agit d'une formule CNF monotone. Une formule plus courte qui représente la même fonction est la suivante: .x 1 ∨ ( x 2 ∧ x 3 ∧ … ∧ x n )
la source
Considérez que pour tout CNF, vous pouvez calculer l'ensemble des principaux implicites (dont tout minimum doit être un sous-ensemble) en prenant la fermeture sous résolution et en appliquant l'élimination de la subsomption.
Bien sûr, je suppose que vous ne voulez pas introduire de nouvelles variables.
la source