Uniquely Satisfiable d-Regular (k,s)-SAT Instances

Unique k-SAT is the promised version of k-SAT where the given formula has 0 or 1 solution and is proved to be as difficult as the general k-SAT. For any k ≥ 3 , s ≥ f ( k , d ) and ( s + d ) / 2 > k - 1 , a parsimonious reduction from k-CNF to d-regular (k,s)-CNF is given. Here regular (k,s)-CNF is a subclass of CNF, where each clause of the formula has exactly k distinct variables, and each variable occurs in exactly s clauses. A d-regular (k,s)-CNF formula is a regular (k,s)-CNF formula, in which the absolute value of the difference between positive and negative occurrences of every variable is at most a nonnegative integer d. We prove that for all k ≥ 3 , f ( k , d ) ≤ u ( k , d ) + 1 and f ( k , d + 1 ) ≤ u ( k , d ) . The critical function f ( k , d ) is the maximal value of s, such that every d-regular (k,s)-CNF formula is satisfiable. In this study, u ( k , d ) denotes the minimal value of s such that there exists a uniquely satisfiable d-regular (k,s)-CNF formula. We further show that for s ≥ f ( k , d ) + 1 and ( s + d ) / 2 > k - 1 , there exists a uniquely satisfiable d-regular ( k , s + 1 ) -CNF formula. Moreover, for k ≥ 7 , we have that u ( k , d ) ≤ f ( k , d ) + 1 .