So obviously, P = NP

Question

SAT is the problem of determining whether a boolean expression can be made true. For example, (A) can be made true by setting A=TRUE, but (A && !A) can never be true. This problem is known to be NP-complete. See Boolean Satisfiability.

Your task is to write a program for SAT that executes in polynomial time, but may not solve all cases.

For some examples, the reason it is not really polynomial could be because:

1. There is an edge case that is not obvious but has a poor runtime
2. The algorithm actually fails to solve the problem in some unexpected case
3. Some feature of the programming language you are using actually has a longer runtime than you would reasonably expect it to have
4. Your code actually does something totally different from what it looks like it's doing

You may use any programming language (or combination of languages) you wish. You do not need to provide a formal proof of your algorithm's complexity, but you should at least provide an explanation.

The primary criteria for judging should be how convincing the code is.

This is a popularity contest, so the highest rated answer in a week wins.

Answer 1

C#

Your task is to write a program for SAT that appears to execute in polynomial time.

"Appears" is unnecessary. I can write a program that really does execute in polynomial time to solve SAT problems. This is quite straightforward in fact.

MEGA BONUS: If you write a SAT-solver that actually executes in polynomial time, you get a million dollars! But please use a spoiler tag anyway, so others can wonder about it.

Awesome. Please send me the million bucks. Seriously, I have a program right here that will solve SAT with polynomial runtime.

Let me start by stating that I'm going to solve a variation on the SAT problem. I'm going to demonstrate how to write a program that exhibits the unique solution of any 3-SAT problem. The valuation of each Boolean variable has to be unique for my solver to work.

We begin by declaring a few simple helper methods and types:

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

Now let's pick a 3-SAT problem to solve. Let's say

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

Let's parenthesize that a bit more.

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

We encode that like this:

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

And sure enough when we run the program, we get a solution to 3-SAT in polynomial time. In fact the runtime is linear in the size of the problem!

x1: false
x2: true
x3: false

You said polynomial runtime. You said nothing about polynomial compile time. This program forces the C# compiler to try all possible type combinations for x1, x2 and x3, and choose the unique one that exhibits no type errors. The compiler does all the work, so the runtime doesn't have to. I first exhibited this interesting techinque on my blog in 2007: http://blogs.msdn.com/b/ericlippert/archive/2007/03/28/lambda-expressions-vs-anonymous-methods-part-five.aspx Note that of course this example shows that overload resolution in C# is at least NP-HARD. Whether it is NP-HARD or actually undecidable depends on certain subtle details in how type convertibility works in the presence of generic contravariance, but that's a subject for another day.

Answer 2

Multi-language (1 byte)

The following program, valid in many languages, mostly functional and esoteric, will give the correct answer for a large number of SAT problems and has constant complexity (!!!):

0

Amazingly, the next program will give the correct answer for all remaining problems, and has the same complexity. So you just need to pick the right program, and you'll have the correct answer in all cases!

1

Answer 3

JavaScript

By using iterated non-determinism, SAT can be solved in polynomial time!

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

Example usage:

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

This algorithm just checks given boolean formula a thousand times with random inputs. Almost always works for small inputs, but is less reliable when more variables are introduced.

By the way, I'm proud that I had the opportunity to utilize two of the most underused features of JavaScript right next to each other: eval and with.

Answer 4

Mathematica + Quantum Computing

You may not know that Mathematica comes with quantum computer aboard

Needs["Quantum`Computing`"];

Quantum Adiabatic Commputing encodes a problem to be solved in a Hamiltonian (energy operator) in such way that its state of minimum energy ("ground state") represents the solution. Therefore adiabatic evolution of a quantum system to the ground state of the Hamiltonian and subsequent measurement gives the solution to the problem.

We define a subhamiltonian that corresponds to || parts of the expression, with appropriate combination of Pauli operators for variables and its negation

Where for expression like this

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

the argument should look like

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

Here is the code to construct such argument from bool expression:

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

Now we construct a full Hamiltonian, summing up the subhamiltonians (the summation corresponds to && parts of the expression)

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

And look for the lowest energy state

QuantumEigensystemForm[H, -1]

If we got an eigenvalue of zero, then the eigenvector is the solution

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

Unfortunately the official site for the "Quantum Computing" add-on is not active and I can't find a place to download it, I just still had it installed on my computer. The Add-on also have a documented solution to the SAT problem, on which I based my code.

Answer 5

Three approaches here, all involve a reduction of SAT into its 2D geometric lingua franca: nonogram logic puzzles. Cells in the logic puzzle correspond to SAT variables, constraints to clauses.

For a full explanation (and to please review my code for bugs!) I've already posted some insight to patterns within the nonogram solution space. See https://codereview.stackexchange.com/questions/43770/nonogram-puzzle-solution-space . Enumerating >4 billion puzzle solutions and encoding them to fit in a truth table shows fractal patterns -- self-similarity and especially self-affinity. This affine-redundancy demonstrates structure within the problem, exploitable to reduce the computational resources necessary to generate solutions. It also shows a need for chaotic feedback within any successful algorithm. There is explanatory power in the phase transition behavior where "easy" instances are those that lie along the coarse structure, while "hard" instances require further iteration into fine detail, quite hidden from normal heuristics. If you'd like to zoom into the corner of this infinite image (all <=4x4 puzzle instances encoded) see http://re-curse.github.io/visualizing-intractability/nonograms_zoom/nonograms.html

Method 1. Extrapolate the nonogram solution space shadow using chaotic maps and machine learning (think fitting functions similar to those that generate the Mandelbrot Set).

Here is a visual proof of induction. If you can scan these four images left to right and think you have a good idea to generate the missing 5th... 6th... etc. images, then I have just programmed you as my NP oracle for the decision problem of nonogram solution existence. Please step forth to claim your prize as the world's most powerful supercomputer. I'll feed you jolts of electricity every now and then while the world thanks you for your computational contributions.

Method 2. Use Fourier Transforms on the boolean image version of inputs. FFTs provide global information about frequency and position within an instance. While the magnitude portion should be similar between the input pair, their phase information is completely different -- containing directionalized information about a solution projection along a specific axis. If you're clever enough you might reconstruct the phase image of the solution via some special superposition of the input phase images. Then inverse transform the phase and common magnitude back to the time domain of the solution.

What could this method explain? There are many permutations of the boolean images with flexible padding between contiguous runs. This allows a mapping between input -> solution taking care of multiplicity while still retaining FFTs' property of bidirectional, unique mappings between time domain <-> (frequency, phase). It also means there's no such thing as "no solution." What it would say is that in a continuous case, there are greyscale solutions that you're not considering when looking at the bilevel image of traditional nonogram puzzle solving.

Why wouldn't you do it? It's a horrible way to actually compute, as FFTs in today's floating-point world would be highly inaccurate with large instances. Precision is a huge problem, and reconstructing images from quantized magnitude and phase images usually creates very approximate solutions, although maybe not visually for human eye thresholds. It's also very hard to come up with this superpositioning business, as the type of function actually doing it is currently unknown. Would it be a simple averaging scheme? Probably not, and there's no specific search method to find it except intuition.

Method 3. Find a cellular automata rule (out of a possible ~4 billion rule tables for von Neumann 2-state rules) that solves a symmetric version of the nonogram puzzle. You use a direct embedding of the problem into cells, shown here.

This is probably the most elegant method, in terms of simplicity and good effects for the future of computing. The existence of this rule isn't proven, but I have a hunch it exists. Here's why:

Nonograms require lots of chaotic feedback in the algorithm to be solved exactly. This is established by the brute force code linked to on Code Review. CA is just about the most capable language to program chaotic feedback.

It looks right, visually. The rule would evolve through an embedding, propogate information horizontally and vertically, interfere, then stabilize to a solution that conserved the number of set cells. This propogation route follows the path (backwards) that you normally think of when projecting a physical object's shadow into the original configuration. Nonograms derives from a special case of discrete tomography, so imagine sitting concurrently in two kitty-cornered CT scanners.. this is how the X-rays would propogate to generate the medical images. Of course, there are boundary issues -- the edges of the CA universe cannot keep propogating information beyond the limits, unless you allow a toroidal universe. This also casts the puzzle as a periodic boundary value problem.

It explains multiple solutions as transient states in a continuously oscillating effect between swapping outputs as inputs, and vis versa. It explains instances that have no solution as original configurations that don't conserve the number of set cells. Depending on the actual outcome of finding such a rule, it may even approximate unsolvable instances with a close solution where the cell states are conserved.

Answer 6

C++

Here is a solution that is guaranteed to run in polynomial time: it runs in O(n^k) where n is the number of booleans and k is a constant of your choice.

It is heuristically correct, which I believe is CS-speak for "it gives the correct answer most of the time, with a bit of luck" (and, in this case, an appropriately large value of k - edit it actually occurred to me that for any fixed n you can set k such that n^k > 2^n - is that cheating?).

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

Answer 7

ruby/gnuplot 3d surface

(ooh stiff competition!) ... anyway ... is a picture worth a thousand words? these are 3 separate surface plots made in gnuplot of the SAT transition point. the (x,y) axes are clause & variable count and the z height is total # of recursive calls in the solver. code written in ruby. it samples 10x10 points at 100 samples each. it demonstrates/uses basic principles of statistics and is a Monte Carlo simulation.

its basically a davis putnam algorithm running on random instances generated in DIMACS format. this is the type of exercise that ideally would be done in CS classes around the world so students could learn the basics but is almost not taught specifically at all... maybe some reason why there are so many bogus P?=NP proofs? there is not even a good wikipedia article describing the transition point phenomenon (any takers?) which is a very prominent topic in statistical physics & is key also in CS.[a][b] there are many papers in CS on the transition point however very few seem to show surface plots! (instead typically showing 2d slices.)

the exponential increase in runtime is clearly evident in 1^st plot. the saddle running through the middle of 1^st plot is the transition point. the 2^nd and 3^rd plots show the % satisfiable transition.

[a] phase transition behavior in CS ppt Toby Walsh
[b] empirical probability of k-SAT satisfiability tcs.se
[c] great moments in empirical/experimental math/(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
}