In my recent work, I have developed a new perspective on the Boolean satisfiability problem (SAT), focusing particularly on formulas in Conjunctive Normal Form (CNF). This exploration introduces a classification of SAT subproblems based on the nature of the literals within the clauses, and a novel concept called saturation as a measure of contradiction. Below, I will provide an overview of this approach and highlight its key implications for SAT complexity and algorithmic design.
1. Classification of Clauses
I categorize the clauses of a CNF formula into three distinct types:
P: Clauses containing only positive literals.
N: Clauses containing only negative literals.
M: Clauses that include at least one positive and one negative literal.
Each clause in a CNF formula fits into exactly one of these categories, leading to seven potential subproblem types in SAT:
P (only positive clauses)
N (only negative clauses)
M (mixed clauses)
M ∧ N
M ∧ P
P ∧ N
M ∧ P ∧ N (the most general case)
2. Triviality of Subproblems
One of the significant findings is that the subproblems P, N, M ( it is clear if you put the formula in an algebric/logic form), M AND N, M AND P, P AND N(this case is satisfiable only if there is no direct contraddiction, s.a. Xi and notXi, due to the Saturation concept) are trivially satisfiable. For example:
In subproblem P, assigning all variables the value 1 satisfies every clause.
Similarly, for N, assigning 0 satisfies every clause.
M is also trivial, since any assignment of 0 or 1 satisfies its mixed structure.
M AND N assigning all variables the value 0 satisfies every clause.
M AND P assigning all variables the value 1 satisfies every clause.
This triviality offers insights into simpler SAT instances, but the combination of these subproblems (especially M ∧ P ∧ N) becomes much more challenging.
3. The Concept of Saturation
In this work, I introduce the idea of saturation, which is essentially a condition of over-determination in SAT. A formula is said to be "saturated" when it includes all possible variations (complementary forms) of a clause. This concept leads to a useful theorem:
If a formula contains all clauses from the complement set of any of its clauses, the formula is unsatisfiable.
This result stems from the fact that if every possible assignment is blocked by at least one clause, there is no way to satisfy the entire formula. Saturation thus provides a direct way to detect unsatisfiability in some cases.
4. A Global Saturation Conjecture
One of the open questions in this research is whether there exists a critical saturation threshold beyond which a formula becomes unsatisfiable. I propose the following conjecture:
There exists a critical saturation degree
𝛿
𝑐
δ
c
such that, if a formula has a saturation degree
𝛿
>
𝛿
𝑐
δ>δ
c
, it becomes unsatisfiable.
Understanding and quantifying this threshold could lead to new tools for analyzing the complexity of SAT instances and potentially developing more efficient algorithms for detecting unsatisfiability.
Right now I'm exploring another way using generating function , to count instances of the varaibles that satisfies the formula.
I'll be vary grateful if you could verify or help me to finish this study :)
