SAT Solving by Multiplication in and Addition out of Clauses

Abstract

In this article, we use the PBNF-transform, or Polynomial Boolean Normal Form, described in the two earlier articles and now extended to higher arity, to solve Boolean satisfiability problems (SAT), which are part of the P versus NP problem. SAT consists of a conjunction of clauses, and in our SAT-solving models, we dualize the logical equations by inverting the problem: we multiply letters (literals) in the transferred clauses and use a binary iterated composition based on adding polynomials for the conjunctions in our solution formula. We obtain Polynomial Boolean Equations, PBE=0, by also renaming the truth value T=0. With reversed literal repetition, we get the CNF as the sum of the transformed clauses. In fact, we can always reduce to multiplication in and addition out of clauses, as we do not look for the entire kernel of PBE for a YES instance for SAT.