Problème P=NP résolu?
Bonjour,
Dans le problème 3-SAT,il y a 3 littéraux pour lesquels on effectue une opération "ou". Ces opérations "ou" se réunissent en regroupements auxquels on effectue une opération "et". Le problème consiste à chercher à l'aide d'un algorithme s'il est possible de satisfaire un résultat vrai pour une ou plusieurs combinaisons de variables. Ce problème est NP-Complet donc si le problème est P, le problème P=NP est résolu et P=NP.
Pour démontrer que le problème 3-SAT est P, nous allons voir les conditions qui empêchent la satisfaction du résultat.
Dans le cas d'une forme disjonctive,nous aurions:
f=(v(1) et non (v1)) ou (v(2) et non v(2)) ou (v(3) et non v(3)) avec v(n) les variables propositionnelles et f la fonction insatisfaisable.
La forme conjonctive est donnée par le logiciel de calcul formel (image ci-jointe).
On n'oublira pas de rayer les v(n) qui ne sont pas assez suffisamment présent et à simplifier l'expression en supprimant la redondance. En effet pour avoir une forme insatisfaisable, nous devons avoir toutes les combinaisons possibles de (v(1),v(2),v(3)). Nous éliminerons tous les v(n) qui ne satisfont pas la condition d'insatisfabilité.
Passons à l'algorithme:
Entrée:
regroupement[] (liste de regroupements des 3 littéraux comme v(1) ou v(2) ou v(3)
Initialisation:
i=0
tailleregroupements=0
tailleregroupements=taille(regroupement[])
compteur={0...0} de taille 3*tailleregroupements // Soit un compteur pour chaque littéral.
suppression=0
Début:
Supprimer les éléments présents plus de 2 fois dans regroupement[]
tailleregroupements=taille(regroupement[])
Tant Que Vrai
suppression=0
Pour i Allant de 1 à 3*tailleregroupements de 1 en 1:
compteur(i)=Nombre ("v(i)",regroupement())+Nombre("non v(i)",regroupement())-Nombre(("v(i)" et "non v(i)",regroupement())
//On compte le nombre de v(n)
Fin Pour
Pour i Allant de 1 à 3*tailleregroupements de 1 en 1:
Si compteur(i)<8 et taille(regroupement)!=0: // Soit 8,le nombre de combinaisons nécessaires.
Supprimer les regroupements contenant v(i) dans regroupement[]
suppression=1
Arrêter boucle
Fin Si
Fin Pour
Si suppression=0:
Arrêter boucle
Fin Si
Fin Tant Que
Si taille(regroupement[])=0:
Afficher "Le problème est satisfaisable."
Sinon:
Afficher "Le problème est insatisfaisable."
Fin Si
Fin du programme.
Je vous transmet mon algorithme python via un lien:ici.
Je l'ai testé, il fonctionne.
Je vous remercie pour vos commentaires et vous remercie d'avance pour vos commentaires sur la démonstration.
Dans le problème 3-SAT,il y a 3 littéraux pour lesquels on effectue une opération "ou". Ces opérations "ou" se réunissent en regroupements auxquels on effectue une opération "et". Le problème consiste à chercher à l'aide d'un algorithme s'il est possible de satisfaire un résultat vrai pour une ou plusieurs combinaisons de variables. Ce problème est NP-Complet donc si le problème est P, le problème P=NP est résolu et P=NP.
Pour démontrer que le problème 3-SAT est P, nous allons voir les conditions qui empêchent la satisfaction du résultat.
Dans le cas d'une forme disjonctive,nous aurions:
f=(v(1) et non (v1)) ou (v(2) et non v(2)) ou (v(3) et non v(3)) avec v(n) les variables propositionnelles et f la fonction insatisfaisable.
La forme conjonctive est donnée par le logiciel de calcul formel (image ci-jointe).
On n'oublira pas de rayer les v(n) qui ne sont pas assez suffisamment présent et à simplifier l'expression en supprimant la redondance. En effet pour avoir une forme insatisfaisable, nous devons avoir toutes les combinaisons possibles de (v(1),v(2),v(3)). Nous éliminerons tous les v(n) qui ne satisfont pas la condition d'insatisfabilité.
Passons à l'algorithme:
Entrée:
regroupement[] (liste de regroupements des 3 littéraux comme v(1) ou v(2) ou v(3)
Initialisation:
i=0
tailleregroupements=0
tailleregroupements=taille(regroupement[])
compteur={0...0} de taille 3*tailleregroupements // Soit un compteur pour chaque littéral.
suppression=0
Début:
Supprimer les éléments présents plus de 2 fois dans regroupement[]
tailleregroupements=taille(regroupement[])
Tant Que Vrai
suppression=0
Pour i Allant de 1 à 3*tailleregroupements de 1 en 1:
compteur(i)=Nombre ("v(i)",regroupement())+Nombre("non v(i)",regroupement())-Nombre(("v(i)" et "non v(i)",regroupement())
//On compte le nombre de v(n)
Fin Pour
Pour i Allant de 1 à 3*tailleregroupements de 1 en 1:
Si compteur(i)<8 et taille(regroupement)!=0: // Soit 8,le nombre de combinaisons nécessaires.
Supprimer les regroupements contenant v(i) dans regroupement[]
suppression=1
Arrêter boucle
Fin Si
Fin Pour
Si suppression=0:
Arrêter boucle
Fin Si
Fin Tant Que
Si taille(regroupement[])=0:
Afficher "Le problème est satisfaisable."
Sinon:
Afficher "Le problème est insatisfaisable."
Fin Si
Fin du programme.
Je vous transmet mon algorithme python via un lien:ici.
Je l'ai testé, il fonctionne.
Je vous remercie pour vos commentaires et vous remercie d'avance pour vos commentaires sur la démonstration.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Je ne sais pas si j'ai du retard mais le prix du millénaire est encore à remporter.Voir ici.
Ensuite, si ton algorithme passe par la forme normale disjonctive, ça ne marchera pas parce que la conversion "forme normale conjonctive" $\to$ "forme normale disjonctive" n'est a priori pas en temps polynomial. C'est d'ailleurs pour ça que la question de savoir si une formule donnée en forme normale disjonctive est une tautologie est un problème co-NP-complet.
Ensuite, et pour finir, un programme seul assez obscur ne sera pas une preuve de quoi que ce soit: il te manque la preuve qu'il est correct, et qu'il termine en temps polynomial, ce que tu n'as fait pour aucun des deux algorithmes que tu présentes.
Si un jour tu prouves $P=NP$ ou $P\neq NP$, il te faudra un peu plus de travail que deux lignes de code ;-) (dis-toi que si la preuve de P=NP était si simple, vu le nombre de personnes qui travaillent dessus, le temps depuis lequel ils travaillent dessus et l'argent qui est en jeu, quelqu'un l'aurait trouvée)
Le "nous aurions P(n)" signifie que pour avoir 3 littéraux dans la liste "regroupement[]", il faut avoir 3 groupes réunis par un opérateur "ou". S'il y a plus de 2 éléments réunis par les parenthèses dans les opérateurs "ou" ils n'auront pas d'impact sur les P(n) mais pas d'impact non plus sur l'autre forme car on n'en tiendra pas compte dans la forme développée, ce qui n'est pas empêché par l'algorithme. La conversion de forme se fait en temps polynomial car il s'agit d'une base de données fixe qui est d'ailleurs calquée sur ce que j'obtiens à partir du logiciel de calcul formel quelque soit le problème de 3-SAT. Il s'agit d'un algorithme de reconnaissance de littéraux et de regroupements. Quant au fait que P(n) la proposition soit insatisfaisable, cela est prévu car l'algorithme détecte l' insatisfaisabilté en affectant un bit à chaque condition d' insatisfaisabilité. J'ai modifié le sujet pour clarifier ma pensée et élargir mon programme à tous les cas possibles.
toujours d'après moi çà ne nécessite pas un truc non polynomiale pour ce faire et l'existence d'un tel groupe serait (au point ou j'en suis dans mes réflexions) une condition nécessaire et suffisante d'insatisfiabilité de la chose dont il est question
cordialement
juanita B
Vous êtes en train de me réconforter pour ma démonstration sur P=NP (et j'en suis très fier)même si mon algorithme n'est pas très bien rédigé.
Cependant,j'ai fait un algorithme en Python, qui lui est disponible et est rédigé sans bug.
De plus, il détaille l'algorithme que j'ai fait en "charabia".
Vous pouvez le tester et voir à quel point il fonctionne agréablement bien.
Sinon, j'explique pourquoi je teste les combinaisons:
Pour avoir une insatisfaisabilité, il faut avoir dans la forme disjonctive (v(n) et non(v(n)), ce qui en développant donne l'ensemble des combinaisons possibles (soit 8 pour le problème 3-sat). Si, dans la forme conjonctive du problème 3-sat, il y a un motif d' insatisfaisabilité, cela est suffisant à cause du "et" qui oblige la satisfaction de toutes les conditions pour la satisfaction du problème.
je me suis peut être trompée dans mon raisonnement (mais je pense pas) en tout les cas il semblerait que l'on soit arrivé à la même conclusion
si je ne me suis pas trompée les matheux qui fréquentent en nombre ce forum vont pas trainer à comprendre le pourquoi du comment
et si çà suffit à montrer p=np (formulation un chouilla paradoxale) je suis sur que tu trouveras bien quelqun pour t'aider à toucher la forte somme
je serais curieux de savoir comment tu tes débrouillé pour arrivé a cette conclusion
pour le reste j'en sais pas plus
@Shah d'Ock
Elle serait drôle, votre blague, si je pouvais être sûr que j'avais faux mais le problème, c'est que j'ai testé un algorithme en Python (un vrai langage de programmation) et il semble marcher. Et je suis sûr qu'il est en temps polynomial car je ne fais pas apparaître d'instructions exponentielle.
Sinon, je vais vous expliquer comment vous pourriez l'utiliser simplement:
J'ai créé un objet v pour les variables.
Pour faire appel à v(n) vous écrivez v(n). Pour faire appel à non(v(n)), vous écrivez v(n).neg().
Pour la première formule((v(a) ou v(b) ou non v(c)) par exemple), vous gardez les doubles crochets.
Pour les formules suivantes, vous mettez en crochets,séparé par des virgules vos 3 variables. Ce triplet vous le mettez dans regroupement.append().(il y a 3 variables car il s'agit du problème 3-sat).
Essayez de ne pas laisser de trous(par exemple v(5) et v(7) sans v(6)), ça pourrait faire boguer l'algorithme.
Ainsi, l'algorithme aura un tableau (ou une liste) bi-dimensionnel qui permettra de faire apparaître la formule.
Mais la seule chose qui compte, c'est l'endroit où c'qu'elle tombe.
Soit tu postes une preuve convaincate que ton algorithme est correct et s'effectue en temps polynomial (pour l'instant, plusieurs personnes te l'ont déjà dit, c'est du charabia), soit tu contactes directement l'Académie des Sciences.
Je vais vous résumer en quelques mots ma preuve(de façon intuitive):
Pour que le problème soit insatisfaisable, il faut avoir l'ensemble des combinaisons de bits dans le problème
Pour ce faire, nous allons supprimer les regroupements identiques, et supprimer les regroupements contenant une variable dont le nombre n'est pas présent au moins 8 fois(le nombre de combinaisons possibles) dans l'ensemble du problème.
Quant à votre question sur les virus:
-Si j'étais un hacker, je ne m'amuserais pas à mettre le code source en ligne (via python)(histoire que l'on sache qu'il y a un virus(surtout dans un programme d'une cinquantaine de lignes)). Je préférerais un fichier exécutable.
-Si cela peut vous rassurer, il existe des machines virtuelles (programmes qui isolent des applications du reste de la machine). Ainsi, si mon programme était un virus(ce qui n'est pas le cas), il ne s'attaquerait qu'à la machine virtuelle.
-Il est également possible d’exécuter un programme sans risque sur un interpréteur en ligne puisque ce dernier ne donne pas accès aux fichiers de l'ordinateur.(fonctionnalité non disponible).Je vous envoie d'ailleurs un lien vers mon programme:ici
Vous me dites que vous ne comprenez rien à ce que j'ai écrit.
Certes, je comprends que vous pensez que ce soit mal rédigé. Vous seriez aimable de me dire ce que vous n'avez pas compris. Ça me fera très plaisir de faire des éclaircissements y compris si cela doit être sur l'ensemble de ma preuve.
Je ne saurais combien vous remercier même à l'avance.
Ce qui est important à comprendre,c'est que dans une formule disjonctive(que l'on peut obtenir à partir de n'importe quelle forme conjonctive) pour qu'elle soit fausse,
il faut que chacune des termes réunis par un opérateur "ou" soit faux. Dans ce groupement des termes réunis par un opérateur "ou", pour avoir plusieurs variables dont la réunion par la valeur "et" donne faux, quelque soit le résultat des autres variables,il faut que chacune des formes soit fausse.
Or, si on prend un regroupement sans contradiction logique, le regroupement peut être satisfait à partir du moment que l'on remplace les non(v(n)) par v(n)=0 et les v(n) par v(n)=1.
D'où la nécessité des contradictions logiques.
En développant ces contradictions logiques, on obtient une combinaison de l'ensemble des bits pour le transformer dans la forme du problème des 3-SAT.
D'où l'utilité de détecter cette combinaison en temps polynomial.
Pour la détecter en temps polynomial, il faut simplifier la proposition, compter le nombre de v(n) dans la proposition, et supprimer chaque triplet qui contient un v(i) dont la quantité dans la proposition est inférieur à 8.
Sinon je met le code en Python, pour ceux qui ont peur des virus et qui ne peuvent pas regarder: Si vous voulez plus de détails sur le problème 3-SAT vous pouvez voir ici.
j'ai appuyé sur "ça va ou quoi?" et ça ne marche pas.
J'ai python version 6.0 pourtant.
S
Pour tester le programme Python, il faut la version 3 (et pas la version 6 qui n'existe pas).
Si ton programme ne prend en entrée que des formes normales disjonctives, ben il ne résout pas 3-SAT.
Ce qui est dans l'algorithme, c'est la vérification de l'ensemble des motifs d'insatisfaisabilité(les 8 combinaisons que vous pouvez voir dans la capture d'écran Maple) que j'ai obtenu en temps exponentiel en dehors de l'algorithme, en comptant le nombre de même variables(que ce soit par exemple à la fois v(1) et non v(1)) dans la proposition.
On pourrait penser que cela non plus ne se fait pas en temps polynomial sauf que je me suis rendu compte qu'il suffisait de simplifier la proposition et de compter le nombre de variables pour s'assurer qu'il y a toutes les combinaisons.
Entrée: une forme normale conjonctive dont toutes les clauses ont au plus trois littéraux,
Question: est-elle satisfaisable?
Si ton algo ne prend pas en entrée des formes normales conjonctives, il ne répond pas à 3-SAT, point barre.
L'algorithme prend bel et bien, en entrée des formes normales conjonctives, l'opération de motifs d'insatisfaisabilité s'applique à une forme conjonctive sous forme de liste à 3 variables que je met dans l'algorithme pour donner le résultat.
S'il y a toutes les combinaisons possibles de variables, il y a 2^3=8 variables identiques. Il suffit de compter chacune des variables et s'il y en a moins de 8 on supprime tous les groupes de 3 littéraux qui contiennent cette variable, jusqu'à ce que les combinaisons pour les ensembles de triplets y soient toutes ou qu'il y en a aucune. En effet, comme je l'ai démontré avec mon logiciel de calcul formel,quand on développe l'expression insatisfaisable, on obtient toutes les combinaisons.
L'algorithme ne prévoit pas le cas avec 2 littéraux mais il est démontré par des chercheurs que le problème avec 2 littéraux est P voir ici.
Tu n'as pas répondu à ma deuxième question.
Je ne suis pas dans une boucle infinie, c'est juste que le problème n'est pas forcément très simple à résoudre donc je réfléchis et je travaille pour la résolution du problème (en dehors de mes heures de cours auxquelles je participe en tant qu'étudiant dans un IUT(horaires très chargés et présence obligatoire pour valider le diplôme)).
Donc on est d'accord que ce qui reste à démontrer c'est la possibilité de mélanger clauses à 3 littéraux et clauses à 2 littéraux.
-Si l'un des deux problèmes: 2-SAT ou problème avec exactement 3 clauses (mon algorithme) ,est insatisfaisable, alors le problème associant les deux types de clauses est insatisfaisable du fait de l'opérateur "et", jusqu'ici tout paraît évident.
-De même une proposition insatisfaisable "et logique" une proposition satisfaisable est insatisfaisable.
-S'il y a une ou deux variables étrangères dans un groupe de 2 clauses par rapport aux groupes de 3 clauses, elle n'empêche pas la satisfaction d'une proposition(le développement en proposition conjonctive le montre).
-S'il y en a dans plusieurs clauses, il suffit de regarder la satisfaisabilité séparément.
-Sinon on peut factoriser la proposition satisfaisable P(3 clauses) dans chacun des cas(pour les clauses à 2 littéraux):
(v(1) ou v(2)) et P = (v(1) et P) ou (v(2) et P) (satisfaisabilité non empêché,si P ne contient ni non(v(1)) ni non(v(2)),de même pour tous les cas avec une seule clause.
v(1) et P(satisfaisabilité non empêché,si P ne contient pas v(1)),de même pour tous les cas avec une seule clause.
(v(1) ou v(2)) et (v(1) ou non v(2)) et P = (v(1) et P) ou (v(1) et non v(2) et P) ou (v(2) et P) ou (v(2) et non v(2) et P)(satisfaisabilité non empêché si P ne contient pas non v(1)).
(non(v(1)) ou non (v(2)) et (v(1) ou v(2)) et P = P (satisfaisabilité non empêché).
(v(1) ou v(2)) et (v(1) ou non(v(2)) et (v(2) ou non v(2)=P et v(1) et v(2)(satisfaisabilité non empêchée si P contient ni non(v(1)),ni non(v(2)).
Je suis quasiment sûr qu'il existe un algorithme permettant de finaliser tout ça en temps polynomial. Je vais essayer de le rédiger dès que je peux.
Et merci pour vos conseils.
J'ai modifié ma formule pour qu'elle soit acceptable par ton programme: ça ne devrait donc pas être bien compliqué de m'expliquer le déroulement de ton algo sur cette formule.
Et tu n'as pas répondu à mon autre question: as-tu bien compris que 3-SAT ça veut dire trois littéraux par clause [et non l'inverse merci Gabu], mais qu'on peut utiliser autant de variables propositionnelles distinctes que l'on veut? Parce qu'il n'y a pas besoin d'être un génie pour s'apercevoir que des applications d'un ensemble de trois variables dans $\{0,1\}$, il y en a exactement $8$, et que de tester si l'une d'entre elle rend vraie une formule ne contenant que ces trois variables, ça se fait en temps linéaire.
J'ai compris que l'on peut utiliser n'importe quel type de variables (y compris triplets de 3 et couples de 2) c'est pour cela que je cherche comment avoir une proposition insatisfaisable avec des couples de 3 et de 2.
Alors juste pour fixer le vocabulaire:
Variable = symbole autre que $\land, \lor, \neg, (, )$,
Littéral: variable éventuellement précédée du symbole $\neg$,
Clause: suite de littéraux séparés les un des autres par le symbole $\lor$,
Forme normale conjonctive: suite de clauses [et non de littéraux, merci Zomeu] entourées de parenthèses et séparées les unes des autres par le symbole $\land$.
3-SAT: étant donnée une forme normale conjonctive dont toutes les clauses comportent au plus trois littéraux, existe-il une application de l'ensemble des variables dans $\{0,1\}$ qui la rende vraie?
"as-tu bien compris que 3-SAT ça veut dire trois clauses par littéraux"
ou là :
"Forme normale conjonctive: suite de littéraux entourés de parenthèses et séparés les un des autres par le symbole $\land$",
ça ne va pas éclaircir cette mélasse !
.
Je me suis mal exprimé mais je voulais dire ensemble de littéraux.(mais je me mélange les pinceaux).
Pour la satisfaisabilité des formules bien sûr que j'ai compris qu'on peut utiliser plus de 3 variables d'où ma référence aux variables étrangères.
Je crois que j'avais raison depuis le départ dans le fait que mon algorithme prouve que P=NP et que j'ai perdu la certitude que c'était le cas car je ne savais rien du cas où il y a deux variables et j'ai donc donné des pistes de recherche à la place qui ne servent à rien.
Revenons à notre forme disjonctive:
Pour satisfaire l'insatisfasibilité,on a:
f=(v(1) et non v(1) et v(2)) ou (v(2) et non v(2)) ou (v(3) et non v(3)) par exemple.
Ce v(2) va se développer de manière à donner des groupes de 2 littéraux par exemple.
Ainsi, on a la seule manière d'obtenir à la fois des clauses de trois littéraux et des clauses de deux littéraux de telle manière qu'ils soit insatisfaisables, qui est de rajouter des propositions dans les parenthèses de la forme disjonctive.
Lors du développement, on obtient les motifs recherchés par mon algorithme.
Cependant s'il y a une insatisfaisabilité lié à : (v(1) et non v(1)) ou (v(2) et non(v(2)), il ne sera détectable qu'avec un algorithme 2-SAT(qu'il faudra faire tourner en plus de mon algorithme pour résoudre le problème et que je ne suis pas sûr de pouvoir mettre sur internet car il est peut-être copyrighté.).
($x,y,z$).
c'est ce que j'appelerais le comment de l'algoritme
il me semble qu'a un certain moment il avait commencé à expliquer en langage comprehensible le pourquoi mais que ca a tourné en eau de boudin sur la fin
bonjour chez vous
juanita
bon le temps que je tapote mes conneries bound à frappé (c'est pas archi clair soit dit en passant)
pour le problème de copyright tu na qu'a ralonger ta formule logique de manière hadock pour qu'il n'y ait que des triplés
Je veux que tu m'expliques pas à pas le déroulement de ton algorithme sur la formule
$(v_1 \lor v_1 \lor \neg v_2) \land (v_2 \lor v_2 \lor \neg v_3) \land \dots \land (v_n \lor v_n \lor \neg v_{n+1}) \land (\neg v_1 \lor \neg v_1 \lor \neg v_1) \land (v_{n+1} \lor v_{n+1} \lor v_{n+1})$. À la fin, cette formule est satisfaisable, ou non?
Milgram: si tu as bien compris l'algorithme alors il est bien clair:
-qu'il s'exécute en temps polynomial,
-qu'il ne résout pas 3-SAT.
Le bonjour chez vous aussi.
Je vais vous expliquer le déroulement de mon algo pour lequel on ne peut pas faire plus simple pour un problème aussi compliqué:
-Il supprime les clauses de 3 littéraux présents plus de deux fois.
-Tant qu'il reste des éléments à supprimer dans la liste il compte le nombre de même littéral dans la proposition et supprime les variables présents moins de 8 fois(le nombre de combinaisons).
-S'il reste aucun triplet le problème est satisfaisable. Sinon il n'est pas satisfaisable.
j'ai trainé mon cul assez longtemps à l'université pour m'apercevoir que les profs était particulierement facétieux
j'ai d'ailleurs conservé assez de paperasse pour prouver mes dires
maintenant soi je me suis planté dans mon raisonement sur ce problème
soi je suis aussis genial que donald Trump (ce qui m'étonnerait vu que résolument je ne suis pas climatosceptique )
soi 3 sat n'est pas np-complet
passe le bonjour à tes voisins de ma part aussi
En attendant bonsoir.
Cordialement.
juanita
Sinon, il suffit de m'envoyer le lien du raisonnement.
Ce n'est pas grave s'il est vérolé, j'ouvrirai le document dans une sandbox. Il suffit de me l'envoyer par message privé.
Sinon, je suis vraiment désolé d'avoir vexé Shah d'Ock à ce point.
Non, je ne me considère pas comme plus intelligent que les autres, intelligence qui n'est même pas définie scientifiquement contrairement à ceux qui parlent de QI ou d'intelligence artificielle. ,Je reconnais juste des facilités que j'ai pour comprendre les mathématiques qui sont en complet décalage avec la rigueur mathématique dans la rédaction que je ne possède pas n'ayant même pas fait une seule année de licence de mathématiques ou de classe préparatoire aux grandes écoles ou d'autres études de mathématiques.
Sinon, à partir de maintenant l'algorithme résout le problème y compris s'il y a 2 littéraux (ou même quatre ou plus du seul moment où il n'y a pas de trous pour les littéraux)
Voici le code source de mon nouveau programme: J'ai modifié le message car j'avais fait un bug puis car les crochets [ i] ont été interprétés comme de l'italique par le forum.
J'ai modifié le fichier sur l'interpréteur en ligne et sur le premier lien également.
Bref, ce programme ne répond pas convenablement.
Je ne le savais pas (désolé, je ne suis pas non plus un gourou en Python).
J'ai vérifié en débuggant, c'était le non(v(4)),donc 1 liste ne contenant qu'un littéral qui pose problème.
Voici donc le nouveau code:
Je reviens sur ce sujet car je pense avoir découvert une piste de recherche.
Le problème 3-SAT se réduit au problème 1-dans-3-3SAT(qui dépend du théorème de Schaefer et dont je n'ai pas tenu compte dans mes programmes) dans lequel il n'y a que des clauses avec 1 seul et unique littéral positif et donc que des clauses avec 2 ou 3 littéraux.
Comme le montre ma capture Maple et mes recherches(en tant que non chercheur) sur le sujet, il semble qu'il suffit que les clauses à deux littéraux contiennent des littéraux annulant ceux des clauses à trois littéraux pour que la proposition soit insatisfaisable. Cela semble être une condition nécessaire car il n'y a pas(je pense) de simplification possible permettant d'obtenir une proposition insatisfaisable à cause du fait que les combinaisons comme {v(1) ou v(2);v(1) ou non v(2);non v(1) ou v(2);v(2) ou non v(1)} car il n'y a qu'un seul et unique littéral positif.