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.
