Parallel Execution of Stochastic Search Procedures on Reduced SAT Instances

摘要: We present a technique for checking instances of the satisfiability (SAT) problem based on combination Davis-Putnam (DP) procedure and stochastic methods. first use DP to some extent, so as partition reduce search space. If reduction does not lead an answer, algorithm is then used each subspace. This approach proven be efficient several types SAT instances. A parallel implementation method described experimental results are reported.