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.

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.

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

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.

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

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]

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.

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).

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.

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.

C ++

Voici une solution dont l'exécution est garantie en temps polynomial: elle s'exécute O(n^k)où 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;
  }
}

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

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
}