
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 firstorder 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. Runtime 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 fastloading ... realtime 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 clauselike 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 maxSAT. 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 clausediffusion: 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 ClauseDiffusion...

MathCheck
 Referenced in 10 articles
[sw13642]
 inner loop of a conflictdriven clauselearning 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 theoryspecific 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 conflictdriven clauselearning 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 userspecified proof search strategies described ... invent new strategies based also on new clause weight functions targeted at problems from large...