• Walksat

  • Referenced in 208 articles [sw04328]
  • above is then repeated until all the clauses are satisfied. WalkSAT and GSAT differ ... change which minimizes the number of unsatisfied clauses in the new assignment, or with some ... will result in the fewest previously satisfied clauses becoming unsatisfied, with some probability of picking ... number of variables in the clause of fixing a currently incorrect assignment. When picking...
  • E Theorem Prover

  • Referenced in 192 articles [sw10187]
  • specification, typically consisting of a number of first-order clauses or formulas, and a conjecture...
  • VAMPIRE

  • Referenced in 239 articles [sw02918]
  • used for this CASC. A number of efficient indexing techniques are used to implement ... major operations on sets of terms and clauses. Run-time algorithm specialisation is used ... logic syntax, clausifies it and performs a number of useful transformations before passing the result...
  • MoMM

  • Referenced in 33 articles [sw04655]
  • allowing fast interreduction of a high number of clauses, dumping and fast-loading ... real-time retrieval of matching clauses in an interactive mode. MoMM’s main task ... predicate logic. This task leads to a number of features (strength, speed, memory efficiency, dealing ... richer logic of MML into the clause-like format suitable for fast interreduction...
  • MaxSolver

  • Referenced in 20 articles [sw01990]
  • sought to satisfy the maximum number of clauses in a Boolean formula. A branch ... this paper, we propose and investigate a number of strategies for max-SAT. The first ... made effective as the number of clauses increases. The third strategy consists of a binary...
  • NiVER

  • Referenced in 18 articles [sw06958]
  • variables), 58% decrease in $K$ (Number of clauses) and 46% decrease in $L$ (Literal count...
  • GOLEM

  • Referenced in 52 articles [sw24695]
  • approach. For the induction of a single clause, it randomly selects several pairs of positive ... largest number of positive examples and is consistent with the negative examples. This clause...
  • sQueezeBF

  • Referenced in 15 articles [sw06959]
  • various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination ... produce significant reductions in the number of clauses and/or variables -- up to the point that...
  • BREAKUP

  • Referenced in 4 articles [sw02078]
  • where nc is the number of clauses and nv is the number of variables...
  • ProVerif

  • Referenced in 41 articles [sw06558]
  • representation of the protocol by Horn clauses. Its main features are: It can handle many ... equations. It can handle an unbounded number of sessions of the protocol (even in parallel...
  • ProGolem

  • Referenced in 4 articles [sw13855]
  • With Plotkin’s RLGG, clause length grows exponentially in the number of examples. By contrast ... system, the length of $ij$-determinate RLGG clauses were shown to be polynomially bounded...
  • npSolver

  • Referenced in 1 article [sw13580]
  • different encodings, based on the number of clauses. As back end of the system...
  • GrADSAT

  • Referenced in 5 articles [sw07282]
  • solving hard SAT instances using a large number of widely distributed commodity computational resources ... algorithm uses intelligent backtracking, sharing of learned clauses and clause reduction. The distributed implementation allows ... resource acquisition. We show how the large number of computational resources and communication overhead influence...
  • Aquarius

  • Referenced in 5 articles [sw26678]
  • Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover. Aquarius is a distribution ... input a theorem proving problem and a number n of active nodes, Aquarius creates ... number of variants of a general methodology for distributed deduction, called deduction by Clause-Diffusion...
  • MathCheck

  • Referenced in 10 articles [sw13642]
  • inner loop of a conflict-driven clause-learning SAT solver. SAT+CAS systems ... mathematical topic (e.g., graph and number theory, algebra, geometry, etc.) supported by the underlying ... solver, by providing learned clauses that encode theory-specific lemmas, as it searches...
  • HSF

  • Referenced in 9 articles [sw09937]
  • Software Verifier based on Horn Clauses. SF is a framework that automates verification of programs ... following the CEGAR paradigm. There are a number of successful tools including SLAM, Blast, ARMC...
  • MapleAmpharos

  • Referenced in 1 article [sw25920]
  • worker conflict-driven clause-learning solvers to the number of times they are branched...
  • SeqLog

  • Referenced in 13 articles [sw01946]
  • knowledge can be specified using Datalog style clauses and sequential queries or patterns correspond ... realize this. Finally, we report on a number of experiments in the domains of user...
  • PaQuBE

  • Referenced in 5 articles [sw06998]
  • split the problem up over an arbitrary number of distributed processes. Furthermore, PaQuBE’s progressive ... which solution cubes as well as conflict clauses can be shared. According to the last...
  • BliStrTune

  • Referenced in 5 articles [sw18721]
  • ATPs) such as E allow a large number of user-specified proof search strategies described ... invent new strategies based also on new clause weight functions targeted at problems from large...