Partition-based decision heuristics for SAT and image computation using SAT and BDDs
AssigneeNEC USA, Inc.
InventorsAarti Gupta, Zijiang Yang, Pranav Ashar, Sharad Malik
Life of this patent
Estimating the term…
Abstract
A method for Boolean Satisfiability (SAT). The method comprises using a variable decision heuristic in a SAT algorithm and pruning the search space of SAT using said decision heuristic. The decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and the partitioning is induced by a separator set. An image computaion method that uses the disclosed method for solving the SAT.
Claims27
1) A method for Boolean Satisfiability (SAT), said method comprising:
- a) using a variable decision heuristic in a SAT algorithm;
- and
- b) pruning the search space of SAT using said decision heuristic, wherein said decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and said partitioning is induced by a separator set.
2) A method of image computation, wherein said image computation uses Boolean Satisfiability (SAT) and binary decision diagrams (BDD), said SAT is performed by a process comprising:
- a) using a variable decision heuristic in a SAT algorithm;
- and
- b) pruning the search space of SAT using said decision heuristic, wherein said decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and said partitioning is induced by a separator set.
12) The method of column 11, wherein said rule comprises giving preference to columns with a most number of entries in an inactive region.
Dependencies are inferred from the claim text.