An implementation of the Davis-Putnam procedure using network structures
Hsin-Tai Yang, Chih‐Hung Wu, Shie-Jue Lee · 2002
The satisfiability (SAT) problem is an important topic in many AI applications, such as theorem proving, decision making, etc. One of the widely adopted approach for SAT problems is the Davis-Putnam procedure (1960). In this paper, we propose an implementation of the Davis-Putnam procedure based on the RETE-like network. By this way, we can gain much efficiency in both CPU time and memory usage.