Research in Unique Satisfiability

Work on analyzing at what ratio of variables to clauses do the most uniquely satisfiable formulas occur.


This report is a study on the effects of clause to variable ratio when checking for the number of USAT cases in a large number of tests. In the paper ”Hard and Easy Distributions of SAT Problems” by D. Mitchell, B. Selman, and H. Levesque (1992), examines the difficulty of SAT when the ratio of the number of clauses to the number of variables was changed. The paper shows a clear peak in the difficulty of SAT cases with around 4.25 clauses to the number of variables. This report is going to look for a clear ratio of clauses to variables, this will be found when the peak number of USAT cases appear in test groups of 100,000.