A Novel, Efficient and Generalised Approach to Boolean Satisfiability
Okoh Ufuoma *
Department of Mathematics, Southern Maritime Academy, Uwheru, Delta State, Nigeria.
*Author to whom correspondence should be addressed.
Abstract
One question which has occupied mathematicians, engineers and scientists of this age is the problem of Boolean satisfiability (SAT) which asks whether a given CNF formula has at least a satisfying assignment. The goal of this work is to present a novel, efficient and general method of deciding SAT and finding all the satisfying assignments of CNF formulas. This method is powerful as it employs resolution identities in transforming clauses without a particular variable into clauses with that variable.
Keywords: SAT, satisfiable, resolution rule, resolution identity, DPLL algorithm