MapleSAT

SAT solvers heavily rely on a handful of heuristics for their surprising effectiveness in solving large practical instances. We propose to design heuristics with the goal of minimizing running time, or another metric as proxy for running time, by using machine learning to leverage the bountiful of data generated by SAT solvers.

The Maple series of SAT solvers is a family of  conflict-driven clause-learning SAT solvers outfitted with machine learning-based heuristics. The key innovation of these solvers is the use of the learning rate branching heuristic (LRB), a departure from the VSIDS branching heuristic that has been the status quo for the past decade of SAT solving. Note that the experiments in our SAT 2016 paper describing LRB use only pure branching heuristics. That is, the VSIDS experiment uses only VSIDS and the LRB experiments uses only LRB. The hybrid LRB-VSIDS branching heuristic in MapleCOMSPS and MapleGlucose is only for the SAT competition and not part of the SAT 2016 paper.



MapleCOMSPS, MapleCOMSPS_LRB, & MapleCOMSPS_CHB

  • MapleCOMSPS won 1st in the SAT Competition 2016 Main track and 2nd in the Application category
  • MapleCOMSPS_LRB won 1st in the SAT Competition 2016 Application category
  • Based off of COMiniSatPS (a.k.a COMSPS)
  • See solver description for details
  • MapleCOMSPS and MapleCOMSPS_LRB use a LRB-VSIDS hybrid branching heuristic, see solver description above for details
  • MapleCOMSPS_CHB uses a CHB-VSIDS hybrid branching heuristic, see solver description above for details
  • Download source code (MapleCOMSPS_LRB) (MapleCOMSPS_CHB)


MapleCOMSPS_Pure_LRB & MapleCOMSPS_Pure_CHB

  • These two solvers remove VSIDS completely and replace it with either LRB or CHB, that is no "hybrid" branching heuristic
  • Note, these two solvers were not submitted to the SAT competition
  • Download source code (MapleCOMSPS_Pure_LRB) (MapleCOMSPS_Pure_CHB)



MapleGlucose



MapleCMS



MapleSAT