Satisfiability filter and query tool and method of building a satisfiability filter and query tool

摘要

A SAT filter builder and method for building a SAT filter is provided. Hash functions are utilized to map elements of a domain subset to a set of literals which are in turn used to create a set of equations. These equations are conjoined to provide a satisfiability instance. The satisfiability instance is provided to an equation solver and the solution is provided to an array to build the filter. A query tool is also provided which allows the filter built by the SAT filter to test an element for set membership. The query tool utilizes the same hash functions used by the SAT filter builder to map the element to be tested to a set of literals. These literals are used to create an equation. The solution identified by the SAT builder tool is then provided to the equation created by the query tool and set membership is determined by determining whether the equation provided by the query tool is satisfied by the solution provided by the SAT filter builder.