How to generate weakly nondecisive SAT instances

In this paper we solve a problem which was unsolved until now. The problem is: How to generate weakly nondecisive SAT instances? As a solution we introduce a very simple algorithm, called WnDGen, which generates weakly nondecisive clause sets. Its input is a clause and a number, its output is a clause set. WnDGen(C, k) works as follows: It generates all k-length subsets of C. For each subset it adds k clauses to the output, negating every time another literal in the subset. Then it does the same with the negation of C. We show that the resulting clause set is always weakly nondecisive and satisfiable. Actually, G and negation of G are solutions of the SAT instance generated by WnDGen(C, k). We also show that there is a threshold: Let n be the length of C; let S be the union of WnDGen(C, k) and the set of C and negation of C; if n ≥ 2k - 3, then S is unsatisfiable, if n <; 2k - 3, the S is satisfiable. We show that around this threshold there are SAT instances, which are difficult for state-of-the-art SAT solvers, i.e., they are good for testing SAT solvers.