Algorithms For Dummies

  Performing Local Search 

     353

n = 1000

# Solvable seeds with n=1000 : 0,1,2,3,4,5,6,9,10

# Unsolvable seeds with n=1000 : 8

clauses = create_clauses(n, seed=0)

history, solution = sat2(clauses, n,

        start=create_random_solution)

Found solution in 1 external loops, 1360 internal loops

Plotting the solution, as a chart representing the number of steps on the abscissa 

(random emendations of the solution) and the clauses left to fix on the ordinal 

axis, you can verify that the algorithm tends to find the correct solution in the 

long run, as shown in Figure 18-5.

plt.plot(np.array(history), 'b-')

plt.xlabel("Random adjustments")

plt.ylabel("Unsatisfied clauses")

plt.grid(True)

plt.show()

If you try the circuit with 1,000 gates and seed equal to 8, you will notice that it 

seems to never end. This is because the circuit is not solvable, and making all the 

random choices and attempts takes a long time. In the end, the algorithm won’t 

provide you with any solution.

FIGURE 18-5: 

The number of 

unsatisfiable 

clauses decreases 

after random 

adjustments.

---

354

 

   

  PART 5