On the Tractability of Un/Satisfiability

2014/08/22 by Latif Salum, Salum, Latif
Computer Science · #Computational Complexity (cs.CC) #F.1.1 #F.2.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Petri Nets in System Modeling

paper · pdf · doi:10.48550/arxiv.1408.5282

openalex publication_date 2014/08/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper shows effectiveness of X3SAT in proving P = NP. This is due to the fact that it is easy to check unsatisfiability of a particular truth assignment. A truth assignment leads to some reductions of clauses by means of "exactly-1 disjunction". The reductions result in a conjunction of literals, called the scope of the assignment. It is proved that this particular truth assignment makes the formula unsatisfiable iff the scope_s is unsatisfiable for some s, which is trivial to check. Then, each literal such that its scope is unsatisfiable is removed from the formula. Therefore, the formula is satisfiable iff the scope of every literal is satisfied.

Related

• Understanding SAT is in P
• Necessary and Sufficient Condition for Satisfiability of a Boolean Formula in CNF and its Implications on P versus NP problem
• An early sign of satisfiability
• A Linear Algebra Formulation for Boolean Satisfiability Testing
• Hiding Satisfying Assignments: Two are Better than One