Kenneth A Roe

US Patent:

20070074152, Mar 29, 2007

Filed:

Jun 8, 2006

Appl. No.:

11/423128

Inventors:

Kenneth Roe - Emerald Hills CA, US

International Classification:

G06F 9/44

US Classification:

717104000

Abstract:

A heuristic theorem prover incrementally simplifies theorems so that they can be more efficiently solved. According to one aspect, the invention provides innovations in preprocessing theorems according to certain heuristics before they are processed using conventional DPLL(T) algorithms. In one innovation, a unate detection algorithm is used to efficiently locate case splitting. A second innovation includes using a scoring algorithm to decide case splits. This algorithm can either be used as an alternative to DPLL(T) algorithms or it can be used to choose some initial case splits before DPLL(T) processing is started. A third innovation includes the use of rewriting before the DPLL(T) solver is called. A fourth innovation introduces two encoding algorithms. The first removes domain theory predicates when there are only a small number of some subset of variables. The second is aimed at encoding difference logic as Boolean expressions.