• ManySAT

  • Referenced in 40 articles [sw00544]
  • DPLL algorithm. Additionally, each sequential algorithm shares clauses to improve the overall performance...
  • Syrup

  • Referenced in 6 articles [sw25919]
  • portfolio SAT solver has to share clauses in order to be efficient. In a distributed ... dedicated approach, it is possible to share many clauses without penalizing the solvers. Experiments conducted ... possibilities to boost parallel solvers needing to share many data...
  • ProVerif

  • Referenced in 42 articles [sw06558]
  • clauses. Its main features are: It can handle many different cryptographic primitives, including shared...
  • SArTagnan

  • Referenced in 2 articles [sw11451]
  • portfolio SAT solver with lockless physical clause sharing. Since multi{core architectures have become well ... shared memory architectures for physical clause sharing. In this paper we present the parallel ... solver SArTagnan that allows for sharing clauses between several threads logically and physically ... clauses. We show how physical clause sharing can be used to propagate one thread...
  • PMiniSAT

  • Referenced in 3 articles [sw11452]
  • work stealing using guiding paths, sharing short learnt clauses ... also features an extended learnt clause sharing heuristic, global restarts, and a series of data...
  • PaQuBE

  • Referenced in 5 articles [sw06998]
  • cubes as well as conflict clauses can be shared. According to the last QBF Evaluation...
  • GrADSAT

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

  • Referenced in 4 articles [sw11454]
  • modes, search space pruning and share of learnt clauses. An analysis of its performance...
  • gini

  • Referenced in 1 article [sw16095]
  • address related problems such as clause sharing...
  • LeoPARD

  • Referenced in 8 articles [sw13554]
  • sharing) with an ambitious multi-agent blackboard architecture (supporting prover parallelism at the term, clause...
  • PARTHENON

  • Referenced in 8 articles [sw25434]
  • able to handle first order formulas in clause form. PARTHENON is the first general theorem ... discusses various implementations of or-parallelism on shared memory multiprocessors. An overview of the system...
  • Aquarius

  • Referenced in 5 articles [sw26678]
  • give first a brief outline of the Clause-Diffusion methodology, with emphasis on the problem ... avoid the backward contraction bottleneck of purely shared memory approaches to parallel deduction. Then...
  • Roo

  • Referenced in 7 articles [sw12478]
  • closure of a set of clauses under a set of inference rules. In particular ... near-linear speedup over OTTER on shared memory multiprocessors...
  • MGTP

  • Referenced in 7 articles [sw09701]
  • useless model candidates caused by irrelevant clauses, a proof simplification method to eliminate duplicated subproofs ... modal logic systems, on MGTP. These techniques share a basic idea, which...
  • PaMira

  • Referenced in 3 articles [sw41089]
  • PaMira - A parallel SAT solver with knowledge sharing. In this paper we describe PaMira ... PaMira also employs the exchange of conflict clauses between the processes to guide the search...
  • Nuprl-Light

  • Referenced in 1 article [sw31982]
  • that addresses the issues of diversity and sharing by providing a modular, object-oriented framework ... theorem prover, Nuprl-Light uses generalized Horn clauses for logical specification. Indeed, specifications in Nuprl...
  • Coq

  • Referenced in 1880 articles [sw00161]
  • Coq is a formal proof management system. It...
  • c-sat

  • Referenced in 8 articles [sw00168]
  • Parallelizing modern SAT solvers for clusters such as...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • PSPLIB

  • Referenced in 269 articles [sw00740]
  • PSPLIB -- a project scheduling problem library. We present...