P versus NP
Bonjour,
Je suis chercheur en mathématiques et en informatique théorique à la retraite. J'aimerais vous proposer une approche de la question de complexité théorique concernant $P/NP$. Cela se fera en plusieurs étapes "pédagogiques".
1) Vers une réduction polynomiale de 3SAT à HORN-SAT.
Les versions successives de la note sont ici :
horner.pdf
horner1.pdf
horner2.pdf
horner3.pdf
Ces approches sont incomplètes. Je l'ai dit, c'est pour présenter les idées et comprendre la suite. De plus, elles ne marchent pas sur certaines formules comme celles traduisant le principe des tiroirs de Dirichlet.
Au final, on en arrive à l'idée que l'on peut intégrer de nouvelles clauses déduites à la formule $F$. Et aussi qu'il faudrait une méthode qui puisse être vérifiée par un logiciel comme Coq. Sinon, la preuve ne sera pas admise.
On peut le comprendre.
Ceci amène à la deuxième phase.
2) Un algorithme de complétion qui intègre ce que l'on a vu et qui l'étend.
C'est compilé dans la présentation suivante.
comp.pdf
c'est un algorithme qui fonctionne très bien et pour lequel je n'ai pas de contre-exemple.
Voilà, maintenant il reste à faire la preuve de cette méthode simple (avec Coq ?)
début de preuve dans comp1.pdf....preuve plus complète dans comp5.pdf
Je suis chercheur en mathématiques et en informatique théorique à la retraite. J'aimerais vous proposer une approche de la question de complexité théorique concernant $P/NP$. Cela se fera en plusieurs étapes "pédagogiques".
1) Vers une réduction polynomiale de 3SAT à HORN-SAT.
Les versions successives de la note sont ici :
horner.pdf
horner1.pdf
horner2.pdf
horner3.pdf
Ces approches sont incomplètes. Je l'ai dit, c'est pour présenter les idées et comprendre la suite. De plus, elles ne marchent pas sur certaines formules comme celles traduisant le principe des tiroirs de Dirichlet.
Au final, on en arrive à l'idée que l'on peut intégrer de nouvelles clauses déduites à la formule $F$. Et aussi qu'il faudrait une méthode qui puisse être vérifiée par un logiciel comme Coq. Sinon, la preuve ne sera pas admise.
On peut le comprendre.
Ceci amène à la deuxième phase.
2) Un algorithme de complétion qui intègre ce que l'on a vu et qui l'étend.
C'est compilé dans la présentation suivante.
comp.pdf
c'est un algorithme qui fonctionne très bien et pour lequel je n'ai pas de contre-exemple.
Voilà, maintenant il reste à faire la preuve de cette méthode simple (avec Coq ?)
début de preuve dans comp1.pdf....preuve plus complète dans comp5.pdf
Réponses
-
Bonjour Serge,
Mon niveau en complexité algorithmique étant ce qu'il est (c'est-à-dire pas grand-chose), je ne me risquerai pas à intervenir sur ce sujet. Mais je lirai avec attention les interventions des spécialistes, ainsi que les évolutions de ton article. En attendant je te souhaite bon courage pour la suite.
Martial
P.S. Ah, purée, si vraiment $P=NP$ on va galérer pour continuer à faire des transactions par CB sur Internet, lol -
Merci Martial....c'est sympathique. Après, pour les CB, ce n'est pas avec cette méthode que l'on va casser des codes. En effet, c'est un résultat théorique. Dans la pratique, c'est abominable pour ne pas dire minable. Une petite formule F toute simple devient un monstre H énorme qui met énormément de temps à être résolu. Il y a beaucoup plus de variables et beaucoup plus de clauses. Mais les clauses sont de Horn et la réduction est polynomiale. C'est suffisant.
-
Pour vous montrer à quel point cette méthode n'est que théorique et en rien pratique,
une "petite" instance F de 3-SAT sur 4 variables et formée de 5 clauses devient....
une "horrible" instance H de Horn-SAT sur 65 variables et formée de 12651 clauses. -
1/ Attention, le fait que "en pratique ça ne marche pas vite" ne doit pas te rassurer quant à l'espoir qu'il n'y ait pas d'erreur.
2/ J'ai lu en diagonale (fatigue, travail à faire). Ton papier fait ... une page et non pas 2, puisque tu occupes la moitié en commentaires.
3/ Pour un résultat aussi révolutionnaire (entre 100000 milliards d'euros et 10^15 euros sur le marché), ce que tu dis est trop rapidement résumé. Trop raconté en anglais courant. Vu comme c'est court, je te conseille de:
3.1/ Le publier en l'état sur ArXiV ou HAL (avec références pour ce que tu admets (par exemple ta définition des Horn et que c'est P)
3.2/ Le réécrire de manière structurée FORMELLE, avec des admis numérotés pour que le lecteur puisse aller de la synthèse au détail. Pas juste une preuve formelle irréfutable chiante, mais des entrées et des aides mais à la fin la preuve formelle doit figurer, on doit pouvoir se balader dedans
3.3/ Pour l'instant (après mon anglais est très mauvais je l'avoue), on a "je réduis 3SAT à Horn-SAT, Horn-SAT est P, la réduction est P donc 3SAT est P". Mais dès qu'on entre dans le détail, ton algo est en anglais courant, tes $S,T_S$, sont difficiles à capter comme sûrs, etc. N'hésite pas à mettre des exemples si tu estimes qu'une définition formelle est indigeste.
4/ Pourquoi ne pas le rédiger en anglais ET en français. (Pour une page à remettre en 5 ....)Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@serge : J'ai lu en diagonale car je ne comprenais pas tout (je ne suis pas trop familier de ce genre de questions). J'ai quelques questions (peut-être naïves) :
1) Le problème est de savoir s'il existe un algorithme et un polynôme $P$ tel que pour toute conjonction $C$ de $N$ trucs (des clauses, c'est ça ?) comme $X_1 \vee X_2 \vee X_3$ où $X_i$ est une variable propositionnelle ou sa négation, quand on donne $C$ à l'algorithme, il nous dit en temps $\leq P(N)$ si on peut attribuer aux variables propositionnelles la valeur "vrai" ou "faux" de sorte que $C$ s'évalue comme "vrai" ?
2) Ton algorithme prend en entrée une formule $F$ dont les variables propositionnelles sont dans l'ensemble $V$, et sort une formule $H$ dont les variables propositionnelles sont dans l'ensemble des parties finies de $V$, n'est-ce pas ? -
Merci christophe c pour ces commentaires détaillés.
1) L'aspect pratique n'importe guère ici. C'est une construction générique qui n'est absolument pas optimisée. La plus grosse partie de la formule H est valable pour toutes les instances portant sur le même nombre N de variables. On lui rajoute K autres clauses en correspondance à celles de la donnée F
2) Cet article est en effet minimaliste et j'envisage bien sûr de l'étoffer. Il a été rédigé hier. Mais l'essentiel est là pour en comprendre les idées.
31) La publication sur ArXiv et dans une revue suivront...c'est prévu. Mais j'attends tout de même des retours de la part d'autres spécialistes. J'ai des publications sur d'autres sujets. Celle-ci est un peu particulière vu la question.
32) Oui, ce sera en effet la forme d'un article avec ses formats standards requis.
33) Des exemples, oui, c'est prévu. Maple est utile pour cela.
4) Mélanger anglais et français...non. Je n'ai pas compris <<(Pour une page à remettre en 5 ....)>> -
Bin je voulais juste dire que pour un truc qui in fine deviendra 5 pages, pourquoi ne pas en faire 10 (5 en français, 5 en anglais): vu que ce sera la plus grande découverte de tous les temps (tu en es conscient?)Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
Merci Georges Abitbol.
1) Non, ce n'est pas en temps P(N) mais P(|C|), c'est fonction de la taille de la représentation de C. Sinon, oui c'est ça.
2) Pas exactement. Les nouvelles variables sont en correspondance avec les sous-ensembles de littéraux portant sur les variables de V et de cardinalité <=3 et ne contenant pas de littéraux opposés. S'il y a N variables dans V, il y a 2N littéraux possibles et il y a au plus C(2N,0)+C(2N,1)+C(2N,2)+C(2N,3) nouvelles variables (où C(n,k) est le coefficient binomial).
On enlève encore les sous-ensembles contenant des littéraux opposés comme x et non x. Sinon, on pourrait aussi ajouter des axiomes supplémentaires du type (non T_s) pour de tels ensembles s comme par exemple s={x,y,non x}.
Par exemple, pour N=6, on obtient 233 nouvelles variables du type T_s.
Le seul axiome est (T_s) où s est l'ensemble vide. -
christophe c
Ton enthousiasme me touche, merci. Mais je dois le modérer au moins en remplaçant ton "ce sera" par "ce serait".
Par ailleurs, bien que ce problème soit célèbre, j'ai suffisamment travaillé dans ce domaine pour avoir du recul et savoir relativiser. Cela concerne à la base des machines de Turing. Des machines théoriques disposant d'une mémoire infinie. Cela n'existe pas. Si on considère les machines qui existent (nos ordinateurs) alors ce ne sont que de simples automates finis (du point de vue théorique) et dans ce cas, tout peut se faire en temps.....constant. Aucun problème de complexité ne se pose. Idem pour le problème indécidable de l'arrêt. Il ne s'applique pas aux ordinateurs qui ont un nombre fini d'états possibles...grand, je l'admet, mais en maths 2^(2^64) cela reste un tout petit nombre.
Dans la conclusion, je relativise encore et invite les scientifiques à travailler sur de "vrais" problèmes majeurs et cruciaux. -
-
Georges Abitbol
N est le nombre de variables sur lesquelles porte la formule F (vous l'appelez C, je préfère F et désigner par C une clause de F).
En complexité théorique, on exprime le temps de calcul (ou plutôt le nombre d'opérations élémentaires) en fonction de la taille de l'entrée (la donnée). La donnée c'est F et sa taille |F| peut être indépendante de N s'il y a des redondances de clauses. Sinon, en effet, la taille de F est majorable par $$(2N)(2N-2)(2N-4).3.(log_2(N)+1)$$ Il y a $2N$ littéraux sur $N$ variables (négation ou pas) et au plus $(2N)(2N-2)(2N-4)$ clauses de 3 littéraux portant sur des variables différentes, chaque littéral se codant en binaire par un mot de taille $log_2(N)$ et le $+1$ sert à indiquer le signe (négation ou pas). On aurait pu aussi écrire $log_2(2N)$. -
Oh oui, mince, c'est encore moi qui ai mal lu : $N$ est le nombre de variables, mais j'avais bien compris que la complexité se mesurait par rapport au nombre de clauses. Conclusion : je vais me coucher !
-
J'ai pu télécharger de mon téléphone. Et ai aussi compris ta traduction SAT--> Horn.
J'ai du taf incroyable today mais je vais pouvoir te dire mon ressenti assez vite. Éventuellement je décrirai ton algo sur forum vu qu'il est simplissime.
:-D je souhaite de tout coeur que tu aies raison. À côté les anciens problèmes ouverts résolus en 5 lignes feront figure de petits joueurs :-DAide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Merci christophe c,
J'ai du boulot aussi. Je vais continuer la rédaction en donnant des exemples. J'ai aussi écrit cette nuit des programmes en Maple dont un qui fournit une méthode bien plus efficace en se passant de la formule H mais qui se base sur cette formule pour effectuer des déductions, notamment pour la plus importante : une preuve de $(\lnot T_{\{\}})$ si possible. Dans ce cas et seulement dans ce cas, la formule F n'est pas satisfiable.
PS. Je suis nouveau sur ce forum et je viens tout juste de comprendre que l'on peut écrire directement en Tex...cool ! -
cons(F) => cons(H) est évident
Ton texte en anglais est par contre bien trop expéditif dans ce qu'il prétend être une preuve de :cons(H) => cons(F)
C'est franchement là dessus et sur rien d'autre que tu dois taffer en priorité:
cons(H)=>cons(F)Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
christophe c
Oui, j'en suis bien conscient. C'est le point flou. C'est bien de l'avoir observé. Là j'ai donné une sorte de "vision" intuitive de l'argument avec cette idée de preuves (recherches) en parallèle. Il va falloir formaliser tout ça et clarifier. -
Bonjour,
Voici donc une version horner1.pdf avec quelques exemples d'illustration.
Je vais maintenant travailler sur la preuve de la Proposition pour expliquer et formaliser la "vision intuitive" de cette recherche en parallèle d'une contradiction. La formule H peut être vue comme un graphe dirigé complexe avec des chemins et des cycles et des coupures. Je vais aussi ajouter de nouvelles règles de déductions relatives à la formule F.
Cela semble au moins plus efficace si ce n'est nécessaire.
Pour chaque $S\in\Delta$ et chaque clause $C=(X\vee Y\vee Z)$ de $F$, on ajoute les règles $T_S\implies T_P\vee T_Q\vee T_R$
pour $P\subseteq S\cup\{X\}$, $Q\subseteq S\cup\{Y\}$, $R\subseteq S\cup\{Z\}$ et $P,Q,R\in\Delta$
puisque $C$ est supposée vraie.
Ces "règles d'inférence" pourraient permettre d'obtenir une preuve assez simple. Partant d'une formule F non satisfiable sur des clauses $C_1,C_2,\dots,C_K$, tout choix de littéraux $[X_1,X_2,\dots,X_K]$, avec $X_i$ pris dans $C_i$, va contenir une paire de littéraux opposés. Partant de l'ensemble vide, on va plonger ce principe dans les règles d'inférence....enfin, on va essayer. On choisi un littéral ou non, on forme des sous-ensembles d'au plus $3$ littéraux et $2$ suffisent à avoir une contradiction (ou plutôt une impossibilité de continuer...une forme de CUT)
C'est rédigé dans horner2.pdf
à suivre : je vais tout de même ajouter un axiome pour le FAUX et considérer les ensembles contradictoires de littéraux. Ce sera plus complet et plus simple.
Fait dans horner3.pdf -
@serge burckel
Pour ce genre de choses, il faut réaliser une preuve formelle avec un logiciel de vérification de preuve.
Les professionnels du sujet sont non seulement sollicités régulièrement par des fausses preuves courtes de P=NP (ton article atterrirait directement dans la corbeille de leur boîte mail sans être lu) mais en plus il existe un très fort consensus parmi eux (non encore prouvé certes) en faveur de P =/= NP.
Les prouveurs formels sont idéaux (Coq, Lean, HOL, agda etc) pour ce genre de chose, publies un logiciel prouvé via un de ces outils et richesse, célébrité et respect mondial t'attendent.
**********************************************
Je dois répondre à ça, ce n'est pas du tout contre toi et ça fait plusieurs fois que je l'entends.serge burckel a écrit:Des machines théoriques disposant d'une mémoire infinie. Cela n'existe pas. Si on considère les machines qui existent (nos ordinateurs) alors ce ne sont que de simples automates finis (du point de vue théorique) et dans ce cas, tout peut se faire en temps.....constant. Aucun problème de complexité ne se pose. Idem pour le problème indécidable de l'arrêt. Il ne s'applique pas aux ordinateurs qui ont un nombre fini d'états possibles...grand, je l'admet, mais en maths 2^(2^64) cela reste un tout petit nombre.
L'affirmation "les machines de Turing n'existent pas" (parce que "les bandes infinies blabla" et "il y a un nombre fini d'atomes sur Terre") est un cliché répandu qui relève de la différence entre "infini potentiel" et "infini actuel".
Le texte ci-dessous se propose de détruire pour toujours cette abomination ultrafinitiste B-).
Soit $E$ un ensemble fini, $i,f\in E$, $\{g,s,d\}$ un ensemble à $3$ éléments, $t: E \times \{g,s,d\} \times \{0,1\} \to E \times \{g,s,d\} \times \{0,1\}$ une fonction (dite de "transition").
Plus bas on note $\{0,1\}^{(\Z)}$ l'ensemble de toutes les fonctions $\varphi$ de $\Z$ dans $\{0,1\}$ telles que $\varphi^{-1} \{1\}$ est borné.
NB:pour tout $n \in \N$ on désignera par $\theta_n$ l'application de $ \{0,1\}^{\{-n, -n+1, ... n-1,n\}}$ dans $ \{0,1\}^{(\Z)}$ qui à $u \in \{0,1\}^{\{-n, -n+1, ... n-1,n\}}$ et à $n\in \N$ et $k\in \Z$, fait correspondre $\theta_n(u)(k)= u(k)$ si $|k| \leq n$ et $\theta_n(u)(k)=0$ si $|k| \geq n$.
1°) on appelle calcul de machine de Turing associé à $(E,i,f,t) $ toute suite finie $(x_i,e_i,b_i,p_i)_{0 \leq i \leq n}$ d'éléments de $ \{0,1\}^{(\Z)} \times E \times \{g,s,d\} \times \Z$ telle que $e_0=i$, $e_n= f$, $b_0=s$, $p_0 = 0$, et pour tout $i\in \{0,1,...,n-1\}$, $[e_{i+1}, b_{i+1}, x_{i+1}(p_i)] = t[e_i, b_i,x_i(p_i)]$ et $p_{i+1}=p_i + \varepsilon (b_i)$ (avec $\varepsilon (g)= -1$, $\varepsilon(s) = 0$ et $\varepsilon(d) = 1$).
2°) Soient $N,M$ deux entiers naturels.
on appelle calcul de machine de Turing associé à $(E,i,f,t) $ et borné par $(M,N)$ toute suite finie $(x_i,e_i,b_i,p_i)_{0 \leq i \leq n}$ d'éléments de $ \{0,1\}^{\{-M,-M+1, ... M-1,M \}} \times E \times \{g,s,d\} \times \Z$ telle que $n \leq N$, $e_0=i$, $e_n= f$, $b_0=s$, $p_0 = 0$, et pour tout $i\in \{0,1,...,n-1\}$, $[e_{i+1}, b_{i+1}, x_{i+1}(p_i)] = t[e_i, b_i,x_i(p_i)]$ et $p_{i+1}=p_i + \varepsilon (b_i)$ (avec $\varepsilon (g)= -1$, $\varepsilon(s) = 0$ et $\varepsilon(d) = 1$)
(i) Il est clair que pour tous $M,N$ et tout calcul $(x_i,e_i,b_i,p_i)_{0 \leq i \leq n}$ de machine de Turing borné par $(M,N)$, $(\theta_M(x_i),e_i,b_i,p_i)_{0 \leq i \leq n}$ est un calcul de machune de Turing.
(ii) Réciproquement pour tout calcul $(y_i,e_i,b_i,p_i)_{0 \leq i \leq n}$ de machine de Turing, il existe deux entiers $M,N$ et un calcul de machine de Turing $(y'_i,e_i,b_i,p_i)_{0 \leq i \leq n}$ borné par $(M,N)$ et tel que $\theta_M(y'_i)=y_i$ pour tout $i$.
Ainsi, la théorie des machines de Turing et celle des machines de Turing bornées décrites ci-dessus sont équivalentes.
Une machine de Turing bornée n'est rien d'autre qu'une machine qui s'exécute sur une bande finie (et accessoirement qui renvoie un message d'erreur en ca de dépassement) et en un nombre d'étapes fixé à l'avance. Le fait qu'il existe des entiers $N,M$ pour lesquelles une machine de bande de taille $M$ ne puisse pas être construite physiquement ou fonctionner en temps réaliste ($N$ supérieur à un multiple de l'âge de l'univers divisé par le temps de Planck mettons ) n'invalide en rien les résultats d'informatique théorique autour de ces concepts. En outre si un problème est insoluble par une machine de Turing, une machine de Turing bornée ne pourra pas non plus le résoudre.Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Les phénomènes d'indécidabilité (comme le problème de l'arrêt) n'ont rien à voir avec l'infinitude éventuelle de l'ensemble des entrées d'un appareil.
Soit $E$ un ensemble (quelconque donc éventuellement fini), $D$ un sous-ensemble de $E^2$, $\Phi: D \to \{0,1\}$ une application, $x, y \mapsto xy$ une application de $E^2$ dans $E$ et $u \mapsto \overline u$ et $u \mapsto u^*$ deux applications de $E$ dans $E$.
Pour tous $x,y\in E$, on dira "$\Phi(x,y)$ est défini" lorsque $(x,y)\in D$.
On suppose que:
1°) pour tous $x,y$, $\Phi(x,y)$ est défini si et seulement si $\Phi(\overline x,y)$ l'est et le cas échéant, $\Phi(\overline x,y) = 1- \Phi(x,y)$
2°) pour tous $x,y$, $\Phi(x^*,y)$ est défini si et seulement si $\Phi(x,yy)$ l'est et le cas échéant, ils sont égaux i.e. $\Phi(x^*,y)=\Phi(x,yy)$.
Lorsque $A$ est une partie de $E$ (resp $E^2$), on dira que "l'appartenance à $A$ est testable par $\Phi$" s'il existe $a\in E$ telle que pour tout $x\in E$,$(a,x)\in D$ et si $x\in A$ alors $\Phi(a,x)=1$ et si $x\notin A$ alors $\Phi(a,x)=0$ (resp pour tous $y,z\in E$, $(a,yz) \in D$ et $\Phi(a,yz)=1$ si $(y,z)\in A$ et $\Phi(a,yz)=0$ si $(y,z)\notin A$).
Alors:
(i) L'appartenance à l'ensemble des $(x,y)$ tels que $\Phi(x,y)=1$ n'est pas testable par $\Phi$.
En effet soit $a\in E$ comme ci-dessus tel que $\Phi(a,xy)=1$ si et seulement si $\Phi(x,y)=1$.
Alors $\Phi(a, \overline{a^*} \: \overline{a^*}) = \Phi(a^*,\overline{a^*}) = 1 - \Phi(\overline{a^*}, \overline{a^*})$
Tout est défini, cf 1)° et 2°). On a également $ \Phi(\overline{a^*}, \overline{a^*})=1$ (resp $0$) ssi $\Phi(a, \overline{a^*} \: \overline{a^*}) = 0$ (resp $1$) ce qui entraîne une contradiction.
(ii) il n'existe aucun $h$ tel que pour tous $x,y\in E$, $(x,y)\notin D$ si et seulement si $(h,xy)\in D$.
Car on a $(h, \overline {h^*} \: \overline {h^*}) \in D$ ssi $(h^*, \overline {h^*})\in D$ ssi $( \overline {h^*}, \overline {h^*}) \in D$ pour tous $h$ via 1°) et 2°).
En particulier, si pour tout $u\in E$ il est possible de construire $u'\in E$ tel que pour tout $x\in E$, $(u',x)\in D$ si et seulement si $(u,x)\in D$ et $\Phi(u,x)=0$ alors l'ensemble $D$ n'est pas testable. (Si on dit que "$\Phi$ plante sur $(x,y)$" lorsque $(x,y)\notin D$, cette hypothèse supplémentaire dit qu'on est capable de produire un programme qui plante lorsqu'une certaine condition est remplie).Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Cher Foys,
pour les preuves ou vérifications de preuves par Coq, oui, j'en ai déjà entendu parler. Il faudrait que je m'y mette... mais je ne suis plus étudiant depuis un moment.
Pour les machines de Turing, ton exposé est un peu compliqué pour dire :
i) tout calcul borné en temps (cela suffit puisque cela donne une borne en espace) de MT est un calcul de MT
ii) tout calcul FINI de MT est réalisable par une MT bornée.
Ce qui est en fait la même chose et une trivialité. Par contre, je ne suis toujours pas d'accord sur le fait de prêter ces propriétés à nos ordinateurs (et cela fait des années que ça dure....;-)) -
Cher Foys,
Au sujet du problème de l'arrêt. Pour un ordinateur, c'est décidable avec.....un chronomètre.
S'il possède M états possibles (du genre M=2^N avec N relativement grand) et passe d'un état à un autre en au plus t secondes, on fait tourner notre programme, on enclenche notre chronomètre et si au bout de M.t secondes il n'y a pas eu d'arrêt, alors c'est que ça boucle.
Bon, le plus probable c'est que l'ordinateur soit depuis longtemps foutu et nous avec ;-) -
Tu noteras que pour établir cet arrêt tu as besoin d'un outil extérieur à l'ordi (chronomètre), le problème de l'arrêt fait référence à un test algorithmique.
Toutes ces considérations sur la finitude sont similaires au point de vue qui dit que l'ensemble des nombres entiers est fini (car on ne pourrait pas écrire certains nombres sur un support physique accessible).
P vs NP n'a pas de sens dans le monde ultrafinitiste au passage (ce résultat parle nécessairement du comportement asymptotique d'une fonction).Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Cher Foys,
Le problème de l'arrêt c'est l'existence d'une MT A qui prend en entrée le code M d'une MT et un mot w et décide si le calcul de M s'arrête en partant du mot w.
La supposée MT A est bien aussi "extérieure"....tout comme un chronomètre.
Pour P vs NP avec des passages à la limite de fonctions....oui, tout à fait ! Là on se rejoint sur le plan philosophique.
;-) -
On note $\{vrai,faux\}$ les booléens.
Soit $t$ le programme qui prend $h,x$ en entrée et qui renvoie $vrai$ si $h(x,x)=faux$ et qui exécute une boucle infinie (while 0 = 0 do (...)) si $h(x,x)=vrai$.
Soit $H$ un programme quelconque à deux entrées. alors $H (T(H))(T(H))$ ne teste pas correctement l'arrêt de $T(H)$ sur $T(H)$ (s'il renvoie quelque chose, ça va être le contraire de la vérité au sujet de l'arrêt de $T(H)$ sur $T(H)$).Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Cher Foys,
En effet, je vais certainement tout reformuler en terme d'un algorithme de preuve qui effectue une clôture par déductions.
Ce sera plus simple et plus "négociable" avec un logiciel de vérification comme Coq.
Je veux bien des informations et de l'aide à ce sujet...je n'y connais rien.
Je programme en Maple pour tester des idées et j'écris parfois des programmes de preuve ou des programmes qui écrivent des parties de preuves.
Bon donc demain à l'aube je m'y mets au chant du Coq.
;-) -
@foys, je sais que tu es à la retraite :-D , mais l'argument de Serge est vraiment simple et fait 5 lignes. J'ai lu en diagonale, mais je crois voir que tu as rebondi sur autre chose, alors que si ça se trouve, vue ta force, tu pourrais peut-être lui dégoter un contre-exemple en 10mn (à la partie qu'il ne justifie pas qui dit que si H (construit avec son algo en fonction de F) est satisfiable alors F l'est. Certes, ce serait trop beau si c'était vrai, n'empêche qu'au moins on a une zolie affirmation bien carrée à gouter.
Ce serait bête qu'il apprenne COQ et tape 3H juste pour ça s'il y a un CE court.
Et moi j'ai des journées de ouf de chez ouf, ne peux pas vrmt chercher un CE.
Si tu veux (mais je pense que tu n'en as pas besoin) je t'écris formellement ce qu'il dit en quelques lignes sans imprécision.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
christophe c
Ce que j'ai décrit ici pour l'instant est une première approche incomplète. Ce n'est pas fini. La complétion est en cours....
Ce n'est pas évident de trouver un contre-exemple. Pour les formules prises au "pseudo-hasard" cela fonctionne.
Mais, pour ce qui est présenté pour l'instant, j'ai un Contre-Exemple. Inutile d'ennuyer Foys. C'est la formule qui dit qu'il n'existe pas d'application injective de $E$ dans $F$ avec $|E|=n+1$ et $|F|=n$. (formule des trous de pigeons / principe des tiroirs). Pour $n=6$, c'est un C.E. Pour le montrer, il m'a fallu tout programmer et faire tourner la méthode sur cette formule assez grosse. Trop grosse pour ma méthode qui a pris toute la journée pour....échouer. Néanmoins, c'est positif car cela me sert actuellement à compléter la méthode....une forme de preuve itérative en quelque sorte. Et je sais comment compléter. Là je le programme et vais essayer sur cette formule. Par ailleurs, cette complétion donne de plus en plus l'idée de la preuve....à suivre..... -
La méthode de complétion fonctionne. Elle est la suivante : lorsqu'une preuve d'un $(\lnot T_s)$ est obtenue, alors on rajoute la clause correspondant à la négation de $s$ à la formule $F$. Tout cela parait bien compliqué dans ce formalisme. Mais quand on l'écrit autrement cela devient très simple. Je vais le rédiger et le publier ici..si c'est possible aujourd'hui.
-
Voilà, j'ai programmé et rédigé rapidement une première petite note qui expose la méthode.
Les précédentes notes permettent (peut-être) de comprendre cette complétion.
En tout cas, cela fonctionne, même sur les "supposés" contre-exemples (formules du principe des tiroirs de Dirichlet)
Et cela devrait pouvoir se traiter avec Coq ou autre logiciel de preuve.
Je vais continuer....à suivre....
Voici la méthode avec quelques explications.
Tout ceci provient de ce que l'on a vu avec les formules de Horn.
C'est quand même plus simple ainsi.
Et pour Coq aussi..... -
Là du coup, je veux bien que vous cherchiez un contre-exemple....je pense qu'il n'y en a pas.
Désolé de vous avoir embarqué avec les présentations par les clauses de Horn.
C'était des approches préliminaires pour pouvoir comprendre celle-ci.
C'est tout autant valable pour moi qui fonctionne ainsi.
Un travail de complétion qui gère les obstacles.
Une sorte d'escalade, pas à pas.
Revoici le pdf...il va falloir en faire la preuve de cette méthode. Je ne sais pas utiliser Coq et je suppose que si je rédige une preuve, cela ne sera jamais considéré comme suffisant....alors que faire ? -
Y a-t-il quelqu'un de compétent ici pour vérifier ce programme avec Coq ou autre ?
Je vais rédiger dans les prochains jours une preuve "à ma façon".
C'est combinatoire. Cela se base sur tous les $3^K$ choix possibles de littéraux dans la formule $F$ de départ ayant $K$ clauses. $F$ est satisfiable si, et seulement si, il existe un tel choix non contradictoire. -
Voici le début de la preuve de la méthode.
La complexité est assez grande : $O(N^{12})$.
Pour la correction, j'y bosse mais je pense que les gens attendent une certification par Coq. -
Bonjour
Voici une suite à une discussion que j'ai engagée sur "Fondements et Logique" : P versus NP.
Je présente ici un algorithme polynomial pour le célèbre problème 3-SAT.
C'est le résultat (assez simple) d'une longue démarche. La méthode est très simple.
Ce serait bien, voire nécessaire, de faire une preuve par Coq de sa correction.
Si quelqu'un ici sait le faire... ce serait cool de le faire ensemble.
[Restons dans le discussion que tu as ouverte sur le sujet. AD] -
@Serge : je pense que Christophe est en mesure de faire la correction en Coq que tu demandes… mais peut-être n'a-t-il pas la disponibilité nécessaire.
Je ne sais pas de quelle université tu es originaire, mais au cas où tu pourrais aller faire un tour sur le site de l'équipe de logique Paris 7. J'ai vu qu'il y avait notamment un certain Pierre Letouzey qui y enseigne en M2 un module intitulé : "Programmation fonctionnelle et preuves formelles en Coq".
Peut-être pourra-t-il t'aider.
Bon, c'est juste une suggestion, je ne connais rien à ce domaine. -
@Martial
Merci. En fait j'ai travaillé au LORIA (INRIA de Nancy) et aussi au CNRS (IML) à Luminy et enseigné à l'Université de la Réunion. Je connaissais quelques logiciens de Paris 7...je vais voir.
J'ai repris contact avec le Loria ce soir mais tes suggestions sont très bonnes et je vais les suivre.
Si Christophe C, qui semblait enthousiaste, est disposé à contribuer, c'est magnifique aussi.
à suivre..... -
@Serge : Christophe C est toujours disposé à contribuer, mais il a aussi beaucoup de chats à fouetter, dont certains chats qui méritent vraiment d'être fouettés. Si je pouvais t'aider ce serait avec plaisir, mais hélas j'ai une formation quasi-nulle en complexité algorithmique. J'ai obtenu le M2 LMFI en 2004, et Ramez Labib-Sami en a parlé un tout petit peu dans son cours de récursivité / calculabilité. Le problème c'est que comme je travaillais en même temps je pouvais suivre un cours sur 15, ce qui ne facilite pas les choses. Quant au Coq, c'est une langue qui m'est beaucoup plus étrangère que le finlandais, dont je connais 5 ou 6 mots, c'est pour te dire...
@Christophe : ce n'est pas une faute de frappe, il y a bien un "s" à "chat" et à "fouetté", lol. -
De mon téléphone: Serge, tu as écritMais, pour ce qui est présenté pour l'instant, j'ai un Contre-Exemple. Inutile d'ennuyer Foys.
Autrement dit que ta preuve NE MARCHE PAS.
Je comprends parfaitement l'addiction que l'on peut avoir (ainsi que la déception) et espérer la réparer en la modifiant un peu.
C'est "la dureté" de la recherche. Mais la probabilité maintenant que des voisinages de ta preuve fausse marchent est extrêmement faible. Tu peux rester sous le charme pendant quelques temps mais n'oublie pas de prendre du recul ensuite. Souvent pour se débarrasser de cette horrible addiction à l'émotion qu'on a eu en la croyant quelque temps vrai c'est de "MAGNIFIER " l'erreur. La grossir et en faire le tout et non pas de d'emprisonner dans un déni qui consiste à juste contourner ce contre exemple là oubliant les germes de fond qui produiront les autres.
SoiS fier d'avoir TROUVE TOI MEME le CEAide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@Christophe
Non, tu n'as pas compris ou alors pas tout suivi. C'est aussi de ma faute.
Je n'ai pas de contre-exemple pour la méthode. J'ai des contre-exemples pour ce que j'ai présenté avec les clauses de Horn. Cette présentation était un préliminaire pour arriver à la méthode de complétion. C'est un cheminement. Il ne faut pas s'arrêter en chemin.
La méthode horner a des contre-exemples...je les connaissais et c'est pourquoi j'ai répondu rapidement à ta demande.
Donc, une fois de plus, pour être clair, la méthode exposée dans comp.pdf est beaucoup plus complète que celle de horner et elle n'a pas de contre-exemple (à ce jour). Cette méthode de complétion devait aussi se cristalliser et je cherchais aussi le cheminement pour l'exposer simplement. Pour ma part, je suis convaincu que ça marche tout le temps et qu'il n'y a pas de CE.
Franchement, la méthode de complétion mérite d'être étudiée. J'espère que tu le comprends. Sinon, je vais regretter d'avoir fait cette démarche sur ce forum. Une démarche de recherche itérative. J'aurais bien aimé exposer directement la version de complétion, mais ce n'était pas encore clair. J'ai fait le chemin en même temps. De plus, des remarques ici m'ont fait comprendre qu'il fallait une vérification par Coq pour que ce soit acceptable, ce qui m'a conduit à modifier l'exposé et à laisser tomber l'approche par les clauses de Horn. On peut toutefois noter que la complétion pourrait aussi s'exprimer avec des clauses de Horn sans même ajouter de nouvelles clauses à $F$. Il suffit alors de considérer des implications du style $$T_s\wedge\lnot T_f\implies T_p\vee T_q\vee T_r$$ qui donne bien une clause de Horn
$$\lnot T_s\vee T_f\vee T_p\vee T_q\vee T_r$$
et où $T_f$ est arbitraire. Ceci veut dire sémantiquement : si on suppose $T_s$ et que l'on aurait déjà prouvé $\lnot T_f$ (ce qui donnerait une nouvelle clause dans $F$) alors au moins un des $T_p,T_q,T_r$ doit être vrai.
C'est plus compliqué et beaucoup moins clair que la méthode de complétion qui prend 10 lignes. -
Voici une petite note synthétisée (pour l'envoyer à des collègues faisant du Coq)
Il y a aussi des exemples qui peuvent donner des petits exercices sympas.
On montre que les simplifications "standards" sont réalisées par la méthode.
L'idée sous-jacente à cette méthode est de considérer la formule $T$ à prouver comme une théorie parlant d'elle-même et qui va par elle-même nous "révéler" son éventuelle contradiction.
Pour @Christophe : il n'y a toujours PAS de Contre-Exemple....pourtant j'en cherche et mes programmes tournent sans relâche sur des benchmarks. -
@Christophe,
Je partage ce que tu as dit sur les "voisinages des idées". C'est souvent vrai..mais pas toujours.
C'est la différence entre avancer et devoir s'arrêter puis se dépatouiller. Dans le cas de cette méthode, c'était en avançant. Une complétion se fait par étapes. Il n'y avait pas d'erreur à corriger mais des points à compléter. Là, je pense que c'est complet. -
Serge, c'est vraiment totalement indépendant de ma volonté, je ne dispose d'aucune disponibilité actuellement. Mais tu dis que je n'ai pas suivi (je simplifie). Je te pose donc une question simple:
dans l'article INITIAL que tu as posté (premier post), tu affirmes que :
[large]$$ cons(H) \Rightarrow cons(F) $$
pour chaque $F$ et chaque $H$ construit, en fonction de $F$ avec ton algo[/large] (qui est très simple et sans ambiguité).
Ai-je loupé quelque chose ou as-tu reconnu que c'est faux EN L'ETAT?
Je n'ai en effet pas compris, en lisant tes derniers posts (et n'ai pas le temps d'investiguer) si le contre-exemple que tu prétendais toi-même avoir trouvé est un contre-exemple à cette affirmation rouge?
Merci.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
J'ai lu ça en 3mn (chrono, pas métaphore) un matin dans le métro, de mon petit téléphone, donc du coup, oui, je reconnais que j'ai peut-être mal compris "contre-exemple à quoi?" tu évoques.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
@Christophe,
oui...ça c'est entièrement de ma responsabilité...désolé, c'est ma façon de rédiger. Je le fais comme un puzzle. Je mets les éléments essentiels et puis je remplis en complétant les trous. J'aurais dû expliquer comment je fonctionne. Je ne suis pas "standard" (autiste asperger) et fonctionne beaucoup par intuitions. Mais au final, cela converge souvent très vite et j'ai des publications "sérieuses" et reconnues.
je voulais partager cette façon de faire ici....un challenge !
Bon, en résumé :
1. OUI, la méthode présentée par réduction à HORN-SAT était en l'état incomplète et avait en l'état des contre-exemples.
2. OUI, en l'état, on n'avait donc pas l'implication $cons(H)\implies cons(F)$ puisqu'il y avait (au moins) un CE
3. OUI, la méthode était en cours de complétion...dans mon esprit et dans les notes successives.
4. OUI, la méthode a été complétée dans la nouvelle série de notes "comp..."
5. OUI, les contre-exemples n'en sont plus avec cette complétion. -
encore quelques petits exercices pour apprendre à pratiquer la méthode.
-
Merci pour ta réponse!Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
En attendant une preuve formelle par Coq, voici une ébauche de preuve manuelle.....
-
Juste pour dire que rien n'a changé dans ma disponibilité. Je n'ai pas le temps de lire les choses que tu as mises depuis ton doc initial. Sache que ce forum est actif, mais tout de même pas au point de fournir des réponses techniques à la vitesse de plusieurs item/(jour ×intervenant) sur des trucs pointus.
Je te souhaite que le WE apporte des réactions.
J'ai cliqué sur "ouvrir" pour ton dernier post: je vois "rough", "rough", "rough" partout. Je vais essayer de te faire comprendre un truc sur les mentalités:
1/ Tu annonces la plus importante découverte de tous les temps avec un coeur de preuve (correct) de 5 lignes où l'admis est faux.
2/ Tu réagis avec une parfaite honnêteté puisque c'est toi-même qui casse ton propre admis (je parle de l'initial cons(H)=>cons(F)).
3/ Depuis, tu as transformé la discussion en "je pense que l'idée est bonne et je vous "rough-dis" pourquoi.
4/ Evidemment, d'éventuels engouements initiaux ont totalement disparu puisque sur un résultat qui vaut 10^15 euros sur le marché (et qui changerait TOTALEMENT LE MONDE en 30ans), une invitation à une "rugh-discussion" en vue d'améliorer un non-rough admis faux devient une invitation à se faire un nouvel ami pour des piques-nique sympas et des cinémas ensemble. Je pense que tu auras des gens qui vont te répondre, mais qu'ils ne le ferontpas forcément avant le WE.
5/ J'ai écrit une thèse sur justement la classification des complexités de choses de ce genre (ie le fait qu'insoupçonnablement des injections virtuelles de 7 dans 6 par exemple, ont telles et telles différences qualitatives fortes et "par nature" avec telles autres) et il n'y a pas de motivation (mais j'insiste je n'ai rien lu, juste ton contre-exemple et l'article initial) ni d'espérance pour moi à penser que la chasse au contre-exemple que tu as trouvé, en l'évitant par une amélioration X, va suffire à exclure des contre-exemples bcp plus vicieux.
L'injection virtuelle que H croit exister mais pas F (ton premier contre-exemple) est DEJA un truc très puissant (dans ma thèse il est non casino inoffensif ET fini). Personnellement, des H", puis des H'' qui vont ne plus accepter injvirt(9,8) peuvent tout à fait accepter des magies bien moins fortes.
6/ En espérant t'avoir exprimé clairement mon ressenti. Mais si je peux, je lirai tes améliorations (à 10^15 euros et proba de 10^(-7) que tu aies raison, ça vaut 10^8 soit 100000000 d'euros de jouer :-D )Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@Christophe
Merci, j'ai bien compris ton ressenti que tu exprimes assez clairement.
Au sujet des "rough", c'est très relatif....j'explique.
pour ce qui est de la complexité, écrire $O(N^{12})$ est une notation standard en théorie de la complexité...ça veut dire asymptotiquement et à un facteur constant près. Pas besoin d'en dire plus pour dire que c'est dans la classe $P$.
pour ce qui est de la correction, là en effet, c'est moins précis. Je donne juste l'idée car j'ai bien compris que de toute façon il va falloir passer par une preuve par Coq et que si j'explique en 3 lignes ou en 300 pages, cela ne changera rien aux attentes "modernes".
pour ce qui est du reste, ma façon de fonctionner n'est pas standard et cela peut être dérangeant. J'ai du mal à me faire comprendre, j'ai du mal à comprendre les preuves trop formelles, ce qui est simple pour certains peut me sembler difficile et vice-versa.
pour ce qui est de ta thèse, c'est très intéressant...c'était dans quel domaine ? En logique ? En épistémologie ?
Merci encore pour tes messages,
Bon week-end. -
@Christophe
Bon, j'ai fait un peu bosser mon cerveau....
Alors voilà des preuves plus formelles (avec moins de "rough").
Est-ce que Coq peut faire ce genre de preuves ? Ce serait quand même vraiment balèze ! J'ai du mal à y croire.....
PS : je viens d'apprendre ici pour Patrick Dehornoy.....triste....j'ai mis un mot. Mais alors...on se connait ? -
Alors voici une note "quasi-complète"...mais c'est très relatif la complétude.
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.1K Toutes les catégories
- 7 Collège/Lycée
- 21.8K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 52 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 62 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 312 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 771 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 4
+3 Invités