Formule CNF équivalente la plus courte

18

Soit une formule CNF satisfaisante avec n variables et m clauses. Soit S F 1 l'espace de solution de F 1 .F1nmSF1F1

Considérons le problème de déterminer, étant donné , une autre formule CNF F 2 avec le même ensemble de variables que F 1 , avec S F 2 = S F 1 (même espace de solution que F 1 ), mais avec le moins de clauses possible ( le seul objectif est de minimiser le nombre de clauses, donc le nombre de littéraux que chaque clause peut avoir n'est pas pertinent).F1F2F1SF2=SF1F1

Question

Quelqu'un a-t-il déjà étudié ce problème? Y a-t-il des résultats dans la littérature à ce sujet?

À titre d'exemple, considérons la formule CNF (chaque ligne est une clause): 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

et la formule : F2

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

les deux ont le même espace de solution, mais alors que a 6 clauses, F 2 n'en a que 4 . F16F24

Enfin, considérons la formule : F3

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

L'espace de solution est à nouveau le même, mais avec seulement clauses.3

Giorgio Camerani
la source
2
@tsuyoshi Je pense qu'il veut obtenir une formule cnf composée d'un nombre minimum de clauses avec le même espace de solution
Tayfun Pay
1
@TsuyoshiIto: Oui, je veux minimiser le nombre de clauses. Je ne pose aucune restriction sur le nombre de littéraux que chaque clause peut avoir.
Giorgio Camerani
1
Pour toute définition raisonnable de "petit", le problème est NP-difficile. Une formule CNF est satisfiable si et seulement si elle n'est pas équivalente à la formule "False", qui a zéro clauses.
Jeffε
1
La section 6 de citeseerx.ist.psu.edu/viewdoc/… mentionne que le problème de déterminer s'il existe une formule CNF équivalente avec au plus un nombre donné de littéraux est complet. Je ne suis pas sûr de comprendre pourquoi votre version minimisant le nombre de clauses est intéressante, car c'est dans un facteur n de la taille de la formule, où n est le nombre de variables. Π2pnn
András Salamon du
1
En outre, un autre résultat récent est pertinent: dx.doi.org/10.1016/j.dam.2011.05.013
András Salamon

Réponses:

10

Le problème de déterminer s'il existe une formule CNF équivalente avec au plus un nombre donné de littéraux est -complet. La version minimisant le nombre de clauses est dans un facteur de n de la taille de la formule, où n est le nombre de variables. Voir section 6 de:Π2pnn

Un résultat récent montre que le calcul d'une borne inférieure particulière pour la taille de la formule CNF équivalente la plus courte (mesurée par le nombre de clauses, comme vous le spécifiez) est NP-complet. Ce document indique également que votre problème de minimiser le nombre de clauses est -complete ainsi, en citant le document Umans ci - dessus, bien pourquoi ce qui suit est pas immédiatement évident pour moi.Π2p

  • Ondřej Čepek, Petr Kučera et Petr Savický, Fonctions booléennes avec un certificat simple pour la complexité CNF , DAM 160 (4–5), 365–382, 2012. doi: 10.1016 / j.dam.2011.05.013
András Salamon
la source
8

Le problème de minalisation du circuit est insoluble (voir les commentaires ci-dessous). De plus, ce qui pourrait vous intéresser, c'est la technique que certains solveurs SAT appliquent (au moins dans une certaine mesure) qui est appelée prétraitement SAT. Par exemple, le solveur MiniSAT bien connu utilise un minimiseur CNF SatELite pour prétraiter une instance. Google Scholar donne également de nombreux résultats pour le "prétraitement sat".

Juho
la source
2
Je pensais que Buchfuhrer et Umans en 2008 avaient réglé le problème de minimisation des circuits étant -complet, sous Turing réductions? Π2p
András Salamon
1
Umans a déjà montré en 1998 que trouver une formule CNF équivalente minimale est -hard ( dx.doi.org/10.1006/jcss.2001.1775 ). Le document mentionné par András le généralise aux circuits de plus grande profondeur. Σ2P
Jan Johannsen
6

la principale solution std / connue pour la minimisation CNF dans EE est l' algorithme Quine-McCluskey qui existe de nombreuses implémentations, certaines du domaine public. cependant, je crois comprendre que (non mentionné dans l'article actuel de wikipedia) la plupart reviennent à l'heuristique et aux algorithmes gourmands pour trouver des solutions, en particulier pour les grandes formules, c'est-à-dire qu'elles ne sont pas nca. trouver la solution optimale esp. pour les grandes instances d'entrée.

Quine-MCluskey est une généralisation du travail avec les cartes de Karnough dont les diagrammes peuvent réussir pour de petites instances.

et notez qu'il peut y avoir plusieurs solutions optimales en termes de formules équivalentes avec la même taille de clause (minimale), cela sera souligné dans une bonne référence sur le subj. trouver le minimum se résume apparemment à lister tous les principaux implicits qui peuvent impliquer une explosion exponentielle massive dans la mémoire / "espace" par rapport à la taille de la formule originale.

vzn
la source