Genetic Algorithm Based Solution to SAT-3 Problem

Veiw figure View Figure

4. NP Complete Problem

There are basically two types of problems

• Polynomial-time problems.

• NP problems.

Polynomial-Time problems-Problems that have algorithms with worst case running time of O(nk), where k is a constant, are called tractable others are called intractable or super-polynomial ^[17].

NP problems- Another class of algorithms that are “verifiable” in polynomial time is called NP problems. Any problem in P is also in NP ^[18].

We say that a language M, defining some decision problem, is NP-hard if every other language L in NP is polynomial-time reducible to M. If a language M is NP –hard and it is also in the class NP itself, then M is NP-complete ^[19].

Thus, an NP –complete problem is, in a very formal sense, one of the hardest problems in NP, as far as polynomial-time computability is concerned. If anyone finds a deterministic polynomial-time algorithm for even one NP-complete problem, then P=NP. ^[19] Figure 2 shows the relation of complexity classes.

Figure 2. Relation of Complexity Classes

Download as

Veiw figure View Figure

Definition: A Boolean formula is in 3SAT if it is in 3CNF form and is also satisfiable. A Boolean formula is in 3CNF if it is of the form

C1∧C2∧•••∧C3

Where, each Ci is an “AND” of three or less literals. ^[20].

5. Existing Approaches To SAT3 Problem

5.1. Brute Force Algorithm

The simplest but also the most time consuming idea. The main approach is to try every possible valuation until a satisfying one is found or there are no more valuations left. It is guaranteed to find a solution but has a slow run-time performance ^[21].

Implementation of this algorithm involves taking a number of variables and the Boolean function as input from the user. Then a 2D array is used as the data structure to store all the possible 2n combinations of values of all the variables. Then each row of the 2D array is used to insert values of variables in the given Boolean function to check its satisfiability, thus in a worst case scenario, all the possible combinations are tried until the solution is obtained.

Complexity-This approach works well for small inputs i.e. Small no of variables and simple functions. But since it is exponential in nature, its run-time complexity is O (2n) in the worst case. Thus, when the number of variables becomes large the algorithm fails to find optimal solution within practical time limit.

Table 1. Literature Review

Download as

Veiw figure View Table

5.2. Davis Putnum Algorithm

The algorithm works on a propositional formula ф. ф should be in CNF form. The algorithm treats ф as a set of clauses that can be manipulated. It defines 3 basic principles for obtaining the answer.

5.2.1 Unit Propagation Rule

Rule I deals with simplifying the formula for determining satisfiability by analyzing one-literal clauses. There are three cases to be distinguished.

Case 1: an atomic formula p occurs as a one-literal clause in both positive and negated form. In this case the resulting formula ф is unsatisfiable, because the empty clause can be deduced by means of resolution.

Case 2: Case 1 does not apply and an atomic formula p occurs as a one literal clause. Then all clauses that contain p can be deleted and -p can be removed from the remaining clauses.

Case 3: Case 1 does not apply and an atomic formula -p occurs as a one literal clause. Then all clauses that contain -p can be deleted and p can be removed from the remaining clauses.

5.2.2. Pure literal Rule

It deals with redundant clauses. It is generally used as a preprocessing step for efficiency reasons. If only p or only -p occurs in the formula, then all clauses which contain p or -p may be deleted.

5.2.3. Resolution Rule

Resolution can be applied to two clauses that have complementary literals L and L’ such that L ≡ -L’. With the help of the resolution step these two clauses can be combined in a single clause called the resolvent that contains all the literals without L and L’ ^[21].

Complexity-The fact that this is an exponential algorithm follows directly from the fact that regular resolution is exponential. This means that this algorithm will generate an exponential number of clauses and thus is very memory inefficient. The lower bound complexity of this algorithm has been proven to be 2cn for some constant c > 0 ^[21]. Figure 3 depicts the basic steps involved in Davis Putnum Algorithm.

Figure 3. Basic steps in Davis-Putnum algorithm

Download as

Veiw figure View Figure

5.3. Davis Logemann and Loveland Algorithm

In this algorithm rule III of Davis Putnum Algorithm was replaced by splitting rule in order to limit the amount of memory used during runtime.

• The simplifying of the formula is now usually done as a preprocessing step for efficiency reasons.

• Heuristics for the branching variable are used

• Backtracking has been replaced by back jumping or non-chronological backtracking in iterative versions of the DLL, so that similar parts of the same tree are not searched over and over again. ^[21]

• New clauses can be ascertained during the search process to increase the amount of branches that can be cut away from the search tree later.

• Improvements in Boolean Constraint Propagation algorithms are introduced.

• Random restarts of the algorithm that make use of previously learned information increase the chances of coming to a solution faster

• For these improvements to be efficient and also to allow non-chronological backtracking the DLL algorithm is usually implemented iteratively ^[21].

Complexity- In general, DPLL requires exponential time (splitting rule!)! Heuristics are needed to determine which variable should be instantiated next and which value should be used.

DPLL is polynomial on Horn clauses, i.e., Clauses with at most one positive literal -A1,V…V-An V B ^[22].

5.4. Binary Decision Diagrams (BDD)

Figure 4. Basic steps in Binary Decision Diagrams

Download as

Veiw figure View Figure

A BDD represents a formula ф (seen as a Boolean function) as a rooted directed acyclic graph G = (V, T, E). Each non-terminal node or vertex v(i) ϵ V is labeled by a variable x and has edges directed towards two successor nodes, called the then-child and the else-child. In a graphical representation, the then-child represents x = 1 via an uninterrupted line and the else-child represents x = 0 via a dotted line. The lines are depicted as undirected for simplicity, but must always be considered as directed to the next node. Each terminal node t(i) ϵ T is labeled with 0 or 1 and does not have any children. For a given assignment of the variables, the value of the function is found by tracing a path from the root to a terminal vertex following the branches indicated by the values assigned to the variables ^[21].

Using reduced order Binary Decision Diagram a set of satisfying assignments is created by looking at the constraints.

The process is to continuously add clauses to an empty BDD until the perfect pattern is described. By adding all the constraint paths to the BDD we get the complete representation of the function for which the satisfiability is being checked. This method solves the problem by building up the solution set in order to verify satisfiability.

Complexity- ROBDDs perform worse, both in terms of space and time complexity in under constrained and critically constrained set of problems. It only works best in over constrained sets of problems ^[21]. Figure 4 shows the steps involved in Binary Decision Diagram approach.

5.5. Set Theory

Set theory based approach decides the un-satisfiability of a given formula. It describes the problem in set theory and investigates what is needed to decide the un-satisfiability of a given sat3 formula.

For a SAT3 function ф of n variables the set V_φ of possible valuations (variable assignments) v is determined, for which v(ф) evaluates to 1. Here v is a mapping {x0::: xn-1} → {0,1} that instantiates every variable to 0 or 1. So each function vi can be depicted as a unique number in binary representation, which is in the set 2n that denotes n-tuples over a binary alphabet {0, 1} n. If any clause that is part of ф is unsatisfiable, then ф is also unsatisfiable. That is, v(ci) = 0 => v(ф) = 0. Using this information, any 3-SAT formula can be proven (un) satisfiable using sets ^[21].

Complexity-This solution is not computationally possible with a high amount of clauses and takes more time than applying brute-force approach to all 2n possible valuations ^[21].

6. Proposed Solution

This work proposes Gas based solution to SAT-3 problem. The algorithm has been presented as follows. The algorithm uses the blend of the theory of natural selection and conventional optimization.

ALGORITHM: SAT-3 problem

1. cell->number of variables

2. expression->given Boolean formula

3. chromosome-> representation of values assigned to the variables of given Boolean formula

4. expression_evaluate->truth value of expression

5. //initial population generation

6. for each chromosome //no. of iterations/initial population ??

7. for each cell

8. If (random () % 100> 50)

9. cell=1;

10. else

11. cell=0;

12. end if

13. end for

14. end for

15. //count number of true values

16. for each chromosome

17. If (expression_evaluate == TRUE)

18. count++;

19. end if

20. end for

21. //crossover

22. for each chromosome-> till crossover_rate

23. chromo some 1=random () % population;

24. chromo some 2=random () % population;

25. crossover_point=random () % cell;

26. for each cell-> beginning to crossover_point

27. chromo some 3[i] = chromo some 1[i];

28. chromo some 4[i] = chromo some 2[i];

29. end for

30. for each cell->crossover_point to end

31. chromo some 3[i] = chromo some 2[i];

32. chromo some 4[i] = chromo some 1[i];

33. end for

34. end for

35. for each chromosome

36. If (expression_evaluate==TRUE)

37. count++;

38. end if

39. end for

40. //mutation

41. for each chromosome->till mutation_rate

42. mutation_point=random () % cell;

43. If (cell[mutation_point]==1)

44. cell[mutation_point]=0;

45. else

46. cell[mutation_point]=1;

47. end if

48. end for

49. for each chromosome

50. If (expression_evaluate==TRUE)

51. count++;

52. End if

53. End for

7. Results

The following tables (Table 2, Table 3, Table 4, Table 5) show the obtained results. Due to time constraints we have considered the case of 4 variables and 7, 8, 9 and 10 clauses. Further analysis with more number of variables and clauses will be considered for future work.

In the following tables the first column shows the no. of true values generated randomly when initial population is formed.

The second column shows the Cross-over Rate. The third column shows the number of true values generated w.r.t the mentioned crossover rate. The fourth column shows the Mutation Rate. Finally, The last column shows the no. of true values generated w.r.t the mentioned mutation rate.

Table 2 shows the results for 4 variables and 7 clauses, Table 3 shows the results for 4 variables and 8 clauses, Table 3 shows the results for 4 vriables and 9 clauses, Table 3 shows the results for 4 variables and 10 clauses.

Table 2. 4 Variables, 7 Clauses (#{A}||#{B}||#{C})&&(#{D}||!#{A}||#{C})&&(!#{B})&&(!#{C}||!#{A})&&(#{A}||!#{B})&&(!#{A}||!#{B}||!#{C})&&(!#{D}||#{C}||#{A})

Download as

Veiw figure View Table

Table 2. 4 Variables, 8 Clauses (#{A}||#{B}||#{C})&&(#{B}||#{C}||#{D})&&(#{C}||#{D}||#{B})&&(#{A}||#{B}||#{D})&&(#{B}||#{D}||#{A})&&(#{A}||#{B}||!#{C})&&(!#{A}||#{C}||#{D})&&(#{C}||!#{D})

Download as

Veiw figure View Table

Figure 5. Graph showing variation in no. of solution with different Crossover Rates

Download as

Veiw figure View Figure

Table 3. 4 Variables, 9 Clauses (#{A}||#{B}||#{C})&&(#{D}||!#{A}||#{C})&&(!#{B})&&(!#{C}||!#{A})&&(#{A}||!#{B})&&(!#{A}||!#{B}||!#{C})&&(!#{D}||#{C}||#{A})&&(!#{A}||#{B}||#{C})&&(!#{A}||#{B}||#{D})&&(!#{A}||!#{B}||!#{D})

Download as

Veiw figure View Table

Table 4. 4 Variables, 10 Clauses (#{A}||#{B}||#{C})&&(#{D}||!#{A}||#{C})&&(!#{B})&&(!#{C}||!#{A})&&(#{A}||!#{B})&&(!#{A}||!#{B}||!#{C})&&(!#{D}||#{C}\||#{A})&&(!#{A}||#{B}||#{C})&&(!#{A}||#{B}||#{D})&&(!#{A}||!#{B}||!#{D})

Download as

Veiw figure View Table

Figure 6. Graph showing variation in no. of solution with different Mutation Rates

Download as

Veiw figure View Figure