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 [Formula: see text] , [Formula: see text] and [Formula: see text] , 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 [Formula: see text] , [Formula: see text] and [Formula: see text]. The critical function [Formula: see text] is the maximal value of s, such that every d-regular (k,s)-CNF formula is satisfiable. In this study, [Formula: see text] denotes the minimal value of s such that there exists a uniquely satisfiable d-regular (k,s)-CNF formula. We further show that for [Formula: see text] and [Formula: see text] , there exists a uniquely satisfiable d-regular [Formula: see text]-CNF formula. Moreover, for [Formula: see text] , we have that [Formula: see text].