Programs I made during the course CS-591: SAT and SMT solvers by Dr. Ashutosh Gupta from IIT Bombay.
Z3 library by Microsoft Research is used.
Peaks are observed when a problem transforms from satisfiable to unsatisfiable. The exact value where such transformations occur are still not proved and is a Hot area of research.
The follwing plots are made for Graph Coloring problem. Number of colors is 3 for both plots.
X-axis - Number of edges
Y-axis - Time required to find the satisfiabilty of the problem
50-nodes nd 800(max)-edges - Transition occurs around 340 edges.
500-nodes nd 5000(max)-edges - Transition occurs around 1150 edges.
