Alors évidemment, P = NP [fermé]

111

SAT est le problème de déterminer si une expression booléenne peut être rendue vraie. Par exemple, (A) peut être rendu vrai en définissant A = TRUE, mais (A &&! A) ne peut jamais être vrai. Ce problème est connu pour être NP-complet. Voir Satisfaiabilité booléenne .

Votre tâche consiste à écrire un programme pour SAT qui s’exécute en temps polynomial, mais ne résout pas tous les cas.

Pour certains exemples, la raison pour laquelle ce n'est pas vraiment polynomial pourrait être parce que:

  1. Il y a un cas de bord qui n'est pas évident mais dont le temps d'exécution est faible
  2. L'algorithme ne résout pas le problème dans certains cas inattendus
  3. Certaines fonctionnalités du langage de programmation que vous utilisez ont une durée d’exécution plus longue que celle à laquelle vous pouvez raisonnablement vous attendre.
  4. Votre code fait en réalité quelque chose de totalement différent de ce à quoi il ressemble

Vous pouvez utiliser n’importe quel langage de programmation (ou combinaison de langues) de votre choix. Vous n'avez pas besoin de fournir une preuve formelle de la complexité de votre algorithme, mais vous devez au moins fournir une explication.

Le critère principal pour juger devrait être de savoir comment convaincre le code.

Il s’agit d’un concours de popularité, la réponse la mieux notée de la semaine l’emporte.

Jonathan Pullano
la source
11
Ce serait mieux si vous limitiez le domaine problématique, sinon vous appelez le nuage d'incertitude autour de ce qui est "bien connu". Pourquoi ne pas choisir un seul problème NP-difficile et se concentrer sur cela? Cela présente l’avantage de laisser d’autres problèmes de ce type ouverts aux questions futures dans le même sens. Plusieurs questions étroites peuvent fournir beaucoup plus de plaisir et de divertissement au site qu’un grand.
Jonathan Van Matre
9
@ gnasher729: J'ai eu le compilateur C # pour résoudre un problème SAT; Je considère cela comme une réalisation raisonnablement intéressante.
Eric Lippert
9
Ce serait amusant si quelqu'un résout accidentellement SAT en temps polynomial ici.
Turion
5
@Turion, des décennies de recherche, des millions de récompenses et de prix, ainsi que toutes les femmes et la renommée que l'on pourrait avoir - mais la véritable motivation pour résoudre P = NP finira par être ce défi PCG.
NothingsImpossible
3
Je vote pour clore cette question hors sujet, car les défis sournois ne sont plus les bienvenus sur ce site. meta.codegolf.stackexchange.com/a/8326/20469
cat.

Réponses:

236

C #

Votre tâche consiste à écrire un programme pour SAT qui semble s’exécuter en temps polynomial.

"Apparaît" est inutile. Je peux écrire un programme qui s'exécute vraiment en temps polynomial pour résoudre les problèmes SAT. C'est assez simple en fait.

MEGA BONUS: Si vous écrivez un solveur SAT qui s'exécute réellement en temps polynomial, vous obtenez un million de dollars! Mais utilisez quand même une balise spoiler pour que les autres puissent s’interroger.

Impressionnant. S'il vous plaît envoyez-moi le million de dollars. Sérieusement, j'ai un programme ici qui résoudra SAT avec une exécution polynomiale.

Permettez-moi de commencer par dire que je vais résoudre une variante du problème SAT. Je vais vous montrer comment écrire un programme qui présente la solution unique à tout problème 3-SAT . La valorisation de chaque variable booléenne doit être unique pour que mon solveur fonctionne.

Nous commençons par déclarer quelques méthodes et types d’aide simples:

class MainClass
{
    class T { }
    class F { }
    delegate void DT(T t);
    delegate void DF(F f);
    static void M(string name, DT dt)
    {
        System.Console.WriteLine(name + ": true");
        dt(new T());
    }
    static void M(string name, DF df)
    {
        System.Console.WriteLine(name + ": false");
        df(new F());
    }
    static T Or(T a1, T a2, T a3) { return new T(); }
    static T Or(T a1, T a2, F a3) { return new T(); }
    static T Or(T a1, F a2, T a3) { return new T(); }
    static T Or(T a1, F a2, F a3) { return new T(); }
    static T Or(F a1, T a2, T a3) { return new T(); }
    static T Or(F a1, T a2, F a3) { return new T(); }
    static T Or(F a1, F a2, T a3) { return new T(); }
    static F Or(F a1, F a2, F a3) { return new F(); }
    static T And(T a1, T a2) { return new T(); }
    static F And(T a1, F a2) { return new F(); }
    static F And(F a1, T a2) { return new F(); }
    static F And(F a1, F a2) { return new F(); }
    static F Not(T a) { return new F(); }
    static T Not(F a) { return new T(); }
    static void MustBeT(T t) { }

Maintenant, choisissons un problème 3-SAT à résoudre. Disons

(!x3) & 
(!x1) & 
(x1 | x2 | x1) & 
(x2 | x3 | x2)

Mettons cela un peu plus entre parenthèses.

(!x3) & (
    (!x1) & (
        (x1 | x2 | x1) & 
        (x2 | x3 | x2)))

Nous encodons cela comme ceci:

static void Main()
{
    M("x1", x1 => M("x2", x2 => M("x3", x3 => MustBeT(
      And(
        Not(x3),
        And(
          Not(x1),
          And(
            Or(x1, x2, x1),
            Or(x2, x3, x2))))))));
}

Et bien sûr, lorsque nous exécutons le programme, nous obtenons une solution à 3-SAT en temps polynomial. En fait, le temps d'exécution est linéaire dans la taille du problème !

x1: false
x2: true
x3: false

Vous avez dit exécution polynomiale . Vous n'avez rien dit sur le temps de compilation polynomial . Ce programme oblige le compilateur C # à essayer toutes les combinaisons de types possibles pour x1, x2 et x3 et à choisir la combinaison unique qui ne présente aucune erreur de type. Le compilateur fait tout le travail, le runtime n'est donc pas obligé. J'ai d'abord exposé cette technologie intéressante sur mon blog en 2007: http://blogs.msdn.com/b/ericlippert/archive/2007/03/28/lambda-expressions-vs-anonymous-methods-part-five.aspx Note Bien entendu, cet exemple montre que la résolution de surcharge en C # est au moins NP-HARD. Que ce soit NP-HARD ou réellement indécidable Cela dépend de certains détails subtils du fonctionnement de la convertibilité des types en présence de contravariance générique, mais c'est un sujet pour un autre jour.

Eric Lippert
la source
95
Vous devrez contacter l'institut de mathématiques pour l'argile pour votre million de dollars. Mais je ne suis pas sûr qu'ils seront satisfaits .
Jonathan Pullano
15
Bien entendu, tout problème SAT peut être transformé en un problème équivalent à 3 SAT, cette restriction n’est donc qu’un inconvénient. Le problème le plus épineux avec ma "solution" est que cela nécessite que le problème ait une solution unique . S'il n'y a pas de solution ou plus d'une solution, le compilateur génère une erreur.
Eric Lippert
11
@EricLippert l'exigence d'unicité est ok. Vous pouvez toujours réduire SAT à Unique-SAT (SAT mais en supposant que les entrées ont 0 ou 1 affectation) en utilisant une réduction aléatoire polynomiale. Mots-clés: Lemme d'isolement, théorème de Valiant-Vazirani.
Diego de Estrada
44
"Sérieusement, j'ai un programme ici qui résoudra SAT avec une exécution polynomiale." - moi aussi, mais malheureusement cela ne rentre pas dans cette boîte de commentaire.
CompuChip
11
@ Kobi: Oui, c'est la blague.
Eric Lippert
166

Multi-langue (1 octet)

Le programme suivant, valable dans de nombreuses langues, principalement fonctionnelle et ésotérique, donnera la réponse correcte à un grand nombre de problèmes SAT et présente une complexité constante (!!!):

0

Étonnamment, le prochain programme donnera la bonne réponse à tous les problèmes restants et aura la même complexité. Il vous suffit donc de choisir le bon programme et vous aurez la bonne réponse dans tous les cas!

1
Mau
la source
6
Ceci est incroyable. Je me suis bien marré.
Karl Damgaard Asmussen
2
Absolument génial!
Le chien bleu
78
Hmm. C'est facile maintenant. Tout ce que j'ai à faire est d'écrire un programme qui choisira le bon programme!
Cruncher
Précisément ! :-)
Mau
6
Réminiscent de xkcd.com/221 .
msh210
34

JavaScript

En utilisant le non-déterminisme itéré, SAT peut être résolu en temps polynomial!

function isSatisfiable(bools, expr) {
    function verify() {
        var values = {};
        for(var i = 0; i < bools.length; i++) {
            values[bools[i]] = nonDeterministicValue();
        }
        with(values) {
            return eval(expr);
        }
    }
    function nonDeterministicValue() {
        return Math.random() < 0.5 ? !0 : !1;
    }

    for(var i = 0; i < 1000; i++) {
        if(verify(bools, expr)) return true;
    }
    return false;
}

Exemple d'utilisation:

isSatisfiable(["a", "b"], "a && !a || b && !b") //returns 'false'

Cet algorithme vérifie mille fois la formule booléenne donnée avec des entrées aléatoires. Presque toujours, cela fonctionne pour de petites entrées, mais est moins fiable lorsque plus de variables sont introduites.

En passant, je suis fier d’avoir eu l’occasion d’utiliser deux des fonctionnalités les plus sous-utilisées de JavaScript, les unes à côté des autres: evalet with.

Peter Olson
la source
4
C'est en fait une méthode de test bien établie. La bibliothèque QuickCheck de Haskell a commencé tout le plaisir, je crois. Il a depuis été réimplanté dans de nombreuses langues.
John Tyree
4
Je pense qu'il convient de noter que, ce programme est moins susceptible de renvoyer la réponse correcte, plus l'expression sat est grande. La 1000boucle for devrait en quelque sorte être mise à l'échelle avec la taille d'entrée (une mise à l'échelle polynomiale non-O (1)).
Cruncher
2
@Cruncher Pour être plus précis, plus le nombre de variables est important, moins il est probable qu'il renvoie la réponse correcte. (par exemple, une très longue expression avec une seule variable retournera presque toujours la bonne réponse)
Peter Olson
2
@ TimSeguine, je reconnais que l'utilisation du mot "non déterministe" dans ce contexte est pour le moins douteuse, tout comme l'affirmation selon laquelle la SAT peut être résolue en temps polynomial. Je sais que ce n'est pas correct, cela fait simplement partie du jeu de la tromperie.
Peter Olson
4
@PaulDraper et appelez-les ensuite sous-utilisés! J'ai bien rigolé!
Rob
32

Mathematica + Informatique quantique

Vous ne savez peut-être pas que Mathematica est livré avec un ordinateur quantique

Needs["Quantum`Computing`"];

Quantum Adiabatic Commputing encode un problème à résoudre dans un hamiltonien (opérateur énergétique) de telle sorte que son état d'énergie minimale ("état fondamental") représente la solution. Par conséquent, l'évolution adiabatique d'un système quantique à l'état fondamental de l'hamiltonien et les mesures subséquentes constituent la solution au problème.

Nous définissons un subhamiltonien qui correspond à des ||parties de l'expression, avec une combinaison appropriée d'opérateurs de Pauli pour les variables et sa négation

entrez la description de l'image ici

Où pour l'expression comme ça

expr = (! x3) && (! x1) && (x1 || x2 || x1) && (x2 || x3 || x2);

l'argument devrait ressembler à

{{{1, x3}}, {{1, x1}}, {{0, x1}, {0, x2}, {0, x1}}, {{0, x2}, {0, x3}, {0, x2}}}

Voici le code pour construire un tel argument à partir d'une expression bool:

arg = expr /. {And -> List, Or -> List, x_Symbol :> {0, x}, 
    Not[x_Symbol] :> {1, x}};
If[Depth[arg] == 3, arg = {arg}];
arg = If[Depth[#] == 2, {#}, #] & /@ arg

Maintenant, nous construisons un hamiltonien complet, résumant les subhamiltoniens (la somme correspond à des &&parties de l'expression)

H = h /@ arg /. List -> Plus;

Et recherchez l'état d'énergie le plus bas

QuantumEigensystemForm[H, -1]

entrez la description de l'image ici

Si nous obtenons une valeur propre égale à zéro, le vecteur propre est la solution

expr /. {x1 -> False, x2 -> True, x3 -> False}
> True

Malheureusement, le site officiel du module complémentaire "Quantum Computing" n’est pas actif et je ne trouve pas d’emplacement pour le télécharger, je l’avais toujours installé sur mon ordinateur. L'add-on a également une solution documentée au problème SAT, sur laquelle j'ai basé mon code.

bruissement
la source
19
Je ne sais pas du tout comment cette réponse fonctionne. +1
Jonathan Pullano
5
@XiaogeSu "Naturellement".
Swish
3
@XiaogeSu Evolution déterminée par l'hamiltonien et évolue naturellement vers l'énergie la plus basse. Donc, connaissant le spectre, nous pouvons supposer que le système se retrouvera dans l'état fondamental.
Swish
3
@XiaogeSu Pour passer à l'état fondamental, il faut également avoir une interaction avec l'environnement qui désexcite les états supérieurs, vous avez raison. L'idée ici est que cette interaction est très petite, "adiabatique".
Turion
3
Le calcul QM adiabatique fyi présente de nombreuses similitudes avec le recuit simulé classique . maintenant implémenté par Dwave . son semblable à un système de refroidissement / température "de refroidissement" qui "trouve / installe" dans les minima locaux .
vzn
27

Trois approches ici impliquent toutes une réduction de la SAT dans sa lingua franca géométrique 2D: énigmes de la logique des non-graphiques. Les cellules du puzzle logique correspondent aux variables SAT, contraintes aux clauses.

Pour une explication complète (et pour vérifier les bogues dans mon code!), J'ai déjà publié des informations sur les modèles dans l'espace des solutions de nonogram. Voir https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space. L'énumération de plus de 4 milliards de solutions de casse-tête et leur codage pour tenir dans une table de vérité montrent des schémas fractals - auto-similarité et surtout auto-affinité. Cette redondance affine démontre la structure du problème, exploitable pour réduire les ressources informatiques nécessaires à la génération de solutions. Cela montre également la nécessité d'un retour d'information chaotique au sein de tout algorithme réussi. Il existe un pouvoir explicatif dans le comportement de transition de phase, où les instances "faciles" sont celles qui se trouvent le long de la structure grossière, tandis que les instances "dures" nécessitent une itération plus poussée dans les moindres détails, assez cachées des heuristiques normales. Si vous souhaitez zoomer dans le coin de cette image infinie (toutes les <= 4x4 casse-têtes codés), voir http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html

Méthode 1. Extrapolez l’ombre de l’espace de la solution de nonogramme à l’aide de cartes chaotiques et d’apprentissage automatique (pensez à des fonctions d’ajustement semblables à celles qui génèrent l’ensemble de Mandelbrot).

http://i.stack.imgur.com/X7SbP.png

Voici une preuve visuelle de l'induction. Si vous pouvez numériser ces quatre images de gauche à droite en pensant que vous avez une bonne idée de générer les images manquantes de la 5ème ... 6ème ... etc., je viens de vous programmer que mon oracle NP pour le problème de la décision de la solution Nonogram existence. Veuillez vous présenter pour réclamer votre prix en tant que supercalculateur le plus puissant au monde. Je vous nourrirai d’électricité de temps en temps pendant que le monde vous remercie pour vos contributions en calcul.

Méthode 2. Utilisez des transformations de Fourier sur la version image booléenne des entrées. Les FFT fournissent des informations globales sur la fréquence et la position dans une instance. Bien que la partie de magnitude devrait être similaire entre les paires d’entrée, leur information de phase est complètement différente - contenant des informations directionnelles sur une projection de solution le long d’un axe spécifique. Si vous êtes assez intelligent, vous pouvez reconstruire l'image de phase de la solution. superposant les images de phase en entrée. Ensuite, inversez la phase et la magnitude commune dans le domaine temporel de la solution.

Qu'est-ce que cette méthode pourrait expliquer? Il existe de nombreuses permutations des images booléennes avec un remplissage flexible entre les exécutions contiguës. Cela permet un mappage entre entrée -> solution en prenant en compte la multiplicité tout en conservant la propriété des mappages bidirectionnels et uniques de la FFT entre le domaine temporel <-> (fréquence, phase). Cela signifie également qu’il n’existe pas de solution «sans solution». Ce que cela indiquerait, c'est que dans un cas continu, il existe des solutions en niveaux de gris que vous n'envisagez pas lorsque vous examinez l'image à deux niveaux de la résolution de casse-tête traditionnelle avec un nonogramme.

Pourquoi tu ne le ferais pas? C'est une façon horrible de calculer, car les FFT dans le monde actuel à virgule flottante seraient très imprécises avec de grandes instances. La précision est un énorme problème et reconstruire des images à partir d’images de magnitude et de phase quantifiées crée généralement des solutions très approximatives, bien que peut-être pas visuellement. pour les seuils de l’œil humain. Il est également très difficile de trouver cette activité de superposition, car le type de fonction qui le fait est actuellement inconnu. S'agirait-il d'un système de moyenne simple? Probablement pas, et il n'y a pas de méthode de recherche spécifique pour le trouver, sauf l'intuition.

Méthode 3 Recherchez une règle d'automate cellulaire (sur environ 4 milliards de tables de règles pour les règles de von Neumann à 2 états) qui résout une version symétrique du casse-tête du nonogramme. Vous utilisez une intégration directe du problème dans des cellules, illustrée ici. Nonogrammes symétriques conservateurs

C'est probablement la méthode la plus élégante, en termes de simplicité et d'effets positifs pour l'avenir de l'informatique. L'existence de cette règle n'est pas prouvée, mais j'ai l'intuition qu'elle existe. Voici pourquoi:

Les nonogrammes nécessitent beaucoup de réactions chaotiques dans l'algorithme pour être résolus avec précision. Ceci est établi par le code de force brute lié à la révision du code. CA est à peu près le langage le plus apte à programmer des retours chaotiques.

Cela semble juste, visuellement. La règle évoluerait à travers une incorporation, propagerait les informations horizontalement et verticalement, interférerait puis se stabiliserait à une solution conservant le nombre de cellules définies. Cet itinéraire de propagation suit le chemin (en arrière) auquel vous pensez normalement lorsque vous projetez l'ombre d'un objet physique dans la configuration d'origine. Les nonogrammes dérivent d'un cas particulier de tomographie discrète. Imaginez donc que vous êtes assis simultanément dans deux tomodensitomètres à coin de chat. C'est ainsi que les rayons X se propageraient pour générer les images médicales. Bien entendu, il existe des problèmes de limites: les bords de l'univers CA ne peuvent pas continuer à propager des informations au-delà des limites, sauf si vous autorisez un univers toroïdal. Cela pose également le casse-tête comme un problème périodique de valeur limite.

Il explique plusieurs solutions sous forme d'états transitoires dans un effet d'oscillation continue entre les sorties d'échange en entrées et inversement. Il explique les instances sans solution en tant que configurations d'origine qui ne conservent pas le nombre de cellules définies. En fonction du résultat réel de la découverte d'une telle règle, elle peut même se rapprocher des instances insolubles avec une solution proche dans laquelle les états des cellules sont conservés.

Communauté
la source
2
+1 pour m'avoir laissé dire "pourquoi n'y ai-je pas pensé?" : P
Navin
Vous êtes Stephen Wolfram et je réclame mes cinq livres!
Quuxplusone
4
Cette réponse mérite vraiment plus de crédit, car c'est la meilleure tentative pour créer un programme convaincant . Bon spectacle.
Jonathan Pullano
10

C ++

Voici une solution dont l'exécution est garantie en temps polynomial: elle s'exécute O(n^k)nest le nombre de booléens et kest une constante de votre choix.

Il est heuristically correct, que je crois CS-parler pour « lui donne la bonne réponse la plupart du temps, avec un peu de chance » (et, dans ce cas, une façon appropriée à grande valeur k- modifier pour moi , il a effectivement eu lieu que pour tout fixe, nvous pouvez définir ktel que n^k > 2^n- est-ce la tricherie?).

#include <iostream>  
#include <cstdlib>   
#include <time.h>    
#include <cmath>     
#include <vector>    

using std::cout;     
using std::endl;     
typedef std::vector<bool> zork;

// INPUT HERE:

const int n = 3; // Number of bits
const int k = 4; // Runtime order O(n^k)

bool input_expression(const zork& x)
{
  return 
  (!x[2]) && (
    (!x[0]) && (
      (x[0] || x[1] || x[0]) &&
      (x[1] || x[2] || x[1])));
}

// MAGIC HAPPENS BELOW:    

 void whatever_you_do(const zork& minefield)
;void always_bring_a_towel(int value, zork* minefield);

int main()
{
  const int forty_two = (int)pow(2, n) + 1;
  int edition = (int)pow(n, k);
  srand(time(6["times7"]));

  zork dont_panic(n);
  while(--edition)
  {
    int sperm_whale = rand() % forty_two;
    always_bring_a_towel(sperm_whale, &dont_panic);

    if(input_expression(dont_panic))
    {
      cout << "Satisfiable: " << endl;
      whatever_you_do(dont_panic);
      return 0;
    }
  }

  cout << "Not satisfiable?" << endl;
  return 0;
}
void always_bring_a_towel(int value, zork* minefield)
{
  for(int j = 0; j < n; ++j, value >>= 1)
  {
    (*minefield)[j] = (value & 1);
  }
}

void whatever_you_do(const zork& minefield)
{
  for(int j = 0; j < n; ++j) 
  {
    cout << (char)('A' + j) << " = " << minefield[j] << endl;
  }
}
CompuChip
la source
Bonne réponse. Je mettrais l'explication dans une étiquette spoiler pour que les gens puissent la regarder et se gratter la tête un peu.
Jonathan Pullano
Merci pour la suggestion @JonathanPullano, j'ai ajouté une balise spoiler et obscurci un peu le code.
CompuChip
En passant, je viens juste d’apprendre bitfield, j’aurais peut-être préféré cela plus longtemps std::vector.
CompuChip
3
+1 pour les références à l'obfuscation créative et aux auto-stoppeurs
Blake Miller
2
Oui bien sûr c'est de la triche, si k dépend de n ce n'est pas vraiment une constante :-)
RemcoGerlich
3

surface 3d ruby ​​/ gnuplot

(ooh concurrence acharnée!) ... de toute façon ... une image vaut-elle mille mots? Ce sont 3 parcelles de surface distinctes réalisées dans gnuplot du point de transition SAT. les axes (x, y) sont la clause et le nombre de variables et la hauteur z est le nombre total d'appels récursifs dans le résolveur. code écrit en rubis. il échantillonne 10x10 points à 100 échantillons chacun. il démontre / utilise les principes de base de la statistique et est une simulation de Monte Carlo .

il s’agit essentiellement d’un algorithme davis putnam s’appuyant sur des instances aléatoires générées au format DIMACS. C’est le type d’exercice qui devrait idéalement être pratiqué dans les classes CS du monde entier afin que les étudiants puissent apprendre les bases, mais n’est presque pas enseigné de manière spécifique… peut-être une raison pour laquelle il existe autant de preuves fictives P? = NP ? il n'y a même pas un bon article de wikipedia décrivant le phénomène de point de transition (qui prône?) qui est un sujet très important en physique statistique et qui est également essentiel en CS. [a] [b] il existe de nombreux articles en CS sur le point de transition cependant très peu semblent montrer des parcelles de surface! (à la place, montrant généralement des tranches 2D.)

l'augmentation exponentielle de la durée d'exécution est clairement évidente dans le 1 er graphique. la selle au milieu du 1 er tracé est le point de transition. les deuxième et troisième tracés montrent le pourcentage de transition satisfaisable.

[a] comportement de transition de phase dans les ppt CS Toby Walsh
[b] probabilité empirique de satisfabilité de k-SAT tcs.se
[c] grands moments dans les mathématiques empiriques / expérimentales / (T) CS / SAT , TMachine blog

entrez la description de l'image ici entrez la description de l'image ici entrez la description de l'image ici

P =? NP QED!

#!/usr/bin/ruby1.8

def makeformula(clauses)
    (1..clauses).map \
    {
            vars2 = $vars.dup
            (1..3).map { vars2.delete_at(rand(vars2.size)) * [-1, 1][rand(2)] }.sort_by { |x| x.abs }
    }

end

def solve(vars, formula, assign)

    $counter += 1
    vars2 = []
    formula.each { |x| vars2 |= x.map { |y| y.abs } }
    vars &= vars2

    return [false] if (vars.empty?)
    v = vars.shift
    [v, -v].each \
    {
            |v2|
            f2 = formula.map { |x| x.dup }
            f2.delete_if \
            {
                    |x|
                    x.delete(-v2)
                    return [false] if (x.empty?)
                    x.member?(v2)
            }
            return [true, assign + [v2]] if (f2.empty?)
            soln = solve(vars.dup, f2, assign + [v2])
            return soln if (soln[0])
    }
    return [false]
end

def solve2(formula)
    $counter = 0
    soln = solve($vars.dup, formula, [])
    return [$counter, {false => 0, true => 1}[soln[0]]]
end


c1 = 10
c2 = 100
nlo, nhi = [3, 10]
mlo, mhi = [1, 50]
c1.times \
{
    |n|
    c1.times \
    {
            |m|
            p1 = nlo + n.to_f / c1 * (nhi - nlo)
            p2 = mlo + m.to_f / c1 * (mhi - mlo)
            $vars = (1..p1.to_i).to_a
            z1 = 0
            z2 = 0
            c2.times \
            {
                    f = makeformula(p2.to_i)
                    x = solve2(f.dup)
                    z1 += x[0]
                    z2 += x[1]
            }
#           p([p1, p2, z1.to_f / c2, z2.to_f / c2]) # raw
#           p(z1.to_f / c2)                         # fig1
#           p(0.5 - (z2.to_f / c2 - 0.5).abs)       # fig2
            p(z2.to_f / c2)                         # fig3
    }
    puts
}
vzn
la source
2
Je suis content que vous ayez contribué à cette réponse. Dans toute démonstration réussie de P contre NP (dans les deux cas), il s'agit de l'une des nombreuses exigences du pouvoir prédictif. Merci d'avoir souligné son importance. :)
plus de rêveries sur P vs NP , beaucoup de références top / collectées, etc.
vzn