### So obviously, P = NP

• 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.

This question hits more than one closure criterion. Too broad: a problem which solves any problem in P meets the criteria. Too subjective and/or unclear: "*appears* to execute in polynomial time" is open to all kinds of interpretations.

Would it be better if we restrict problem choices to well-known NP problems, and remove the twist? I think *appears* to execute in polynomial time is what gives people flexibility for the popularity contest.

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.

Fair enough. I'll edit shortly.

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: I got the C# *compiler* to solve a SAT problem; I consider that to be a reasonably interesting achievement.

It would be fun if someone accidentally solves SAT in polynomial time here.

@Turion: S/He'd be recruited to the Laundry.

fyi further inquiry there are P vs NP tags on cs.se & tcs.se. see also how not to solve P=?NP cs.se and math monster/many P vs NP refs/stackexchange questions

@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.

Not thinking about the problem can sometimes make it easier.

@TimSeguine ...why?

Warhing: Do not do this in PHP. *Everything* is true if the PHP gods want it to be.

@NothingsImpossible: Women? Really?

I'm voting to close this question as off-topic because underhanded challenges are no longer welcome on this site. http://meta.codegolf.stackexchange.com/a/8326/20469

• ## 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: falsex2: truex3: 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.

You'll have to contact the clay mathematics institute for your million bucks. But I am not sure they will be _satisfied_.

This is absolutely amazing. Good job.

I think it's worth mentioning that this approach specifically solves 3-SAT, and can at best be generalized to solve K-SAT, for some finite K. However, afaict you cannot generalize this approach to solve general SAT, at least in a staticly typed language like C#.

@EricLippert: Actually, by nesting `Or` clauses (since `Or(x,y,z) == Or(x,Or(y,z))`), you can make the clauses arbitrarily long. Therefore, it is possible to solve SAT problems directly using the current framework.

@mneonneo: Arbitrarily long is not infinitely long. I could nest the clauses 1,000,000 times, but that would not allow me to solve 1,000,001-SAT, without writing a new program and recompiling. If I don't know the size of the input beforehand, this is not feasable.

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.

@JonathanPullano I believe everything above 1,000,000 can be considered an edge case and unexpected input, according to 1. and 2. in the question.

@Petr: I agree with you. I just to inform the readers and perhaps encourage someone to try something new.

@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.

@JonathanPullano: Nesting `Or`s gives you a way to **encode** arbitrary `SAT` problems in a manner consistent with the helper types already defined (this is distinct from converting SAT->3SAT because you encode the boolean logic directly). Plus, `SAT` isn't defined in terms of infinite-length clauses (that would make the problems infinitely long), but rather in terms of clauses that can be of arbitrary length.

@DiegodeEstrada: I did not know that -- thanks for the note!

@EricLippert: AFAIK the compiler errors should tell you if the problem is satisfiable or not (i.e. whether the invocations are ambiguous or unsatisfiable). Too bad it won't produce anything executable...

@nneonneo: That's correct.

@mneonneo: Encoding SAT problems is a fine approach, though that encoding not explicitly written in this code, and the challenge is to write a program that solves SAT (The solution is still valid as per Petr's comment). I was not referring to infinite length clauses though. To solve a SAT problem directly with this method with a finite but arbitrarily long number of clauses would require an infinite amount of code. This is because even though each individual input is finite, it can be arbitrarily high, and so there are an infinite number of cases for the code to check.

@JonathanPullano: I'm not following your train of thought here. Take your finite SAT problem. There's allegedly a polynomial algorithm to turn that into a "unique 3-SAT" problem. That will have a finite number n of variables and a finite number m of AND clauses, each clause having no more than three variables. Encode the variables by introducing n nested lambdas as I show, and encode the AND clauses with m nested calls to `And`. Run the compiler -- that's the non-polynomial step -- and then run the executable to get the answer.

@JonathanPullano: The contents of `Main()` constitute an encoding of the problem into C# code. **Encoding** is distinct from **transformation**; in the former case, you are simply translating the problem from mathematical terminology into a particular sequence of characters understood by the compiler, and in the latter you are creating a problem instance of a different problem which equivalently solves the original problem instance.

@EricLippert: My point actually is that you don't need to turn your SAT problem into a 3SAT problem because you can just nest `Or` clauses to get arbitrarily long boolean clauses.

Eric: I completely agree with you that transforming the problem to 3SAT is a valid answer. It might be nice to see that transformation explicitly, but even without that the answer is valid as per Petr's logic. mneonneo suggests that you can also encode arbitrarily long clauses to solve general SAT directly, however unless I am misunderstanding how he does this, I think you could only solve an instance of K-SAT this way, but not general SAT, because in the general case you would need to list out an infinite number of cases in code. This is getting a bit off-topic though guys :)

Nit: UNIQUE-3SAT, the problem you are solving here, is **not** NP-complete. It is co-NP-complete, and it is widely thought (though not proven) that co-NP != NP. So, technically, this answer does not solve a known NP-complete problem.

@JonathanPullano: Why would you need to list out an infinite number of cases? For example, we can encode `(x v y v z v w)` as `Or(Or(x,y,z),x,w)`, without having to create a 4-argument version of the `Or` function.

@nneonneo: I am learning all kinds of new things today, thanks!

@nneonneo: Thanks, I now follow what you are saying. I suppose an ideal answer would take in some input and then generate the source code above via your encoding, but that is really just a technicality.

Nitpicking: The code above isn't really the *program*, it is the **input**. The program that is solving 3-SAT is the **C# compiler**. The solution is the **compiled program** - it already contains the solution, you don't even have to run it. The run time of the compiled program is irreverent - the complexity is of the run time is inside the compiler. All of this isn't very important, but I wouldn't give you a million dollars. Thanks for this answer and for the interesting discussion is created!

@Kobi even if he *did* solve P=NP, I don't think many people here would have the means/will to give him a million dollars. I, for starters, surely wouldn't.