Partition-based decision heuristics for SAT and image computation using SAT and BDDs
AssigneeNEC Corporation
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
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.
The method of column 10, wherein said rule comprises giving preference to columns with a most number of entries in an inactive region.
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.
Dependencies are inferred from the claim text.