SAT - это проблема определения того, можно ли сделать булево выражение истинным. Например, (A) можно сделать истинным, установив A = TRUE, но (A &&! A) никогда не может быть истинным. Эта проблема, как известно, является NP-полной. См. Булево соответствие .

Ваша задача - написать программу для SAT, которая выполняется за полиномиальное время, но может решить не все случаи.

Для некоторых примеров, причина не очень Полином может быть:

1. Существует крайний случай, который не очевиден, но имеет плохое время выполнения
2. Алгоритм фактически не может решить проблему в каком-то неожиданном случае
3. Некоторые функции используемого вами языка программирования на самом деле имеют более длительное время выполнения, чем можно было бы ожидать
4. Ваш код на самом деле делает что-то совершенно отличное от того, что он делает

Вы можете использовать любой язык программирования (или комбинацию языков), который пожелаете. Вам не нужно предоставлять формальное доказательство сложности вашего алгоритма, но вы должны хотя бы предоставить объяснение.

Основным критерием оценки должно быть то, насколько убедительным является код.

Это конкурс популярности, поэтому победитель получает самый высокий рейтинг за неделю.

C #

Ваша задача - написать программу для SAT, которая, по-видимому, будет выполняться за полиномиальное время.

«Появляется» не нужно. Я могу написать программу, которая действительно выполняется за полиномиальное время для решения проблем SAT. Это довольно просто на самом деле.

MEGA BONUS: Если вы напишите SAT-решатель, который фактически выполняется за полиномиальное время, вы получите миллион долларов! Но в любом случае, пожалуйста, используйте тег спойлера, чтобы другие могли задуматься над этим.

Потрясающие. Пожалуйста, пришлите мне миллион долларов. Серьезно, у меня здесь есть программа, которая решает SAT с полиномиальным временем выполнения.

Позвольте мне начать с заявления о том, что я собираюсь решить вариацию проблемы SAT. Я собираюсь продемонстрировать, как написать программу, которая демонстрирует уникальное решение любой проблемы 3-SAT . Оценка каждой логической переменной должна быть уникальной, чтобы мой решатель работал.

Мы начнем с объявления нескольких простых вспомогательных методов и типов:

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

Теперь давайте выберем проблему 3-SAT для решения. Скажем

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

Давайте заключим это в скобки немного больше.

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

Мы кодируем это так:

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

И, конечно же, когда мы запускаем программу, мы получаем решение 3-SAT за полиномиальное время. На самом деле время выполнения является линейным по размеру проблемы !

x1: false
x2: true
x3: false

Вы сказали, полиномиальное время выполнения . Вы ничего не сказали о времени полиномиальной компиляции . Эта программа заставляет компилятор C # пробовать все возможные комбинации типов для x1, x2 и x3 и выбирать уникальную, которая не содержит ошибок типов. Компилятор выполняет всю работу, поэтому среда выполнения не обязана. Впервые я продемонстрировал эту интересную технику в своем блоге в 2007 году: http://blogs.msdn.com/b/ericlippert/archive/2007/03/28/lambda-expressions-vs-anonymous-methods-part-five.aspx Примечание. это, конечно, этот пример показывает, что разрешение перегрузки в C # по крайней мере NP-HARD. Будь то NP-жесткий или на самом деле неразрешимый зависит от некоторых тонких деталей того, как работает конвертируемость типов при наличии общей контравариантности, но это тема для другого дня.

Многоязычность (1 байт)

Следующая программа, действительная на многих языках, в основном функциональная и эзотерическая, даст правильный ответ для большого числа проблем SAT и имеет постоянную сложность (!!!):

0

Удивительно, но следующая программа даст правильный ответ на все оставшиеся проблемы, и имеет такую ​​же сложность. Так что вам просто нужно выбрать правильную программу, и вы получите правильный ответ во всех случаях!

1

JavaScript

Используя повторный недетерминизм, SAT может быть решена за полиномиальное время!

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

Пример использования:

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

Этот алгоритм просто проверяет данную логическую формулу тысячу раз со случайными входами. Почти всегда работает для небольших входов, но менее надежен, когда вводится больше переменных.

Кстати, я горжусь тем, что у меня была возможность использовать две наиболее недоиспользуемые функции JavaScript прямо рядом друг с другом: evalи with.

Mathematica + Quantum Computing

Вы можете не знать, что Mathematica поставляется с квантовым компьютером на борту

Needs["Quantum`Computing`"];

Квантовая адиабатическая коммутация кодирует задачу, которая должна быть решена в гамильтониане (оператор энергии) таким образом, что ее состояние минимальной энергии («основное состояние») представляет решение. Поэтому адиабатическая эволюция квантовой системы до основного состояния гамильтониана и последующее измерение дает решение задачи.

Определим субгамильтониан, соответствующий ||частям выражения, с соответствующей комбинацией операторов Паули для переменных и его отрицанием

Где для выражения, как это

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

аргумент должен выглядеть так

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

Вот код для построения такого аргумента из выражения 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

Теперь построим полный гамильтониан, суммируя субгамильтонианы (суммирование соответствует &&частям выражения)

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

И искать самое низкое энергетическое состояние

QuantumEigensystemForm[H, -1]

Если мы получили собственное значение ноль, то собственный вектор является решением

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

К сожалению, официальный сайт надстройки «Quantum Computing» не активен, и я не могу найти место для его загрузки, я все еще установил его на своем компьютере. У дополнения также есть документированное решение проблемы SAT, на котором я основал свой код.

Здесь три подхода, каждый из которых включает в себя сокращение SAT до его двумерного геометрического языка: неграммы логические головоломки. Ячейки в логической головоломке соответствуют переменным SAT, ограничениям на предложения.

Для полного объяснения (и, пожалуйста, просмотрите мой код на предмет ошибок!), Я уже опубликовал некоторое представление о шаблонах в пространстве решений неграммы. См. Https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space, Перечисление> 4 миллиардов решений головоломок и их кодирование, чтобы они поместились в таблицу истинности, показывает фрактальные паттерны - самоподобие и, особенно, родство. Эта аффинная избыточность демонстрирует структуру проблемы, которую можно использовать для уменьшения вычислительных ресурсов, необходимых для генерации решений. Это также показывает необходимость хаотической обратной связи в любом успешном алгоритме. Существует объяснительная сила в поведении фазового перехода, где «легкие» экземпляры - это те, которые лежат вдоль грубой структуры, в то время как «жесткие» экземпляры требуют дальнейшей итерации в мелкие детали, совершенно скрытые от обычной эвристики. Если вы хотите увеличить угол этого бесконечного изображения (все <= 4x4 закодированные экземпляры головоломки), см. Http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html.

Метод 1. Экстраполируйте тень пространства решения неограммы, используя хаотические карты и машинное обучение (продумайте функции подбора, аналогичные тем, которые генерируют множество Мандельброта).

Вот наглядное доказательство индукции. Если вы можете отсканировать эти четыре изображения слева направо и подумать, что у вас есть хорошая идея сгенерировать недостающие 5-е ... 6-е ... и т. Д. Изображения, то я только что запрограммировал вас как своего оракула NP для решения проблемы неграмового решения. существование. Пожалуйста, сделайте шаг вперед, чтобы получить свой приз как самый мощный суперкомпьютер в мире. Время от времени я буду кормить вас электричеством, пока мир благодарит вас за ваш вычислительный вклад.

Способ 2. Используйте преобразования Фурье на булевой версии изображения входов. БПФ предоставляют глобальную информацию о частоте и положении в экземпляре. В то время как часть величины должна быть одинаковой между входной парой, их фазовая информация совершенно другая - содержащая направленную информацию о проекции решения вдоль конкретной оси. Если вы достаточно умны, вы можете восстановить фазовое изображение решения с помощью некоторой специальной суперпозиции входных фазовых изображений. Затем обратное преобразование фазы и общей величины обратно во временную область решения.

Что может объяснить этот метод? Существует много перестановок булевых изображений с гибким заполнением между непрерывными сериями. Это позволяет сопоставлять решение input ->, заботясь о множественности, при этом сохраняя свойство FFT двунаправленных, уникальных отображений между временной областью <-> (частота, фаза). Это также означает, что нет такого понятия, как «нет решения». То, что он сказал бы, - то, что в непрерывном случае есть решения в градациях серого, которые Вы не рассматриваете, смотря на двухуровневое изображение традиционного решения головоломки неграммы.

Почему бы тебе не сделать это? Это ужасный способ на самом деле вычислить, так как БПФ в современном мире с плавающей запятой было бы очень неточно с большими экземплярами. Точность является огромной проблемой, и реконструкция изображений по квантованным величинам и фазовым изображениям обычно создает очень приблизительные решения, хотя, возможно, не визуально для порогов человеческого глаза. Также очень сложно придумать этот суперпозиционный бизнес, так как тип функции, фактически выполняющей его, в настоящее время неизвестен. Будет ли это простая схема усреднения? Наверное, нет, и нет особого метода поиска, кроме интуиции.

Метод 3. Найти правило клеточных автоматов (из возможных ~ 4 миллиардов таблиц правил для правил двух состояний фон Неймана), которое решает симметричную версию головоломки неграммы. Вы используете прямое встраивание проблемы в ячейки, показанные здесь.

Это, вероятно, самый элегантный метод с точки зрения простоты и хороших эффектов для будущего вычислительной техники. Существование этого правила не доказано, но я догадываюсь, что оно существует. Вот почему:

Nonograms требуют много хаотической обратной связи в алгоритме, чтобы быть точно решенным. Это установлено кодом перебора, связанным с Обзором кода. CA - почти самый способный язык для программирования хаотической обратной связи.

Это выглядит правильно, визуально. Правило будет развиваться путем встраивания, распространять информацию по горизонтали и вертикали, вмешиваться, а затем стабилизироваться до решения, которое сохранит количество заданных ячеек. Этот путь распространения идет по пути (назад), о котором вы обычно думаете, проецируя тень физического объекта в исходную конфигурацию. Nonograms происходит из особого случая дискретной томографии, так что представьте себе, что вы сидите одновременно в двух сканерах компьютерной томографии в углах котла ... именно так рентгеновские лучи будут распространяться для создания медицинских изображений. Конечно, существуют пограничные проблемы - границы вселенной CA не могут продолжать распространять информацию за пределами границ, если вы не разрешите использование тороидальной вселенной. Это также создает загадку как периодическую краевую задачу.

Это объясняет множественные решения как переходные состояния в непрерывно колеблющемся эффекте между заменой выходов в качестве входов и наоборот. Это объясняет случаи, которые не имеют решения, как оригинальные конфигурации, которые не сохраняют количество установленных ячеек. В зависимости от фактического результата нахождения такого правила, он может даже приблизительно неразрешимые случаи с близким решением , где клеточные состояния являются законсервированными.

C ++

Вот решение, которое гарантированно будет работать за полиномиальное время: оно работает O(n^k)там, где nнаходится число логических значений и kявляется константой по вашему выбору.

Это эвристически правильно, что, как я полагаю, говорит CS, потому что «оно дает правильный ответ большую часть времени, с небольшим количеством удачи» (и, в этом случае, достаточно большое значение k- отредактируйте это, на самом деле мне пришло в голову, что для любого фиксированного nвы можете установить так k, что n^k > 2^n- это обман?).

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

рубин / гнуплот 3d поверхность

(о, жесткая конкуренция!) ... в любом случае ... стоит ли картина тысячи слов? это 3 отдельных поверхностных графика, выполненных в gnuplot точки перехода SAT. оси (x, y) - это разделы и переменные, а высота z - это общее количество рекурсивных вызовов в решателе. код написан на ruby. это образцы 10x10 пунктов в 100 образцах каждый. он демонстрирует / использует основные принципы статистики и представляет собой симуляцию Монте-Карло .

в основном это алгоритм Дэвиса Патнама , работающий на случайных экземплярах, сгенерированных в формате DIMACS. это тот тип упражнений, который в идеале должен выполняться на уроках CS по всему миру, чтобы ученики могли изучать основы, но почти совсем не учат ... может быть, почему так много поддельных P? = NP доказательств ? нет даже хорошей статьи в Википедии, описывающей феномен точки перехода (кто-нибудь?), которая является очень важной темой в статистической физике и является ключевой также в CS. [a] [b] Есть много статей в CS о точке перехода однако очень немногие, кажется, показывают поверхностные участки! (вместо этого, как правило, показаны 2d срезы.)

экспоненциальное увеличение времени выполнения ясно видно на 1- ^м графике. седло, проходящее через середину 1- ^го сюжета, является точкой перехода. 2- ^й и 3- ^й графики показывают% выполнимого перехода.

[a] фазовый переход поведения в CS ppt Тоби Уолша
[b] эмпирическая вероятность выполнимости k-SAT tcs.se
[c] большие моменты в эмпирической / экспериментальной математике / (T) CS / SAT , блог 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
}