Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Note On The Natural Range Of Unambiguous-SAT

Tayfun Pay

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.

A Note On The Natural Range Of Unambiguous-SAT

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.
Paper Structure (8 sections, 6 theorems, 2 algorithms)

This paper contains 8 sections, 6 theorems, 2 algorithms.

Table of Contents

  1. Introduction
  2. Defining Precise Conjunctive Normal Form
  3. Finding the natural range of ${Unambiguous-SAT}$
  4. Solving PCNF formulas in the natural range of ${Unambiguous-SAT}$
  5. Functions that count literals and variables to determine unsatisfiability
  6. Algorithm that counts related clauses to determine unsatisfiability
  7. Conclusion
  8. Appendix

Key Result

theorem 1

A Boolean formula in Precise Conjunctive Normal Form can have up to $m(n) = \sum_{i=1}^{n} 2^{i} \binom{n} {i}$ different clauses, where $n$ is the number of variables.

Theorems & Definitions (15)

  • definition 1
  • definition 2
  • theorem 1
  • proof
  • theorem 2
  • proof
  • theorem 3
  • proof
  • definition 3
  • corollary 1
  • ...and 5 more