METHOD FOR DECIDING BOOLEAN SATISFIABILITY AND IMAGE COMPUTATION METHOD USING BOOLEAN SATISFIABILITY AND BINARY DECISION DIAGRAM

摘要

PROBLEM TO BE SOLVED: To improve performance in the various examples applied with Boolean satisfiability(SAT). SOLUTION: This method for Boolean satisfiability(SAT) comprises a step for using variable decision heuristic in a SAT algorithm and a step for pruning the search space of the Boolean satisfiability(SAT) by using the decision heuristic. The decision heuristic is based on the partitioning of a conjunctive normal form(CNF) of a Boolean formula corresponding to the Boolean satisfiability(SAT), and the portioning is induced by a separator set. An image computation method is provided for solving the Boolean satisfiability(SAT).