Problem-Sensitive Restart Heuristics for the DPLL Procedure

Lecture Notes in Computer Science - Theory and Applications of Satisfiability Testing - SAT 2009 ◽

10.1007/978-3-642-02777-2_33 ◽

2009 ◽

pp. 356-362 ◽

Cited By ~ 4

Author(s):

Carsten Sinz ◽

Markus Iser

Keyword(s):

Dpll Procedure

Download Full-text

Extending Unit Propagation Look-Ahead of DPLL Procedure

PRICAI 2004: Trends in Artificial Intelligence - Lecture Notes in Computer Science ◽

10.1007/978-3-540-28633-2_20 ◽

2004 ◽

pp. 173-182 ◽

Cited By ~ 2

Author(s):

Anbulagan

Keyword(s):

Look Ahead ◽

Unit Propagation ◽

Dpll Procedure

Download Full-text

Formal Correctness Proof for DPLL Procedure

Informatica ◽

10.15388/informatica.2010.273 ◽

2010 ◽

Vol 21 (1) ◽

pp. 57-78 ◽

Cited By ~ 5

Author(s):

Filip Marić ◽

Predrag Janičić

Keyword(s):

Correctness Proof ◽

Dpll Procedure

Download Full-text

Exploiting parallelism in the ME calculus

10.29007/v1f2 ◽

2018 ◽

Author(s):

Tianyi Liang ◽

Cesare Tinelli

Keyword(s):

Synergistic Effect ◽

Decision Procedure ◽

Experimental Results ◽

Model Evolution ◽

First Order ◽

Proof Procedure ◽

Dpll Procedure

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.

Download Full-text