Boolean satisfiability (SAT) solver
AssigneeSynopsys, Inc.
InventorWilliam Clark Naylor, Jr.
Life of this patent
Estimating the term…
Abstract
Techniques and systems for solving a Boolean satisfiability (SAT) problem are described. Specifically, embodiments solve the SAT problem by generating an extended resolution proof. It is well-known that many technological problems can be modeled as SAT problems, and that solving an underlying SAT problem effectively solves the original technological problem. Therefore, embodiments described herein can be used to solve any technological problem that can be modeled as a SAT problem.
Claims20
A non-transitory computer-readable storage medium storing instructions that, when executed by a computer, cause the computer to perform a method for solving a technological problem, the method comprising:
- constructing a Boolean satisfiability (SAT) problem based on the technological problem;
- maintaining a database that stores clauses that are used while solving the SAT problem;
- solving the SAT problem by generating an extended resolution proof, wherein each new variable is defined as a Boolean OR of a pair of literals involving existing variables, and the pair of literals are chosen as a most common pair occurring in the clauses in the database;
- and
- using a solution to the SAT problem to solve the technological problem.
A non-transitory computer-readable storage medium storing instructions that, when executed by a computer, cause the computer to perform a method for solving a technological problem, the method comprising:
- constructing a Boolean satisfiability (SAT) problem based on the technological problem;
- maintaining a database that stores clauses that are used while solving the SAT problem;
- solving the SAT problem by generating an extended resolution proof, wherein new variables are defined only when a resolution method fails to generate clauses of a predefined type;
- and
- using a solution to the SAT problem to solve the technological problem.
A non-transitory computer-readable storage medium storing instructions that, when executed by a computer, cause the computer to perform a method for solving a technological problem, the method comprising:
- constructing a Boolean satisfiability (SAT) problem based on the technological problem;
- maintaining a database that stores clauses that are used while solving the SAT problem;
- solving the SAT problem by generating an extended resolution proof, wherein new variables are defined only when a resolution method fails to generate clauses of a predefined type at a rate that is greater than a threshold;
- and
- using a solution to the SAT problem to solve the technological problem.
Dependencies are inferred from the claim text.