ManySat: solver description
- Youssef Hamadi ,
- Said Jabbour ,
- Lakhdar Sais
MSR-TR-2008-83 |
ManySat is a DPLL-engine which includes all the classical features like two watched-literal, unit propagation, activity-based decision heuristics, lemma deletion strategies, and clause learning. In addition to the classical first-UIP scheme, it incorporates a new technique which extends the classical implication graph used during conflict-analysis to exploit the satisfied clauses of a formula [1]