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

Area of Science:

• Theoretical Computer Science
• Computational Complexity
• Satisfiability Problems (SAT)

Background:

• Unique k-SAT, a variant where formulas have 0 or 1 solution, is as difficult as general k-SAT.
• Regular (k,s)-CNF formulas, with k distinct variables per clause and s occurrences per variable, are a key subclass.
• d-regular (k,s)-CNF introduces a constraint on variable occurrence differences (positive vs. negative).

Purpose of the Study:

• To establish conditions for the existence of uniquely satisfiable d-regular (k,s)-CNF formulas.
• To analyze the relationship between the maximal satisfiable density f(k,d) and minimal uniquely satisfiable density u(k,d).
• To provide a parsimonious reduction from k-CNF to d-regular (k,s)-CNF.

Main Methods:

• Development of a parsimonious reduction from general k-CNF to d-regular (k,s)-CNF.
• Mathematical analysis of the critical functions f(k,d) and u(k,d) related to satisfiability density.
• Proof of existence for uniquely satisfiable d-regular (k,s+1)-CNF formulas under specific conditions.

Main Results:

• Established bounds: f(k,d) ≤ u(k,d) + 1 and f(k,d+1) ≤ u(k,d) for k ≥ 3.
• Demonstrated that for s ≥ f(k,d) + 1 and (s+d)/2 > k-1, uniquely satisfiable d-regular (k,s+1)-CNF formulas exist.
• Showed that for k ≥ 7, u(k,d) ≤ f(k,d) + 1.

Conclusions:

• The study provides precise characterizations for uniquely satisfiable d-regular (k,s)-CNF formulas.
• The findings contribute to understanding the phase transition in satisfiability for structured CNF formulas.
• This work deepens insights into the computational complexity of SAT variants.