  We discuss the natural range of the Unambiguous-SAT problem with respect to
the number of clauses. We prove that for a given Boolean formula in precise
conjunctive normal form with n variables, there exist functions f(n) and g(n)
such that if the number of clauses is greater than f(n) then the formula does
not have a satisfying truth assignment and if the number of clauses is greater
than g(n) then the formula either has a unique satisfying truth assignment or
no satisfying truth assignment. The interval between functions f(n) and g(n) is
the natural range of the Unambiguous-SAT problem. We also provide several
counting rules and an algorithm that determine the unsatisfiability of some
formulas in polynomial time.

Computational Complexity