Dans SODA 1995 , Jeff Erickson a montré des limites inférieures pour la satisfiabilité linéaire (vérifier si un certain ensemble de n nombres réels satisfait une équation linéaire sur r variables). La méthode de preuve utilise des infinitésimales et le principe de transfert de Tarski .
Quelqu'un pourrait-il expliquer l'intuition derrière la route prise pour prouver cette limite? Quelle est la difficulté de trouver une preuve directe comme celle-ci: "Étant donné un arbre de décision qui prend des nombres réels, voici comment nous pouvons construire une entrée contradictoire"?
Réponses:
Je suggère fortement de lire le document de suivi le plus récent d'Ailon et Chazelle , qui évite entièrement le problème infinitésimal. Si vous voulez vous en tenir à mon article, veuillez lire la version du journal ( Chicago J Theoretical Computer Science 1999 ). La version SODA a un bug majeur dans la section 5, et (je pense) la version du journal explique la preuve principale beaucoup plus clairement.
la source
En effet, l'argument principal est de construire un arbre de décision et de concevoir des entrées contradictoires, mais il y a des problèmes techniques à ce sujet que les infinitésimaux évitent. Regardez la discussion au bas de la première colonne de la page 2 et continuez, ce qui explique cela assez clairement.
la source