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 NP-complete problem, as proved by Stephen Cook in 1971 (see Cook's theorem for the proof). Until that time, the concept of an NP-complete problem did not even exist. The problem remains NP-complete even if all expressions are written in conjunctive normal form with 3 variables per clause (3-CNF), 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 k-SAT (the general case) reduces to 3-SAT, and 3-SAT can be proven to be NP-complete, it can be used to prove that other problems are also NP-complete. This is done by showing how a solution to another problem could be used to solve 3-SAT.

(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".