Take the 2-minute tour ×
Programming Puzzles & Code Golf Stack Exchange is a question and answer site for programming puzzle enthusiasts and code golfers. It's 100% free, no registration required.

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.

share|improve this question
11  
It would be better if you restrict the problem domain, otherwise you invoke the cloud of uncertainty around what is "well-known". Why not pick a single NP-hard problem and focus on that? That has the advantage of leaving other such problems open to future questions along the same line. Several narrow questions can provide far more ongoing delight and entertainment to the site than one broad one. –  Jonathan Van Matre Mar 17 at 16:38
1  
Can't add comments yet... Eric Lippert's "solution" is of course a sleight of hand. The C# language requires the compiler to do all the work. So given a 3SAT problem, you can ask the C# compiler to solve it, which will take exponential time. With that done, the C# compiler generates a program that solves one instance of 3SAT in linear time. Now since the solution of any instance of any NP complete problem is either YES or NO, that's not really much of an achievement. –  gnasher729 Mar 18 at 8:57
7  
@gnasher729: I got the C# compiler to solve a SAT problem; I consider that to be a reasonably interesting achievement. –  Eric Lippert Mar 18 at 22:07
6  
It would be fun if someone accidentally solves SAT in polynomial time here. –  Turion Mar 19 at 16:06
3  
@Turion decades of Research, millions in rewards and prizes and all the women and fame one could have - but the real motivation for solving P=NP will end up being this PCG challenge. –  NothingsImpossible Mar 22 at 0:20

7 Answers 7

up vote 222 down vote accepted

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.

share|improve this answer
83  
You'll have to contact the clay mathematics institute for your million bucks. But I am not sure they will be satisfied. –  Jonathan Pullano Mar 17 at 20:01
13  
Of course any SAT problem can be transformed into an equivalent 3-SAT problem, so this restriction is merely an inconvenience. The more vexing issue with my "solution" is that it requires that the problem have a unique solution. If there is no solution or more than one solution then the compiler gives an error. –  Eric Lippert Mar 17 at 23:04
10  
@EricLippert the uniqueness requirement is ok. You can always reduce SAT to Unique-SAT (SAT but assuming the inputs have 0 or 1 assignments) using a polynomial time randomized reduction. Keywords: Isolation Lemma, Valiant-Vazirani theorem. –  Diego de Estrada Mar 18 at 0:02
36  
"Seriously, I have a program right here that will solve SAT with polynomial runtime." - me too, but unfortunately it does not fit in this comment box. –  CompuChip Mar 18 at 11:00
9  
@Kobi: Yes, that's the joke. –  Eric Lippert Mar 18 at 13:48

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
share|improve this answer
5  
This is amazing. I had myself a good laugh. –  Karl Damgaard Asmussen Mar 18 at 13:16
2  
Absolutely f****** brilliant! –  The Blue Dog Mar 18 at 18:57
69  
Hmm. It's easy now. All I need to do is write a program that will pick the right program! –  Cruncher Mar 19 at 13:48
    
Precisely ! :-) –  Mau Mar 19 at 13:50
5  
Reminiscent of xkcd.com/221. –  msh210 Mar 21 at 6:43

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.

share|improve this answer
3  
This is actually a well established testing method. Haskell's QuickCheck library started all the fun, I believe. It has since been reimplmented in many languages. –  John Tyree Mar 17 at 21:10
3  
I think it should be noted that, this program is less likely to return the correct answer, the bigger the sat expression. The 1000 in the for loop should somehow scale with the input size(some polynomial non-O(1) scaling). –  Cruncher Mar 18 at 14:32
1  
@Cruncher To be more precise, the larger the number of variables, the less likely it is to return the correct answer. (e.g. a very long expression with a single variable will almost always return the correct answer) –  Peter Olson Mar 18 at 14:45
1  
@TimSeguine I admit that my use of the word "nondeterministic" in this context is dubious at best, just like the claim that SAT can be solved in polynomial time. I know it's not correct, it's just part of the game of deception. –  Peter Olson Mar 19 at 19:30
3  
@PaulDraper and then call them underused! I had a nice laugh! –  Rob Mar 20 at 16:01

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

enter image description here

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]

enter image description here

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.

share|improve this answer
15  
I have no idea how this answer works. +1 –  Jonathan Pullano Mar 19 at 20:07
4  
@XiaogeSu "Naturally". –  swish Mar 21 at 0:14
3  
@XiaogeSu Evolution determined by the Hamiltonian, and naturally it evolves to the lowest energy. So knowing the spectrum, we can assume that the system will end up in the ground state. –  swish Mar 21 at 0:30
3  
@XiaogeSu in order to go to the ground state, one also needs to have an interaction with the environment that deexcitates the higher states, you're right. The idea here is that this interaction is very small, "adiabatic". –  Turion Mar 22 at 1:11
3  
fyi adiabatic QM computing has a lot of similarities to classical simulated annealing. now implemented by Dwave. its similar to a "cooling" temperature/energy system that "finds/settles" in local minima. –  vzn Mar 22 at 14:34

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 http://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).

http://i.stack.imgur.com/X7SbP.png

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. Conservative, symmetric nonograms

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.

share|improve this answer
2  
+1 for leaving me saying "why didn't I think of that?" :P –  Navin Mar 24 at 22:53
    
You are Stephen Wolfram and I claim my five pounds! –  Quuxplusone Mar 25 at 5:12
3  
This answer really deserves more credit, as it's the best attempt to make a convincing program. Good show. –  Jonathan Pullano Apr 2 at 16:23

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;
  }
}
share|improve this answer
    
Good answer. I would put the explanation in a spoiler tag so people can stare at it and scratch their head a bit. –  Jonathan Pullano Mar 19 at 18:28
    
Thanks for the suggestion @JonathanPullano, I've added a spoiler tag and obfuscated the code a bit. –  CompuChip Mar 19 at 18:38
    
By the way, I only just found out about bitfield, maybe I would have preferred that over std::vector. –  CompuChip Mar 19 at 18:38
2  
+1 for the creative obfuscation and hitchhiker's references –  Blake Miller Mar 20 at 1:12
1  
Yes of course that's cheating, if k depends on n it's not much of a constant :-) –  RemcoGerlich Mar 23 at 20:17

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 1st plot. the saddle running through the middle of 1st plot is the transition point. the 2nd and 3rd 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

enter image description here enter image description here enter image description here

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
}
share|improve this answer
2  
I'm glad you contributed this answer. In any successful proof of P versus NP (either way) it's one of many requirements for predictive power. Thanks for pointing out its importance. :) –  Joel Snyder Mar 25 at 0:20

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.