2021/01/13 by Manoj Kumar, Kumar, Manoj
Computer Science · #Advanced Graph Theory Research #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Methods in Verification #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2101.05597
openalex publication_date 2021/01/13 · openalex created_date 2021/01/18 · openalex updated_date 2026/07/28
Boolean satisfiability problem has applications in various fields. An efficient algorithm to solve satisfiability problem can be used to solve many other problems efficiently. The input of satisfiability problem is a finite set of clauses. In this paper, properties of clauses have been studied. A type of clauses have been defined, called fully populated clauses, which contains each variable exactly once. A relationship between two unequal fully populated clauses has been defined, called sibling clauses. It has been found that, if one fully populated clause is false, for a truth assignment, then all it's sibling clauses will be true for the same truth assignment. Which leads to the necessary and sufficient condition for satisfiability of a boolean formula, in CNF. The necessary and sufficient condition has been used to develop a novel algorithm to solve boolean satisfiability problem in polynomial time, which implies, P equals NP. Further, some optimisations have been provided that can be integrated with the algorithm for better performance.