/* The Algorithm that is NOT Worth a Million Dollars:
A linear-time algorithm for SAT3
Copyright (c) 2007 Miguel A. Pizana.
http://xamanek.izt.uam.mx/map
map(at)xanum(dot)uam(dot)mx
This DOCUMENT is distributed under the terms of the
GNU Free Documentation License (GNU FDL) version 1.2
with no Invariant Sections, no Front-Cover Texts,
and no Back-Cover Texts.
(http://www.gnu.org/licenses/fdl.html)
This PROGRAM is distributed under the terms of the
GNU General Public License (GNU GPL) version 2
(http://www.gnu.org/licenses/gpl.html)
*** INTRODUCTION ***
This is a linear-time algorithm for SAT3...
YES, SAT3 stands for the satisfiability problem for Boolean expressions in
conjunctive normal form, with three literals per clause. This problem is known
to be NP-Complete.
HOWEVER, "linear-time" stands for linear-time on a Random-Access-Machine-
under-the-uniform-cost-criterion (uRAM). Therefore this algorithm does NOT
solve the P vs NP problem, to do so, we would need a linear-time algorithm
running on a Turing-Machine (TM) or running on a Random-Access-Machine-under-
the-logarithm-cost-criterion (lRAM). The lRAM model of computation is known
to be polynomially equivalent to the TM model, but uRAM is not.
The main difference is that the uRAM model assumes that basic operations can
be performed in constant time while the lRAM model acknowledges the fact that
basic operations such as x+y indeed require Omega(log2(x)+log2(y)) time
(multiplication is likely to require even more).
This code has been written therefore for educational purposes. It clearly
shows the dangers of taking the uniform cost criterion for Random Access
Machines (which is the most widely used when analyzing every-day algorithms)
too seriously. It also stresses the importance of knowing the difference
between uRAM and lRAM models, difference often disregarded in many textbooks.
The "Million Dollars" in the title refers, of course, to the Millennium Prize
Problems http://www.claymath.org/millennium/ from the Clay Mathematics
Institute.
*** WHAT DOES IT DO? ***
The program reads Boolean expressions from stdin and outputs TRUE if the
Boolean expression is satisfiable and FALSE otherwise. Boolean expressions are
coded using a list of space separated integers in the format:
c v n_{1} n_{2} n_{3} ... n_{3*c}
where "c" is the number of clauses, "v" is the number of variables and each
n_{i} is the number ( 1 <= n_{i} <= v ) of the variable occurring in the i-th
literal (and (i/3)-th clause), but if n_{i} is negative ( -v <= n_{i}<= -1 ),
it means that the literal is the negation of that variable instead.
For instance, the following codification:
3 4 -1 2 3 2 -4 -1 2 3 1
means:
(not(x1) or x2 or x3) and (x2 or not(x4) or not(x1)) and (x2 or x3 or x1).
*** HOW DOES IT DO IT? ***
In order to attain linear execution time (in the uRAM model) we take advantage
of the arbitrarily long integers that a uRAM can store at each memory cell. We
then use bitwise operations on these integers to perform many logical
operations in one step (in the uRAM).
The tricky part is the initialization of the array X. The code is designed
such that if (say) V=4 then the variables X[i] are initialized with the
following binary values are:
X[1]=1010101010101010
X[2]=1100110011001100
X[3]=1111000011110000
X[4]=1111111100000000
Therefore we can evaluate all the possible truth values of a clause using
bit-wise operations, for instance if the clause is:
x_{1} or not(x_{2}) or x_{3}
take
C = X[1] | ~X[2] | X[3]
to obtain:
C = 1111101111111011
which is a list of all the possible truths values of the clause, one for each
truth value assignment of the variables.
I'm using the multiple precision arithmetic library GMP (http://gmplib.org) in
order to make the program a little bit more interesting (this way we can
compute Boolean expressions with more variables than what would be allowed by
the extremely short 64/128-bit registers).
*** COMPILE ***
Compile using: g++ sat3.cc -lgmpxx -lgmp -o sat3
*/
#include
#include
#include
#include
#include
typedef mpz_class integer; //I just love the term 'integer'
//overloaded operator~ doesn't work as we wish, hence:
#define BitwiseNot(X) (Max-X)
int Fatal(char *s){printf("%s\n",s);exit(1);}
int
main(){
int C, V, N, i, j;
integer *X, Expr, Clause, Max;
std::cin >> C; //number of clauses
std::cin >> V; //number of variables
X = new integer[V+1]; // one for each variable, 0-th entry is unused.
if(!X) Fatal("Insuficient Memory");
//begin initialization of X[]
X[0]=2; //X[0] is not really used... except here.
for(i=0;i0;i--)X[i]=X[i+1] ^ (X[i+1]/X[i-1]);
//end Initialization of X[]
//Now read and compute the clauses:
for(i=0;i> N;
if(N>0){
Clause=Clause | X[N];
}else{ // N<0,
Clause=Clause | BitwiseNot(X[-N]);
}
}
Expr=Expr & Clause;
}
if(Expr==0){
//Not Satisfiable if all bits are set to cero:
std::cout << "FALSE\n";
}else{
//Satisfiable if some bit is set to one.
std::cout << "TRUE\n";
}
delete[] X;
return 0;
}