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]