• Glucose

  • Referenced in 38 articles [sw07833]
  • introduced in 2009) for the clause learning mechanism of so called ”Modern” SAT sovlers ... contraction of the concept of ”glue clauses”, a particular kind of clauses that glucose detects...
  • Pueblo

  • Referenced in 29 articles [sw00743]
  • clauses in order to simultaneously learn both a CNF clause and a PB constraint with ... Several techniques for handling the original and learned PB constraints are introduced. Overall, our method...
  • HySAT

  • Referenced in 24 articles [sw01980]
  • checking context, e.g. isomorphic replication of learned conflict clauses or tailored decision strategies, and extends...
  • MathCheck

  • Referenced in 10 articles [sw13642]
  • inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems ... solver, by providing learned clauses that encode theory-specific lemmas, as it searches...
  • Caffe

  • Referenced in 56 articles [sw17850]
  • developed by the Berkeley Vision and Learning Center (BVLC) and by community contributors. Yangqing ... Caffe is released under the BSD 2-Clause license...
  • MiniMaxSat

  • Referenced in 34 articles [sw09732]
  • mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost ... main features are: learning and backjumping on hard clauses; resolution-based and subtraction-based lower...
  • Lynx

  • Referenced in 10 articles [sw13643]
  • specific code into modern conflict-driven clause-learning (CDCL) SAT solvers, thus enabling users ... search, and to respond by adding CNF clauses back to the solver dynamically and incrementally...
  • versat

  • Referenced in 9 articles [sw08417]
  • features of modern SAT solvers, including clause learning, watched literals, optimized conflict analysis, non-chronological ... data structures like mutable C arrays for clauses and other solver state, and machine integers...
  • DepQBF

  • Referenced in 31 articles [sw09734]
  • with conflict-driven clause and solution-driven cube learning. By analyzing the structure...
  • DPvis

  • Referenced in 7 articles [sw00219]
  • search tree and the effects of clause learning. DPvis is supposed to help in teaching...
  • satUZK

  • Referenced in 4 articles [sw18570]
  • description. satUZK is a conflict-driven clause learning solver for the boolean satisfiability problem ... standard DPLL [1] algorithm with clause learning the solver is able to perform various preprocessing...
  • GrADSAT

  • Referenced in 5 articles [sw07282]
  • algorithm uses intelligent backtracking, sharing of learned clauses and clause reduction. The distributed implementation allows...
  • GPy

  • Referenced in 25 articles [sw14302]
  • machine learning algorithms based on GPs. GPy is available under the BSD 3-clause license...
  • COMiniSatPS

  • Referenced in 4 articles [sw18569]
  • VSIDS, and the roles of learned clauses. We give a wide range of concrete evidence...
  • MapleSAT

  • Referenced in 2 articles [sw25918]
  • MapleSAT: A Machine Learning based SAT Solver. The Maple series of SAT solvers ... family of conflict-driven clause-learning SAT solvers outfitted with machine learning-based heuristics. Currently ... machine learning based clause learning policy. A key innovation in the MapleSAT series...
  • Scavenger

  • Referenced in 3 articles [sw23945]
  • first-order generalization of) conflict-driven clause learning...
  • SATGraf

  • Referenced in 3 articles [sw14761]
  • being processed by a conflict-driven clause-learning (CDCL) solver. The tool is parametric, allowing...
  • MapleCOMSPS

  • Referenced in 2 articles [sw31642]
  • family of conflict-driven clause-learning SAT solvers outfitted with machine learning-based heuristics. MapleCOMSPS...
  • ENIGMA

  • Referenced in 4 articles [sw28655]
  • Machine. ENIGMA is a learning-based method for guiding given clause selection in saturation-based ... clause as useful or un-useful for the proof search. This learned classification is used...
  • MapleCOMSPS_LRB

  • Referenced in 1 article [sw31643]
  • family of conflict-driven clause-learning SAT solvers outfitted with machine learning-based heuristics...