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.

翻译：本文讨论了无歧义SAT问题关于子句数量的自然范围。我们证明，对于含n个变量的精确合取范式布尔公式，存在函数f(n)和g(n)，使得当子句数量大于f(n)时公式无满足真值赋值，当子句数量大于g(n)时公式要么有唯一满足真值赋值，要么无满足真值赋值。函数f(n)与g(n)之间的区间即为无歧义SAT问题的自然范围。本文还提供了若干计数规则及一个算法，可在多项式时间内判定某些公式的不可满足性。