SATLab: X-raying random k-SAT (Tool presentation)

Abstract

In the random k-SAT model, probabilistic calculations are often limited to the first and second moments, thus giving an idea of the average behavior, whereas what happens with high probability can significantly differ from this average behavior. In these conditions, we believe that the handiest way to understand what really happens in random k-SAT is experimenting. Experimental evidence may then give some hints hopefully leading to fruitful calculations. Also, when you design a solver, you may want to test it on real instances before you possibly prove some of its nice properties. However doing experiments can also be tedious, because you must generate random instances, then measure the properties you want to test and eventually you would even like to make your results accessible through a suitable graph. All this implies lots of repetitive tasks, and in order to automate them we developed a GUI-software called SATLab. © 2012 Springer-Verlag.