SAT jest problemem polegającym na ustaleniu, czy wyrażenie logiczne może być prawdziwe. Na przykład (A) można spełnić, ustawiając A = PRAWDA, ale (A &&! A) nigdy nie może być prawdziwe. Ten problem jest znany jako NP-zupełny. Zobacz wartość logiczna .

Twoim zadaniem jest napisanie programu dla SAT, który będzie wykonywany w czasie wielomianowym, ale może nie rozwiązać wszystkich przypadków.

W niektórych przykładach powodem, dla którego tak naprawdę nie jest wielomianem, może być:

1. Istnieje przypadek skrajny, który nie jest oczywisty, ale ma słaby czas działania
2. Algorytm faktycznie nie rozwiązuje problemu w nieoczekiwanym przypadku
3. Niektóre funkcje języka programowania, którego używasz, mają dłuższy czas działania, niż można by się spodziewać
4. Twój kod faktycznie robi coś zupełnie innego niż to, na co wygląda

Możesz używać dowolnego języka programowania (lub kombinacji języków). Nie musisz przedstawiać formalnego dowodu złożoności algorytmu, ale powinieneś przynajmniej wyjaśnić.

Podstawowymi kryteriami oceny powinno być przekonujący kod.

To konkurs popularności, więc wygrywa najwyżej oceniana odpowiedź w ciągu tygodnia.

DO#

Twoim zadaniem jest napisanie programu dla SAT, który wydaje się działać w czasie wielomianowym.

„Pojawia się” jest niepotrzebne. Potrafię napisać program, który naprawdę wykonuje się w czasie wielomianowym, aby rozwiązać problemy SAT. W rzeczywistości jest to dość proste.

BONUS MEGA: Jeśli napiszesz SAT-solver, który faktycznie działa w czasie wielomianowym, dostaniesz milion dolarów! Ale i tak proszę użyć tagu spoiler, aby inni mogli się nad tym zastanawiać.

Niesamowite. Proszę, wyślij mi milion dolarów. Poważnie, mam tutaj program, który rozwiąże SAT z wielomianowym środowiskiem uruchomieniowym.

Zacznę od stwierdzenia, że ​​rozwiążę wariację na temat problemu SAT. Pokażę, jak napisać program, który pokazuje unikalne rozwiązanie dowolnego problemu 3-SAT . Wycena każdej zmiennej logicznej musi być unikalna, aby mój solver mógł działać.

Zaczynamy od zadeklarowania kilku prostych metod i typów pomocników:

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

Teraz wybierzmy problem 3-SAT do rozwiązania. Powiedzmy

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

Rozwijajmy to trochę bardziej.

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

Kodujemy to tak:

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

I oczywiście, kiedy uruchamiamy program, otrzymujemy rozwiązanie dla 3-SAT w czasie wielomianowym. W rzeczywistości środowisko uruchomieniowe ma rozmiar problemu liniowy !

x1: false
x2: true
x3: false

Powiedziałeś, że środowisko uruchomieniowe wielomianowe . Nie powiedziałeś nic o czasie kompilacji wielomianowej . Ten program zmusza kompilator C # do wypróbowania wszystkich możliwych kombinacji typów dla x1, x2 i x3 i wybrania tej unikalnej, która nie wykazuje błędów typu. Kompilator wykonuje całą pracę, więc środowisko wykonawcze nie musi. Po raz pierwszy zaprezentowałem tę interesującą technikę na swoim blogu w 2007 roku: http://blogs.msdn.com/b/ericlippert/archive/2007/03/28/lambda-expressions-vs-anonymous-methods-part-five.aspx Uwaga że oczywiście ten przykład pokazuje, że rozdzielczość przeciążenia w C # wynosi co najmniej NP-HARD. Niezależnie od tego, czy jest to NP-HARD, czy faktycznie nierozstrzygalne zależy od pewnych subtelnych szczegółów działania konwertowalności typu w obecności ogólnej sprzeczności, ale jest to temat na inny dzień.

Wielojęzyczny (1 bajt)

Poniższy program, ważny w wielu językach, głównie funkcjonalny i ezoteryczny, da poprawną odpowiedź na wiele problemów SAT i ma stałą złożoność (!!!):

0

O dziwo, następny program da poprawną odpowiedź na wszystkie pozostałe problemy i ma tę samą złożoność. Musisz więc wybrać odpowiedni program, a we wszystkich przypadkach będziesz mieć poprawną odpowiedź!

1

JavaScript

Dzięki iterowanemu niedeterminizmowi SAT można rozwiązać w czasie wielomianowym!

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

Przykładowe użycie:

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

Algorytm ten po prostu sprawdza podaną formułę logiczną tysiąc razy przy losowych danych wejściowych. Prawie zawsze działa w przypadku małych nakładów, ale jest mniej niezawodna, gdy wprowadza się więcej zmiennych.

Nawiasem mówiąc, jestem dumny, że miałem okazję korzystać z dwóch najbardziej niewykorzystanych funkcji JavaScript obok siebie: evali with.

Matematyka + Obliczenia kwantowe

Być może nie wiesz, że Mathematica jest wyposażona w komputer kwantowy na pokładzie

Needs["Quantum`Computing`"];

Kwantowa komunikacja adiabatyczna koduje problem, który należy rozwiązać u hamiltonianów (operator energii) w taki sposób, że jego stan minimalnej energii („stan podstawowy”) stanowi rozwiązanie. Dlatego adiabatyczna ewolucja układu kwantowego do stanu podstawowego hamiltonianu i późniejszy pomiar daje rozwiązanie problemu.

Definiujemy subhamiltonian, który odpowiada ||części wyrażenia, z odpowiednią kombinacją operatorów Pauliego dla zmiennych i ich negacją

Gdzie takie wyrażenie

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

argument powinien wyglądać

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

Oto kod konstruujący taki argument z wyrażenia 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

Teraz konstruujemy pełny hamiltonian, sumując subhamiltonianie (sumowanie odpowiada &&częściom wyrażenia)

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

I poszukaj najniższego stanu energii

QuantumEigensystemForm[H, -1]

Jeśli otrzymamy wartość własną zero, to wektor własny jest rozwiązaniem

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

Niestety oficjalna strona dodatku „Quantum Computing” nie jest aktywna i nie mogę znaleźć miejsca do pobrania, po prostu wciąż mam go zainstalowanego na moim komputerze. Dodatek ma również udokumentowane rozwiązanie problemu SAT, na którym oparłem swój kod.

Trzy podejścia tutaj, wszystkie polegają na redukcji SAT do 2D geometrycznej lingua franca: łamigłówki logiczne nonogram. Komórki w układance logicznej odpowiadają zmiennym SAT, ograniczeniom klauzul.

Aby uzyskać pełne wyjaśnienie (i proszę przejrzeć mój kod pod kątem błędów!) Już opublikowałem pewien wgląd w wzorce w obszarze rozwiązania nonogram. Zobacz https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space. Wyliczenie> 4 miliardów rozwiązań łamigłówek i zakodowanie ich w tabeli prawdy pokazuje wzorce fraktalne - podobieństwo do siebie, a zwłaszcza powinowactwo do siebie. Ta nadmiarowość afiniczna pokazuje strukturę problemu, którą można wykorzystać do zmniejszenia zasobów obliczeniowych niezbędnych do generowania rozwiązań. Pokazuje także potrzebę chaotycznej informacji zwrotnej w ramach dowolnego udanego algorytmu. W zachowaniu przejścia fazowego występuje moc wyjaśniająca, w której „łatwymi” instancjami są te, które leżą wzdłuż grubej struktury, podczas gdy „twarde” instancje wymagają dalszej iteracji do drobnych szczegółów, całkowicie ukrytych przed normalną heurystyką. Jeśli chcesz powiększyć narożnik tego nieskończonego obrazu (wszystkie zakodowane instancje <= 4x4) zobacz http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html

Metoda 1. Ekstrapoluj cień przestrzeni rozwiązania nonogram za pomocą chaotycznych map i uczenia maszynowego (pomyśl dopasowanie funkcji podobnych do tych, które generują zestaw Mandelbrota).

Oto wizualny dowód indukcji. Jeśli możesz zeskanować te cztery obrazy od lewej do prawej i uważasz, że masz dobry pomysł, aby wygenerować brakujące 5. ... 6. ... itd., To właśnie zaprogramowałem cię jako moją wyrocznię NP dla problemu decyzyjnego rozwiązania nonogram istnienie. Zrób krok, aby odebrać swoją nagrodę jako najpotężniejszy superkomputer na świecie. Od czasu do czasu karmię cię prądem, podczas gdy świat dziękuje ci za wkład w obliczenia.

Metoda 2. Użyj transformacji Fouriera w wersji wejściowej z obrazem logicznym. FFT zapewniają globalne informacje o częstotliwości i pozycji w instancji. Podczas gdy część wielkości powinna być podobna między parą wejściową, ich informacja o fazie jest zupełnie inna - zawiera ukierunkowane informacje o rzucie rozwiązania wzdłuż określonej osi. Jeśli jesteś wystarczająco sprytny, możesz zrekonstruować obraz fazowy rozwiązania za pomocą specjalnej superpozycji wejściowych obrazów fazowych. Następnie odwróć transformację fazy i wspólnej wielkości z powrotem do dziedziny czasu rozwiązania.

Co ta metoda może wyjaśnić? Istnieje wiele kombinacji obrazów boolowskich z elastycznym wypełnieniem między ciągłymi przebiegami. Pozwala to na mapowanie między rozwiązaniem wejściowym -> dbającym o wielość, przy jednoczesnym zachowaniu właściwości FFT dwukierunkowych, unikalnych mapowań między dziedziną czasu <-> (częstotliwość, faza). Oznacza to również, że nie ma czegoś takiego jak „brak rozwiązania”. Mówiłoby to, że w ciągłym przypadku istnieją rozwiązania w skali szarości, których nie bierze się pod uwagę, patrząc na dwupoziomowy obraz tradycyjnego rozwiązywania łamigłówek z użyciem nonogramów.

Dlaczego tego nie zrobiłeś? To okropny sposób na obliczenia, ponieważ FFT w dzisiejszym zmiennoprzecinkowym świecie byłyby bardzo niedokładne w przypadku dużych instancji. Precyzja jest ogromnym problemem, a rekonstrukcja obrazów z kwantowanych obrazów wielkości i faz zwykle tworzy bardzo przybliżone rozwiązania, choć może nie wizualnie dla progów ludzkiego oka. Bardzo trudno jest wymyślić ten biznes superpozycjonowania, ponieważ rodzaj faktycznie wykonującej go funkcji jest obecnie nieznany. Czy byłby to prosty schemat uśredniania? Prawdopodobnie nie i nie ma żadnej konkretnej metody wyszukiwania oprócz intuicji.

Metoda 3. Znajdź regułę automatów komórkowych (z możliwych ~ 4 miliardów tabel reguł dla reguł 2-stanowych von Neumanna), która rozwiązuje symetryczną wersję łamigłówki nonogramowej. Wykorzystujesz bezpośrednie osadzenie problemu w pokazanych tutaj komórkach.

Jest to prawdopodobnie najbardziej elegancka metoda pod względem prostoty i dobrych efektów na przyszłość komputerów. Istnienie tej reguły nie zostało udowodnione, ale mam przeczucie, że ona istnieje. Dlatego:

Nonogramy wymagają wielu chaotycznych informacji zwrotnych w algorytmie, aby zostały dokładnie rozwiązane. Jest to ustalone przez kod brutalnej siły powiązany z przeglądem kodu. CA jest językiem najbardziej zdolnym do programowania chaotycznego sprzężenia zwrotnego.

To wygląda dobrze, wizualnie. Reguła ewoluowałaby poprzez osadzanie, przekazywanie informacji poziomo i pionowo, ingerowanie, a następnie stabilizowanie do rozwiązania, które zachowało liczbę ustawionych komórek. Ta trasa propagacji podąża ścieżką (do tyłu), o której zwykle myślisz, rzutując cień obiektu fizycznego na pierwotną konfigurację. Nonogramy wywodzą się ze specjalnego przypadku tomografii dyskretnej, więc wyobraź sobie, że siedzisz jednocześnie w dwóch tomografach komputerowych z rogami kotka. W ten sposób promieniowanie rentgenowskie zareagowałoby na generowanie obrazów medycznych. Oczywiście istnieją problemy graniczne - krawędzie wszechświata CA nie mogą dalej propagować informacji poza granicami, chyba że dopuścisz wszechświat toroidalny. To także stawia zagadkę jako okresowy problem z wartością graniczną.

Wyjaśnia wiele rozwiązań jako stany przejściowe z ciągłym oscylującym efektem między zamianą wyjść jako danych wejściowych i odwrotnie. Wyjaśnia przypadki, które nie mają rozwiązania, jako oryginalne konfiguracje, które nie oszczędzają liczby ustawionych komórek. W zależności od faktycznego wyniku znalezienia takiej reguły może ona nawet przybliżać nierozwiązywalne przypadki za pomocą bliskiego rozwiązania, w którym zachowane są stany komórek .

C ++

Oto rozwiązanie, które gwarantuje działanie w czasie wielomianowym: działa O(n^k)tam, gdzie njest liczba booleanów i kjest stałą do wyboru.

Jest heurystycznie poprawny, co moim zdaniem jest CS-speak, ponieważ „daje poprawną odpowiedź przez większość czasu, przy odrobinie szczęścia” (i, w tym przypadku, odpowiednio dużą wartość k- edycja faktycznie przyszło mi do głowy, że dla każdego ustalonego nmożna ustawić ktak, aby n^k > 2^n- czy to oszustwo?).

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

powierzchnia 3d ruby ​​/ gnuplot

(och, twarda konkurencja!) ... w każdym razie ... czy obraz jest wart tysiąca słów? są to 3 osobne wykresy powierzchni wykonane w gnuplot punktu przejścia SAT. osie (x, y) są klauzulami i zmiennymi, a wysokość z jest całkowitą liczbą wywołań rekurencyjnych w solwerze. kod napisany w rubinie. Próbkuje 10x10 punktów po 100 próbek. demonstruje / wykorzystuje podstawowe zasady statystyki i jest symulacją Monte Carlo .

jest to w zasadzie algorytm davis putnam działający na przypadkowych instancjach generowanych w formacie DIMACS. jest to rodzaj ćwiczenia, które najlepiej byłoby wykonać na zajęciach z CS na całym świecie, aby uczniowie mogli nauczyć się podstaw, ale prawie wcale nie są specjalnie nauczani ... może z jakiegoś powodu, dlaczego istnieje tak wiele fałszywych dowodów P? = NP ? nie ma nawet dobrego artykułu w Wikipedii opisującego zjawisko punktu przejścia (któryś z nich?), który jest bardzo ważnym tematem w fizyce statystycznej i jest kluczowy również w CS. [a] [b] w CS jest wiele artykułów na temat punktu przejścia jednak niewielu wydaje się pokazywać wykresy powierzchniowe! (zamiast tego zazwyczaj pokazuje plastry 2d.)

wykładniczy wzrost czasu działania jest wyraźnie widoczny na ^pierwszym wykresie. siodło przebiegającej przez środku 1 ^st działki to punkt przejścia. z 2 ^ND i 3 ^rd wykresy pokazują% spe przejścia.

[a] zachowanie przejścia fazowego w CS ppt Toby Walsh
[b] empiryczne prawdopodobieństwo satysfakcji k-SAT tcs.se
[c] wspaniałe momenty w matematyce empirycznej / eksperymentalnej / (T) CS / SAT , blog TMachine

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
}