Uniquely Satisfiable d-Regular (k,s)-SAT Instances - Zufeng Fu (Entropy, 2020)
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.