• Nitpick

  • Referenced in 63 articles [sw00622]
  • counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model ... TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order...
  • Satallax

  • Referenced in 55 articles [sw06849]
  • SAT solver MiniSat is responsible for much of the search for a proof. Satallax generates...
  • CPSparrow

  • Referenced in 1 article [sw40132]
  • Predefined Solution. It is crucial to generate crafted SAT formulas with predefined solutions ... generating algorithms have been proposed to generate SAT formulas with predefined solutions, community structures ... considered. We propose a 3-SAT formula generating algorithm that not only guarantees the existence ... leading SLS solver), on the generated SAT formulas under different groups of parameter settings. Through...
  • gluHack

  • Referenced in 1 article [sw40133]
  • Predefined Solution. It is crucial to generate crafted SAT formulas with predefined solutions ... generating algorithms have been proposed to generate SAT formulas with predefined solutions, community structures ... considered. We propose a 3-SAT formula generating algorithm that not only guarantees the existence ... leading SLS solver), on the generated SAT formulas under different groups of parameter settings. Through...
  • iSat

  • Referenced in 4 articles [sw14762]
  • interactive shell to control propositional SAT solvers and generate graph representations of the internal structure ... enable simple integration of both new SAT solvers and new visualization graphs and statistics with...
  • PASSAT

  • Referenced in 3 articles [sw10074]
  • PASSAT: Effcient SAT-based test pattern generation for industrial circuits. Automatic test pattern generation (ATPG...
  • SatEx

  • Referenced in 15 articles [sw01588]
  • SatEx is a web site devoted to SAT experimentation. It is not only a front ... detailed explorations of experimentation results. Being dynamically generated and constantly updated and improved, this site ... almost always up-to-date SAT experimentation paper. To the current time, SatEx presents...
  • SMCHR

  • Referenced in 2 articles [sw09322]
  • with a modern Boolean satisfiability (SAT) solver for quantifier-free formulae with an arbitrary propositional ... SMCHR is based on lazy clause generation, where ... clause for the SAT solver is generated whenever a rule is applied. We shall also...
  • PeRIPLO

  • Referenced in 7 articles [sw07896]
  • interpolating SAT-solver that implements a set of techniques to generate and manipulate interpolants...
  • ASPTools

  • Referenced in 3 articles [sw33089]
  • ground logic program (module); rsat: generate a random 3-SAT instance as a logic program...
  • SONOLAR

  • Referenced in 2 articles [sw26291]
  • Boolean formula and lets a SAT solver decide the satisfiability. For handling the extensional theory ... Boolean CNF formula is generated and fed to a SAT solver. MiniSat 2.2.0 and Glucose ... SAT solvers [4, 1]. SONOLAR is currently used for automatic test data generation...
  • CryptLogVer

  • Referenced in 3 articles [sw13253]
  • contest finalists through SAT-based attacks: Toolkit CryptLogVer for generating the conjunctive normal form...
  • OKlibrary

  • Referenced in 2 articles [sw28616]
  • OKlibrary: A generative research platform for (generalised) SAT solving. The OKlibrary is introduced, an active...
  • LPG

  • Referenced in 12 articles [sw20690]
  • durations. The system can solve both plan generation and plan adaptation problems. The basic search ... Walksat, an efficient procedure to solve SAT-problems. The search space of LPG consists...
  • Alcoa

  • Referenced in 28 articles [sw09481]
  • diagrams, checking for consistency of multiplicities and generating sample snapshots. At the other ... then applying state-of-the-art SAT solvers. It can analyze billions of states...
  • PaSAT

  • Referenced in 4 articles [sw41090]
  • PaSAT- parallel SAT-checking with lemma exchange: implementation and applications. We present PaSAT, a parallel ... generation and exchange; the main focus of our implementation is on speeding up SAT-checking...
  • Lynx

  • Referenced in 10 articles [sw13643]
  • enables non-expert users to specialize the SAT solver to a class of Boolean instances ... code is allowed to examine partial solutions generated by the solver during its search ... targeted fashion. While the power of incremental SAT solvers has been amply demonstrated...
  • DPvis

  • Referenced in 7 articles [sw00219]
  • Java tool to visualize the structure of SAT instances and runs of the DPLL (Davis ... interaction) graph. DPvis is also able to generate animations showing the dynamic change ... MiniSAT can be visualized -- including the generated search tree and the effects of clause learning ... insights in the structure (and hardness) of SAT instances...
  • CalCS

  • Referenced in 7 articles [sw13098]
  • solver, CalCS, uses a lazy combination of SAT and a theory solver. A key step ... complementary slackness and duality theory to generate succinct infeasibility proofs that support conflict-driven learning...
  • Wombit

  • Referenced in 2 articles [sw39885]
  • clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which...