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.

主权项

1. A computer system comprising:
a bijective set memory for storing data representing bidirectional relationships, wherein the bijective set memory comprises:
an element memory for storing data representing elements; anda class memory for storing data representing classes; a parallel information processor comprising means for reading input to the computer system and means for performing set operations on the input to produce output representing results of the set operations; an induction module, under control of the parallel information processor, comprising means for using induction to learn relationships between the elements and the classes and for storing data representing the learned relationships in the bijective set memory; a deduction module, under control of the parallel information processor, for receiving data representing input perceptions and for using deduction to retrieve, from the bijective set memory, data representing conceptions having relationships to the input perceptions; a reduction module, under control of the parallel information processor, for receiving data representing input conceptions and for using reduction to retrieve, from the bijective set memory, data representing perceptions having relationships to the input conceptions; means for receiving data representing an input 3-SAT formula; wherein the parallel information processor further comprises means for determining whether the input 3-SAT formula is satisfiable, comprising:
means for using an inverse function to convert disjunctions of literals in the input 3-SAT formula into semantic equivalent conjunctions, thereby producing data representing a converted input 3-SAT formula;means for controlling the induction module to learn relationships among elements of the converted 3-SAT formula;means for organizing the learned relationships into a plurality of levels;means for storing data representing the learned relationships in the bijective set memory according to the plurality of levels;means for using the deduction module and the reduction module to apply a plurality of rejection rules to a knowledge domain associated with the converted input 3-SAT formula, and thereby to reject all elements of the converted input 3-SAT formula which are not satisfiable, thereby leaving a range of a remaining domain as the range of assignments;means for determining whether the range of the remaining domain includes at least one assignment;means for providing output indicating that the input 3-SAT formula is satisfiable in response to determining that the remaining domain includes at least one assignment; andmeans for providing output indicating that the input 3-SAT formula is not satisfiable in response to determining that the remaining domain does not include at least one assignment.