Inverse Function Method of Boolean Satisfiability (SAT)

摘要

A computer system uses an inverse function method to solve Boolean Satisfiability problems. The system benefits from the system disclosed in the US patent “Knowledge Acquisition and Retrieval Apparatus and Method” (U.S. Pat. No. 6,611,841). The system applies a learning function to access iterative set relations among variables, literals, words and clauses as knowledge; and applies deduction and reduction functions to retrieve relations as reasoning. The system uses knowledge learning (KL) and knowledge reasoning algorithms (KRA). The system abandons the “OR” operation of Boolean logic and processes only set relations on data. The system leverages the reversibility of deduction and reduction to determine whether 3-SAT formulas are satisfiable.