Exploiting parallelism in the ME calculus

We present some parallelization techniques for the Model Evolution (ME) calculus,an instantiation-based calculus that lifts the DPLL procedureto first-order clause logic.Specifically, we consider a restriction of ME to the EPR fragmentof clause logic for which the calculus is a decision procedure.The main operations in ME's proof procedures, namely clause instantiationand candidate literal generation, offer opportunities for MapReduce-styleparallelization.This term/clause-level parallelization is largely orthogonal to the sortof search-level parallelization performed by portfolio approaches.We describe a hybrid parallel proof procedure for the restricted calculusthat exploits parallelism at both levels to synergistic effect.The calculus and the proof procedure have been implemented ina new solver for EPR formulas.Our initial experimental results show that our term/clause-level parallelizationalone is effective in reducing runtime and can be combinedwith a portfolio-based approach to maximize performance.