Satisfiability Problem
Satisfiability is the problem of determining if the variables of a
given Boolean formula can be assigned in such a way as to make the
formula evaluate to TRUE. Equally important is to determine whether no
such assignments exist, which would imply that the function expressed
by the formula is identically FALSE for all possible variable
assignments. In this latter case, we would say that the function is
unsatisfiable; otherwise it is satisfiable.
In complexity theory, the Boolean satisfiability problem (SAT) is a
decision problem, whose instance is a Boolean expression written in
conjunctive normal form (CNF). The question is: given the expression,
is there some assignment of TRUE and FALSE values to the variables
that will make the entire expression true?
SAT was the first known NPcomplete problem, as proved by Stephen Cook
in 1971 (see Cook's theorem for the proof). Until that time, the
concept of an NPcomplete problem did not even exist. The problem
remains NPcomplete even if all expressions are written in conjunctive
normal form with 3 variables per clause (3CNF), yielding the 3SAT
problem. This means the expression has the form:
(x11 OR x12 OR x13) AND
(x21 OR x22 OR x23) AND
(x31 OR x32 OR x33) AND ...
where each x is a variable or a negation of a variable, and each
variable can appear multiple times in the expression.
Since kSAT (the general case) reduces to 3SAT, and 3SAT can be
proven to be NPcomplete, it can be used to prove that other problems
are also NPcomplete. This is done by showing how a solution to
another problem could be used to solve 3SAT.
(source: Wikipedia)
The idea of Brejova et al.
to solve the SAT problem, is to split it into two distinct
subproblems. A fundamental assumption for solving SAT is that the
variables in the clauses are always the same, i.e. variable x1 in
clause 1 has the same truth assignment as variable x1 in clause
2. Brejova et al. sacrifice this assumption for a simpler
algorithm. In this way the first subproblem is to find truth
assignments that satisfies the given formula where the variables for
each clause are completely independent. Given a formula with n
variables and m clauses one now has not only to check 2^n possible
truth assignments but 2^(n*m). This subproblem is solved by the SAT
algebra within the ADP program. The second subproblem becomes
necessary to assure that only such answers, found in subproblem one,
are valid that first satisfy the formula and second have equal truth
assignments for each variable in all clauses. The second aspect is the
tasks of the EQA algebra.
A given formula with three variables and two clauses in CNF could be:
(x1 OR x2) AND (NOT(x2) OR x3). For the classical way exist 2^3 = 8
different truth assignments that maybe satisfy the formula. In
Brejovas variant there are 2^(2*3) = 64 truth assignments that have to
be checked. The SAT algebra would find 36 satisfying answers, but many
of these have contradicting assignments for e.g. x2. The EQA algebra
filters all 8 answers out of the overall 64 answers, where x1, x2 and
x3 have the same value for each clause. That are exactly those 8
possible truth assignments from the classical way. The combination of
both algebras can solve the SAT problem: (sat *** eqa).
To calculate the example formula with ADP one has to encode it to a
machine readable code. A "formula" consists of one or more "clauses",
that must be separated by a '&' character. One clause is composed of
one ore more "literals" in direct concatenation. A literal could
either be positive 'P', negative 'N' or missing ''. The first clause
from the example has two positive literals followed by a missing
one. So its representation is "PP". The second clause is "NP" and
the complete encoded formula is "PP&NP".
