| 摘要 |
Computer implemented method to indicate whether a CNF sentence representing a physical system is satisfiable. The method includes structuring a search tree based upon received data representing the CNF sentence. The search tree includes a root node and a plurality of other nodes. The method includes causing the computer to use a search to visit nodes using a decision heuristic at each node to determine which of the branches of the search tree to explore from that node, determining which nodes lie on the solution path, modifying the decision heuristic according to the analysis, generating a trained decision heuristic, and using the trained decision heuristic to process CNF sentences to determine whether those CNF sentences are satisfiable. A shortest path through the search tree provides a solution path and the heuristic can be trained with a set of training instances.
|
