A Note On The Natural Range Of Unambiguous-SAT

TL;DR

This paper explores the natural range of the Unambiguous-SAT problem based on clause count, establishing bounds for satisfiability and uniqueness, and offers polynomial-time algorithms for certain formulas.

Contribution

It defines the natural range of Unambiguous-SAT with respect to clause numbers and introduces counting rules and algorithms for satisfiability determination.

Findings

Existence of functions f(n) and g(n) bounding satisfiability and uniqueness.

Identification of the natural range between f(n) and g(n).

Polynomial-time algorithms for specific unsatisfiability cases.

Abstract

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.