Saturday, July 25, 2015

Reduction from SAT to Clique (proving NP-complete)



SAT problem description:

Assume a boolean expression in CNF (conjuctive normal form). The question for this decision problem is, can you set the variables to a combination of TRUE/FALSE so that the boolean expression becomes true.
(Using the laws of Boolean algebra, every boolean expression can be transformed into an equivalent conjuctive normal form, which may, however , be exponentially longer).

In order to show reduction from SAT to Clique, i have to transform the input of the SAT into an input for Clique ( Boolean expression to graph ).
SAT is a NP-complete problem.

BE = (x1 or x2) and (-x2 or x3) and (-x3 or x1 or x2)
This Bollean expression has 3 clauses:
Clause_1 contains x1, x2
Clause_2 contains -x2, x3
Clause_3 contains -x3, x1, x2

The graph is going to have as vertexes as the variables in BE (7 vertices).
Every vertex is going to connect with all the others. Attention, there is no connection among the vertices that belong to the same clause,  and also, there is no connection between the
xi,-xi vertices.

Now it's time to construct the graph

This is the input graph for clique. A max clique for this graph is c1:(x2, x3, x1), another max clique is c2:(x1, x3, x1)

From reduction's definition you know that, solving problem Y (Clique) on transformed input yields some answer as solving X (SAT) on original input.

So if  i set the variables x2, x3, x1 (c1 clique result) to TRUE at the same time,then boolean's expression result should be TRUE. 

We just prove reduction from SAT to Clique. We prove also, that Clique is a NP-complete problem!!!

Below, is presented a function, which take as its input a boolean formula and assignments of the variables and returns TRUE if the formula is satisfied by the assignment and False otherwise. 

def is_satisfied(clauses, assignment):
    
    counter = 0    for clause in clauses:
        for item in clause:
            if item > 0:
                if assignment[item] == 1:
                    counter += 1                    break            else:
                if assignment[abs(item)] == 0:
                    counter += 1                    break
    if counter == len(clauses):
        return True    else:
        return False

def test():
    clauses = [[1,2,-3],[2,-4],[-1,3,4]]
    assignment = [0,1,1,1,1]
    assert is_satisfied(clauses, assignment)

    assignment = [0,1,0,1,1]
    assert not is_satisfied(clauses, assignment)

print test()

No comments:

Post a Comment