Exploration of Hard to Solve 3-sat Problems

Abstract

We designed and implemented an efficient tough random symmetric 3-SAT generator and propose two deterministic algorithms that efficiently generate 3-SAT instances with a unique solution. We quantify the first algorithms hardness in terms of CPU time, numbers of restarts, decisions, propagations, conflicts and conflicted literals that occur when a solver tries to solve 3-SAT instances. In this experiment, the clause variable ratio was chosen to be around the conventional critical phase transition number 4.24. The experiment shows that instances generated by our generator are significantly harder than instances generated by the Tough K-SAT generator. The two deterministic algorithms generate 3-SAT instances with the number of clauses scaling as 4n, where n is the number of variables, and (n+6), respectively. By combining these two algorithms along with a simple padding algorithm, we prove a hybrid algorithm that can generate n-variable instances with the number of clauses that scale between (n+6) and 7n(n-1)(n-2). Overall, all proposed SAT generators seek to explore unique difficult to solve SAT problems.