SAT ist das Problem zu bestimmen, ob ein boolescher Ausdruck wahr gemacht werden kann. Zum Beispiel kann (A) durch Setzen von A = TRUE wahr gemacht werden, aber (A &&! A) kann niemals wahr sein. Es ist bekannt, dass dieses Problem NP-vollständig ist. Siehe Boolesche Zufriedenheit .

Ihre Aufgabe ist es, ein Programm für SAT zu schreiben, das in Polynomialzeit ausgeführt wird, aber möglicherweise nicht alle Fälle löst.

Für einige Beispiele könnte der Grund dafür, dass es nicht wirklich polynomisch ist, sein, dass:

1. Es gibt einen Randfall, der nicht offensichtlich ist, aber eine schlechte Laufzeit hat
2. Der Algorithmus kann das Problem in unerwarteten Fällen nicht lösen
3. Einige Funktionen der von Ihnen verwendeten Programmiersprache haben tatsächlich eine längere Laufzeit, als Sie vernünftigerweise erwarten würden
4. Ihr Code macht tatsächlich etwas völlig anderes, als es aussieht

Sie können eine beliebige Programmiersprache (oder eine Kombination von Sprachen) verwenden. Sie müssen keinen formalen Beweis für die Komplexität Ihres Algorithmus liefern, aber Sie sollten zumindest eine Erklärung liefern.

Das Hauptkriterium für die Beurteilung sollte sein, wie überzeugend der Code ist.

Dies ist ein Beliebtheitswettbewerb, daher gewinnt die bestbewertete Antwort in einer Woche.

C #

Ihre Aufgabe ist es, ein Programm für SAT zu schreiben, das in polynomialer Zeit ausgeführt wird.

"Erscheint" ist nicht erforderlich. Ich kann ein Programm schreiben, das wirklich in Polynomialzeit ausgeführt wird, um SAT-Probleme zu lösen. Das ist in der Tat ganz einfach.

MEGA BONUS: Wenn Sie einen SAT-Solver schreiben, der tatsächlich in Polynomialzeit ausgeführt wird, erhalten Sie eine Million Dollar! Aber bitte benutzen Sie trotzdem ein Spoiler-Tag, damit andere sich darüber wundern können.

Genial. Bitte senden Sie mir die Millionen Dollar. Im Ernst, ich habe genau hier ein Programm, das SAT mit polynomialer Laufzeit löst.

Lassen Sie mich zunächst feststellen, dass ich eine Variation des SAT-Problems lösen werde. Ich werde zeigen, wie man ein Programm schreibt, das die einzigartige Lösung eines 3-SAT-Problems zeigt . Die Bewertung jeder Booleschen Variablen muss eindeutig sein, damit mein Solver funktioniert.

Wir beginnen mit der Deklaration einiger einfacher Hilfsmethoden und -typen:

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) { }

Lassen Sie uns nun ein 3-SAT-Problem auswählen, das gelöst werden soll. Sagen wir

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

Lassen Sie uns das ein bisschen näher erläutern.

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

Wir kodieren das so:

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))))))));
}

Und wenn wir das Programm ausführen, erhalten wir eine Lösung für 3-SAT in Polynomialzeit. Tatsächlich ist die Laufzeit in der Größe des Problems linear !

x1: false
x2: true
x3: false

Sie sagten Polynomlaufzeit . Sie haben nichts über die Kompilierungszeit des Polynoms gesagt . Dieses Programm zwingt den C # -Compiler, alle möglichen Typkombinationen für x1, x2 und x3 auszuprobieren und die eindeutige zu wählen, die keine Typfehler aufweist. Der Compiler erledigt die ganze Arbeit, die Laufzeit muss also nicht. Ich habe diese interessante Technik erstmals 2007 in meinem Blog vorgestellt: http://blogs.msdn.com/b/ericlippert/archive/2007/03/28/lambda-expressions-vs-anonymous-methods-part-five.aspx Hinweis Das Beispiel zeigt natürlich, dass die Überlastungsauflösung in C # mindestens NP-HARD ist. Ob es NP-HARD oder tatsächlich unentscheidbar ist Es hängt von bestimmten Details ab, wie die Typkonvertierbarkeit bei generischer Kontravarianz funktioniert, aber das ist ein Thema für einen anderen Tag.

Mehrsprachig (1 Byte)

Das folgende Programm, das in vielen Sprachen gültig ist, meistens funktional und esoterisch, wird die richtige Antwort für eine große Anzahl von SAT-Problemen geben und hat eine konstante Komplexität (!!!):

0

Erstaunlicherweise gibt das nächste Programm die richtige Antwort auf alle verbleibenden Probleme und hat dieselbe Komplexität. Sie müssen also nur das richtige Programm auswählen und haben in jedem Fall die richtige Antwort!

1

JavaScript

Durch die Verwendung von iteriertem Nichtdeterminismus kann SAT in Polynomialzeit gelöst werden!

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;
}

Anwendungsbeispiel:

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

Dieser Algorithmus überprüft eine gegebene Boolesche Formel nur tausendmal mit zufälligen Eingaben. Funktioniert fast immer für kleine Eingaben, ist jedoch weniger zuverlässig, wenn mehr Variablen eingeführt werden.

Ich bin übrigens stolz darauf, dass ich die Gelegenheit hatte, zwei der am wenigsten genutzten Funktionen von JavaScript direkt nebeneinander zu nutzen: evalund with.

Mathematica + Quantencomputing

Möglicherweise wissen Sie nicht, dass Mathematica mit einem Quantencomputer ausgestattet ist

Needs["Quantum`Computing`"];

Quantum Adiabatic Commputing codiert ein in einem Hamilton-Operator (Energieoperator) zu lösendes Problem so, dass sein Zustand der minimalen Energie ("Grundzustand") die Lösung darstellt. Die adiabatische Evolution eines Quantensystems in den Grundzustand des Hamiltonschen und die anschließende Messung liefert daher die Lösung des Problems.

Wir definieren einen Subhamilton, der ||Teilen des Ausdrucks entspricht, mit einer geeigneten Kombination von Pauli-Operatoren für Variablen und deren Negation

Wo zum Ausdruck so

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

Das Argument sollte so aussehen

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

Hier ist der Code, um ein solches Argument aus dem bool-Ausdruck zu konstruieren:

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

Jetzt konstruieren wir einen vollständigen Hamilton-Operator, der die Subhamiltonen summiert (die Summation entspricht &&Teilen des Ausdrucks).

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

Und suchen Sie nach dem niedrigsten Energiezustand

QuantumEigensystemForm[H, -1]

Wenn wir einen Eigenwert von Null haben, ist der Eigenvektor die Lösung

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

Leider ist die offizielle Seite für das Add-On "Quantum Computing" nicht aktiv und ich kann keinen Ort zum Herunterladen finden. Ich habe es gerade noch auf meinem Computer installiert. Das Add-on hat auch eine dokumentierte Lösung für das SAT-Problem, auf der ich meinen Code basierte.

Drei Herangehensweisen beinhalten alle eine Reduktion von SAT in seine 2D-geometrische Verkehrssprache: Nicht-Programm-Logik-Rätsel. Zellen im Logikrätsel entsprechen SAT-Variablen, Nebenbedingungen zu Klauseln.

Für eine vollständige Erklärung (und um meinen Code auf Fehler zu überprüfen!) Habe ich bereits einige Informationen zu Mustern im Nicht-Programm-Lösungsbereich veröffentlicht. Siehe https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space. Die Aufzählung von> 4 Milliarden Rätsellösungen und deren Codierung in eine Wahrheitstabelle zeigt fraktale Muster - Selbstähnlichkeit und insbesondere Selbstaffinität. Diese affine Redundanz zeigt eine Struktur innerhalb des Problems, die ausgenutzt werden kann, um die zur Generierung von Lösungen erforderlichen Rechenressourcen zu reduzieren. Es zeigt auch die Notwendigkeit einer chaotischen Rückkopplung in jedem erfolgreichen Algorithmus. Das Phasenübergangsverhalten hat Erklärungskraft, wenn "einfache" Instanzen entlang der groben Struktur liegen, während "harte" Instanzen eine weitere Iteration bis ins kleinste Detail erfordern, die von normalen Heuristiken völlig verborgen ist. Wenn Sie in die Ecke dieses unendlichen Bildes zoomen möchten (alle <= 4x4 Puzzle-Instanzen sind codiert), lesen Sie http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html

Methode 1. Extrapolieren Sie den Nicht-Programmlösungsraumschatten mit chaotischen Karten und maschinellem Lernen (denken Sie an Anpassungsfunktionen, die denen ähneln, die das Mandelbrot-Set generieren).

Hier ist ein visueller Induktionsnachweis. Wenn Sie diese vier Bilder von links nach rechts scannen und denken , Sie haben eine gute Idee , die fehlende 5. ... 6. zu generieren ... etc. Bilder, dann habe ich gerade programmiert Sie als mein NP Orakel für das Entscheidungsproblem der nonogram Lösung Existenz. Bitte treten Sie vor, um Ihren Preis als den leistungsstärksten Supercomputer der Welt zu beanspruchen. Ich füttere Sie hin und wieder mit Strom, während die Welt Ihnen für Ihre Rechenbeiträge dankt.

Methode 2. Verwenden Sie Fourier-Transformationen für die Boolesche Bildversion von Eingaben. FFTs liefern globale Informationen zu Häufigkeit und Position innerhalb einer Instanz. Während der Betragsteil zwischen den Eingangspaaren ähnlich sein sollte, ist ihre Phaseninformation völlig unterschiedlich - sie enthält gerichtete Information über eine Lösungsprojektion entlang einer bestimmten Achse. Wenn Sie klug genug sind, können Sie das Phasenbild der Lösung durch eine spezielle Überlagerung der Eingangsphasenbilder rekonstruieren . Dann transformieren Sie die Phase und die gemeinsame Größe invers zurück in den Zeitbereich der Lösung.

Was könnte diese Methode erklären? Es gibt viele Permutationen der Booleschen Bilder mit flexiblem Auffüllen zwischen aufeinander folgenden Läufen. Dies ermöglicht eine Zuordnung zwischen Eingabe -> Lösung, die sich um die Multiplizität kümmert, während die Eigenschaft von FFTs von bidirektionalen, eindeutigen Zuordnungen zwischen Zeitbereich <-> (Frequenz, Phase) beibehalten wird. Es bedeutet auch, dass es keine "keine Lösung" gibt. Es würde heißen, dass es in einem fortlaufenden Fall Graustufenlösungen gibt, die Sie nicht in Betracht ziehen, wenn Sie sich das Bilevel-Bild des herkömmlichen Lösen von Nonogramm-Rätseln ansehen.

Warum würdest du es nicht tun? Es ist eine schreckliche Art zu rechnen, da FFTs in der heutigen Fließkomma-Welt bei großen Instanzen sehr ungenau wären. Präzision ist ein großes Problem, und die Rekonstruktion von Bildern aus quantisierten Größen- und Phasenbildern führt in der Regel zu sehr ungefähren Lösungen, auch wenn dies für die Schwellenwerte des menschlichen Auges möglicherweise nicht visuell ist . Es ist auch sehr schwierig, dieses Überlagerungsgeschäft zu entwickeln, da die Art der Funktion, die es tatsächlich ausführt, derzeit unbekannt ist. Wäre es ein einfaches Mittelungsschema? Wahrscheinlich nicht, und es gibt keine bestimmte Suchmethode, um es zu finden, außer Intuition.

Methode 3. Suchen Sie eine zellulare Automatenregel (aus einer möglichen Anzahl von 4 Milliarden Regeltabellen für von Neumann-Regeln mit zwei Zuständen), die eine symmetrische Version des Nonogramm-Puzzles löst. Sie verwenden eine direkte Einbettung des Problems in die hier gezeigten Zellen.

Dies ist wahrscheinlich die eleganteste Methode in Bezug auf Einfachheit und gute Effekte für die Zukunft des Rechnens. Die Existenz dieser Regel ist nicht bewiesen, aber ich habe eine Vermutung, dass es existiert. Hier ist der Grund:

Nonogramme erfordern viel chaotisches Feedback im Algorithmus, um genau gelöst zu werden. Dies wird durch den Brute-Force-Code festgelegt, der mit Code Review verknüpft ist. CA ist gerade die fähigste Sprache, um chaotisches Feedback zu programmieren.

Es sieht richtig, visuell. Die Regel würde sich durch eine Einbettung entwickeln, Informationen horizontal und vertikal verbreiten, interferieren und sich dann zu einer Lösung stabilisieren, die die Anzahl der gesetzten Zellen konserviert. Diese Weiterleitungsroute folgt dem Pfad (rückwärts), an den Sie normalerweise denken, wenn Sie den Schatten eines physischen Objekts in die ursprüngliche Konfiguration projizieren. Nonogramme stammen aus einem speziellen Fall der diskreten Tomographie. Stellen Sie sich also vor, Sie sitzen gleichzeitig in zwei Computertomographen mit Kitty-Ecke. Auf diese Weise würden die Röntgenstrahlen die medizinischen Bilder erzeugen. Natürlich gibt es Grenzprobleme - die Ränder des CA-Universums können Informationen nur dann weitergeben, wenn Sie ein toroidales Universum zulassen. Dies wirft das Rätsel auch als periodisches Randwertproblem auf.

Es werden mehrere Lösungen als Übergangszustände in einem kontinuierlich oszillierenden Effekt zwischen dem Austauschen von Ausgängen als Eingängen und umgekehrt erläutert. Es werden Instanzen erläutert, die keine Lösung als Originalkonfigurationen haben, bei denen die Anzahl der gesetzten Zellen nicht erhalten bleibt. Abhängig vom tatsächlichen Ergebnis des Auffindens einer solchen Regel kann sie sogar unlösbare Instanzen mit einer engen Lösung approximieren, bei der die Zellzustände erhalten bleiben .

C ++

Hier ist eine Lösung , die garantiert in polynomialer Zeit laufen: es läuft in O(n^k)denen ndie Anzahl der booleans und kist eine Konstante Ihrer Wahl.

Es ist heuristisch korrekt, was meiner Meinung nach CS-speak ist, denn "es gibt die meiste Zeit die richtige Antwort, mit ein bisschen Glück" (und in diesem Fall ist mir tatsächlich ein entsprechend großer Wert von k- edit eingefallen, dass für jedes feste nkannst du so einstellen k, dass n^k > 2^n- das schummelt?).

#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;
  }
}

rubin / gnuplot 3d oberfläche

(ooh harte Konkurrenz!) ... jedenfalls ... sagt ein Bild mehr als tausend Worte? Dies sind 3 separate Flächendiagramme, die im Gnuplot des SAT-Übergangspunkts erstellt wurden. Die (x, y) Achsen sind Klausel & Variable Anzahl und die z Höhe ist die Gesamtanzahl der rekursiven Aufrufe im Solver. Code in Ruby geschrieben. Es werden 10x10 Punkte mit jeweils 100 Abtastwerten abgetastet. es demonstriert / verwendet grundlegende Prinzipien der Statistik und ist eine Monte-Carlo-Simulation .

Es handelt sich im Grunde genommen um einen Davis Putnam- Algorithmus, der auf zufälligen Instanzen im DIMACS-Format ausgeführt wird. Dies ist die Art von Übung, die idealerweise in CS-Kursen auf der ganzen Welt durchgeführt wird, damit die Schüler die Grundlagen erlernen können, die aber fast überhaupt nicht speziell unterrichtet werden ... Vielleicht aus irgendeinem Grund, warum es so viele falsche P = NP-Beweise gibt ? Es gibt nicht einmal einen guten Wikipedia-Artikel, der das Übergangspunkt-Phänomen beschreibt (irgendwelche Nehmer?), das in der statistischen Physik ein sehr wichtiges Thema ist und auch in CS eine Schlüsselrolle spielt. [a] [b] Es gibt in CS viele Artikel über den Übergangspunkt Es scheinen jedoch nur sehr wenige Flächenplots zu zeigen! (Stattdessen werden normalerweise 2D-Slices angezeigt.)

die exponentielle Zunahme der Laufzeit ist deutlich in 1 ersichtlich ^st Plot. der Sattel durch die Mitte von 1 läuft ^st Handlung ist der Übergangspunkt. die 2 ^nd und 3 ^rd Plots zeigt das% erfüllbar Übergang.

[a] Phasenübergangsverhalten in CS ppt Toby Walsh
[b] empirische Wahrscheinlichkeit der Erfüllbarkeit von k-SAT tcs.se
[c] große Momente in empirischer / experimenteller Mathematik / (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
}