SAT adalah masalah menentukan apakah ekspresi boolean dapat dibuat benar. Misalnya, (A) dapat dibuat benar dengan menetapkan A = BENAR, tetapi (A &&! A) tidak pernah benar. Masalah ini dikenal sebagai NP-complete. Lihat Kepuasan Boolean .

Tugas Anda adalah menulis program untuk SAT yang dijalankan dalam waktu polinomial, tetapi mungkin tidak menyelesaikan semua kasus.

Untuk beberapa contoh, alasan itu tidak benar-benar polinomial bisa karena:

1. Ada kasus tepi yang tidak jelas tetapi memiliki runtime yang buruk
2. Algoritma sebenarnya gagal menyelesaikan masalah dalam beberapa kasus yang tidak terduga
3. Beberapa fitur bahasa pemrograman yang Anda gunakan sebenarnya memiliki runtime yang lebih lama daripada yang Anda harapkan
4. Kode Anda sebenarnya melakukan sesuatu yang sama sekali berbeda dari apa yang dilakukannya

Anda dapat menggunakan bahasa pemrograman apa pun (atau kombinasi bahasa) yang Anda inginkan. Anda tidak perlu memberikan bukti formal tentang kompleksitas algoritme Anda, tetapi Anda setidaknya harus memberikan penjelasan.

Kriteria utama untuk menilai harus seberapa meyakinkan kode tersebut.

Ini adalah kontes popularitas, jadi jawaban dengan nilai tertinggi dalam seminggu menang.

C #

Tugas Anda adalah menulis program untuk SAT yang tampaknya dijalankan dalam waktu polinomial.

"Muncul" tidak perlu. Saya dapat menulis sebuah program yang benar-benar mengeksekusi dalam waktu polinomial untuk menyelesaikan masalah SAT. Ini sebenarnya cukup mudah.

BONUS MEGA: Jika Anda menulis SAT-solver yang sebenarnya dieksekusi dalam waktu polinomial, Anda mendapatkan satu juta dolar! Tapi tolong gunakan tag spoiler, jadi orang lain bisa bertanya-tanya tentang itu.

Luar biasa. Tolong kirimi saya jutaan dolar. Serius, saya punya program di sini yang akan menyelesaikan SAT dengan runtime polinomial.

Biarkan saya mulai dengan menyatakan bahwa saya akan menyelesaikan variasi pada masalah SAT. Saya akan menunjukkan cara menulis program yang menunjukkan solusi unik dari masalah 3-SAT . Penilaian setiap variabel Boolean harus unik agar pemecah saya bekerja.

Kita mulai dengan mendeklarasikan beberapa metode dan tipe pembantu sederhana:

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

Sekarang mari kita pilih masalah 3-SAT untuk dipecahkan. Katakanlah

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

Mari kita kurung sedikit lagi.

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

Kami menyandikannya seperti ini:

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

Dan tentu saja ketika kami menjalankan program, kami mendapatkan solusi untuk 3-SAT dalam waktu polinomial. Bahkan runtime linier dalam ukuran masalah !

x1: false
x2: true
x3: false

Anda mengatakan runtime polinomial . Anda tidak mengatakan apa pun tentang waktu kompilasi polinomial . Program ini memaksa kompiler C # untuk mencoba semua kombinasi tipe yang mungkin untuk x1, x2 dan x3, dan memilih yang unik yang tidak menunjukkan kesalahan tipe. Compiler melakukan semua pekerjaan, sehingga runtime tidak harus. Saya pertama kali memamerkan teknik menarik ini di blog saya pada tahun 2007: http://blogs.msdn.com/b/ericlippert/archive/2007/03/28/lambda-expressions-vs-anonymous-methods-part-five.aspx Catatan bahwa tentu saja contoh ini menunjukkan bahwa resolusi kelebihan dalam C # setidaknya NP-HARD. Apakah itu NP-HARD atau sebenarnya tidak dapat diputuskan tergantung pada perincian halus tertentu dalam cara kerja konvertibilitas jenis dengan adanya contravariance generik, tapi itu subjek untuk hari lain.

Multi-bahasa (1 byte)

Program berikut, valid dalam banyak bahasa, sebagian besar fungsional dan esoterik, akan memberikan jawaban yang benar untuk sejumlah besar masalah SAT dan memiliki kompleksitas konstan (!!!):

0

Hebatnya, program selanjutnya akan memberikan jawaban yang benar untuk semua masalah yang tersisa, dan memiliki kompleksitas yang sama. Jadi Anda hanya perlu memilih program yang tepat, dan Anda akan memiliki jawaban yang benar dalam semua kasus!

1

JavaScript

Dengan menggunakan non-determinisme iterated, SAT dapat diselesaikan dalam waktu polinomial!

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

Contoh penggunaan:

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

Algoritma ini hanya memeriksa formula boolean yang diberikan seribu kali dengan input acak. Hampir selalu bekerja untuk input kecil, tetapi kurang dapat diandalkan ketika lebih banyak variabel diperkenalkan.

Ngomong-ngomong, saya bangga bahwa saya memiliki kesempatan untuk memanfaatkan dua fitur JavaScript yang paling jarang digunakan di samping satu sama lain: evaldan with.

Mathematica + Quantum Computing

Anda mungkin tidak tahu bahwa Mathematica hadir dengan komputer kuantum

Needs["Quantum`Computing`"];

Quantum Adiabatic Commputing mengkode masalah yang harus dipecahkan dalam Hamiltonian (operator energi) sedemikian rupa sehingga keadaan energi minimumnya ("ground state") merupakan solusinya. Oleh karena itu evolusi adiabatik dari sistem kuantum ke keadaan dasar Hamiltonian dan pengukuran selanjutnya memberikan solusi untuk masalah tersebut.

Kami mendefinisikan subhamilton yang sesuai dengan ||bagian ekspresi, dengan kombinasi yang tepat dari operator Pauli untuk variabel dan negasinya

Di mana untuk ekspresi seperti ini

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

argumennya harus seperti

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

Berikut adalah kode untuk membangun argumen seperti itu dari ekspresi 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

Sekarang kita membangun Hamiltonian penuh, merangkum subhamilton (penjumlahan sesuai dengan &&bagian dari ekspresi)

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

Dan cari kondisi energi terendah

QuantumEigensystemForm[H, -1]

Jika kita mendapat nilai eigen nol, maka vektor eigen adalah solusinya

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

Sayangnya situs resmi untuk add-on "Quantum Computing" tidak aktif dan saya tidak dapat menemukan tempat untuk mengunduhnya, saya hanya menginstalnya di komputer saya. Add-on ini juga memiliki solusi yang terdokumentasi untuk masalah SAT, di mana saya mendasarkan kode saya.

Tiga pendekatan di sini, semua melibatkan pengurangan SAT ke dalam lingua franca geometris 2D: teka-teki logika nonogram. Sel-sel dalam teka-teki logika sesuai dengan variabel SAT, batasan untuk klausa.

Untuk penjelasan lengkap (dan silakan tinjau kode saya untuk bug!) Saya sudah memposting beberapa wawasan untuk pola dalam ruang solusi nonogram. Lihat https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space. Menghitung> 4 miliar solusi teka-teki dan menyandikannya agar sesuai dengan tabel kebenaran menunjukkan pola fraktal - kesamaan diri dan khususnya afinitas diri. Afine-redundancy ini menunjukkan struktur dalam masalah, dapat dieksploitasi untuk mengurangi sumber daya komputasi yang diperlukan untuk menghasilkan solusi. Ini juga menunjukkan perlunya umpan balik kacau dalam setiap algoritma yang berhasil. Ada kekuatan penjelas dalam perilaku transisi fase di mana instans "mudah" adalah instans yang terletak di sepanjang struktur kasar, sementara instans "keras" memerlukan iterasi lebih lanjut menjadi detail halus, cukup tersembunyi dari heuristik normal. Jika Anda ingin memperbesar ke sudut gambar yang tak terbatas ini (semua <= 4x4 instance puzzle dikodekan) lihat http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html

Metode 1. Ekstrapolasi bayangan ruang solusi nonogram menggunakan peta kacau dan pembelajaran mesin (berpikir fungsi pas mirip dengan yang menghasilkan Set Mandelbrot).

Berikut ini adalah bukti visual induksi. Jika Anda dapat memindai keempat gambar ini dari kiri ke kanan dan berpikir Anda memiliki ide bagus untuk menghasilkan gambar ke-5 ... ke-6 yang hilang, dll., Maka saya baru saja memprogram Anda sebagai ramalan NP saya untuk masalah keputusan solusi nonogram adanya. Silakan melangkah maju untuk mengklaim hadiah Anda sebagai superkomputer paling kuat di dunia. Saya akan memberi Anda kejutan listrik setiap saat, sementara dunia berterima kasih atas kontribusi komputasi Anda.

Metode 2. Gunakan Fourier Transforms pada input gambar versi boolean. FFT menyediakan informasi global tentang frekuensi dan posisi dalam sebuah instance. Sementara bagian besarnya harus serupa antara pasangan input, informasi fase mereka benar-benar berbeda - berisi informasi terarah tentang proyeksi solusi sepanjang sumbu tertentu. Jika Anda cukup pintar, Anda mungkin merekonstruksi gambar fase dari solusi melalui beberapa superposisi khusus dari gambar fase input. Kemudian invers mengubah fase dan besarnya umum kembali ke domain waktu dari solusi.

Apa yang bisa dijelaskan metode ini? Ada banyak permutasi dari gambar boolean dengan padding fleksibel di antara run yang berdekatan. Ini memungkinkan pemetaan antara input -> solusi yang menjaga multiplisitas sambil tetap mempertahankan properti FFT dari bidirectional, pemetaan unik antara domain waktu <-> (frekuensi, fase). Ini juga berarti tidak ada yang namanya "tidak ada solusi." Apa yang akan dikatakannya adalah bahwa dalam kasus berkelanjutan, ada solusi skala abu-abu yang tidak Anda pertimbangkan ketika melihat gambar bilevel dari pemecahan teka-teki nonogram tradisional.

Kenapa kamu tidak melakukannya? Ini adalah cara yang mengerikan untuk benar-benar menghitung, karena FFT di dunia floating-point saat ini akan sangat tidak akurat dengan contoh besar. Presisi adalah masalah besar, dan merekonstruksi gambar dari besaran fase dan gambar fase biasanya menghasilkan solusi yang sangat mendekati, meskipun mungkin tidak secara visual untuk ambang mata manusia. Ini juga sangat sulit untuk menghasilkan bisnis superposisi ini, karena jenis fungsi yang sebenarnya melakukannya saat ini tidak diketahui. Apakah itu skema rata-rata yang sederhana? Mungkin tidak, dan tidak ada metode pencarian khusus untuk menemukannya kecuali intuisi.

Metode 3. Temukan aturan automata seluler (dari kemungkinan ~ 4 miliar tabel aturan untuk aturan 2-negara von Neumann) yang memecahkan versi simetris dari teka-teki nonogram. Anda menggunakan penyematan langsung masalah ke dalam sel, ditunjukkan di sini.

Ini mungkin metode yang paling elegan, dalam hal kesederhanaan dan efek yang baik untuk masa depan komputasi. Keberadaan aturan ini tidak terbukti, tetapi saya punya firasat itu ada. Inilah alasannya:

Nonogram membutuhkan banyak umpan balik kacau dalam algoritma yang harus dipecahkan dengan tepat. Ini dibuat oleh kode brute force yang tertaut pada Review Kode. CA hanya tentang bahasa yang paling mampu memprogram umpan balik kacau.

Ini terlihat benar, secara visual. Aturan tersebut akan berkembang melalui penyisipan, penyebarluasan informasi secara horizontal dan vertikal, mengganggu, kemudian distabilkan menjadi solusi yang menghemat jumlah sel yang ditetapkan. Rute propogasi ini mengikuti jalur (mundur) yang biasanya Anda pikirkan ketika memproyeksikan bayangan objek fisik ke konfigurasi asli. Nonogram berasal dari kasus khusus tomografi diskrit, jadi bayangkan duduk bersamaan dalam dua pemindai CT yang dipojokkan dengan kitty .. ini adalah bagaimana sinar-X akan mempropogasi untuk menghasilkan gambar medis. Tentu saja, ada masalah batas - tepi alam semesta CA tidak dapat terus menyebarkan informasi di luar batas, kecuali jika Anda mengizinkan alam semesta toroidal. Ini juga melemparkan puzzle sebagai masalah nilai batas periodik.

Ini menjelaskan beberapa solusi sebagai kondisi transien dalam efek osilasi terus menerus antara menukar output sebagai input, dan sebaliknya. Ini menjelaskan contoh yang tidak memiliki solusi sebagai konfigurasi asli yang tidak menghemat jumlah sel yang ditetapkan. Tergantung pada hasil yang sebenarnya menemukan aturan tersebut, bahkan mungkin mendekati contoh dipecahkan dengan solusi yang dekat di mana negara-negara sel yang dilestarikan.

C ++

Berikut ini adalah solusi yang dijamin untuk dijalankan dalam waktu polinomial: ini berjalan di O(n^k)mana njumlah boolean dan kkonstanta pilihan Anda.

Itu heuristically benar, yang saya percaya adalah CS-berbicara untuk "itu memberikan jawaban yang benar sebagian besar waktu, dengan sedikit keberuntungan" (dan, dalam hal ini, nilai yang tepat besar k- sunting itu benar-benar terjadi pada saya bahwa untuk setiap perbaikan nAnda dapat mengatur ksedemikian rupa n^k > 2^n- apakah itu curang?).

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

permukaan 3d ruby ​​/ gnuplot

(ooh persaingan yang ketat!) ... Lagi pula ... apakah gambar itu bernilai ribuan kata? ini adalah 3 plot permukaan terpisah yang dibuat di gnuplot dari titik transisi SAT. sumbu (x, y) adalah klausa & jumlah variabel dan tinggi z adalah total # panggilan rekursif dalam pemecah. kode yang ditulis dalam ruby. itu sampel 10x10 poin masing-masing 100 sampel. itu menunjukkan / menggunakan prinsip-prinsip dasar statistik dan merupakan simulasi Monte Carlo .

pada dasarnya algoritma davis putnam berjalan pada instance acak yang dihasilkan dalam format DIMACS. ini adalah jenis latihan yang idealnya akan dilakukan di kelas CS di seluruh dunia sehingga siswa dapat mempelajari dasar - dasarnya tetapi hampir tidak diajarkan secara khusus sama sekali ... mungkin ada beberapa alasan mengapa ada begitu banyak P palsu ? = Bukti NP ? bahkan tidak ada artikel wikipedia yang bagus yang menggambarkan fenomena titik transisi (ada yang mengambil?) yang merupakan topik yang sangat menonjol dalam fisika statistik & kuncinya juga dalam CS. [a] [b] ada banyak makalah dalam CS tentang titik transisi namun sangat sedikit yang menunjukkan plot permukaan! (Sebaliknya biasanya menampilkan irisan 2d.)

peningkatan eksponensial dalam runtime adalah jelas dalam 1 ^st petak. pelana berjalan melalui tengah-tengah 1 ^st plot titik transisi. 2 ^nd dan 3 ^rd plot menunjukkan transisi satisfiable%.

[a] fase transisi perilaku dalam CS ppt Toby Walsh
[b] probabilitas empiris kepuasan k-SAT tcs.se
[c] momen-momen hebat dalam empiris / matematika eksperimental / (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
}