
Walksat
 Referenced in 204 articles
[sw04328]
 change which minimizes the number of unsatisfied clauses in the new assignment, or with some ... WalkSAT first picks a clause which is unsatisfied by the current assignment, then flips ... clause is generally picked at random among unsatisfied clauses. The variable is generally picked that ... fewest previously satisfied clauses becoming unsatisfied, with some probability of picking one of the variables...

Sat4j
 Referenced in 72 articles
[sw07283]
 solve SAT, MAXSAT, PseudoBoolean, Minimally Unsatisfiable Subset (MUS) problems. Being in Java, the promise...

MathSAT
 Referenced in 56 articles
[sw09449]
 incremental interface (for BMC), and computation of unsatisfiable cores and Craig interpolants (for abstraction refinement...

AMUSE
 Referenced in 24 articles
[sw11915]
 AMUSE: a minimallyunsatisfiable subformula extractor. This paper describes a new algorithm for extracting unsatisfiable ... subformulas from a given unsatisfiable CNF formula. Such unsatisfiable ”cores” can be very helpful ... modern SAT solver to identify unsatisfiable subformulas rather than search for satisfying assignments. Compared...

MUP
 Referenced in 15 articles
[sw11910]
 minimal unsatisfiability prover. After establishing the unsatisfiability of a SAT instance encoding a typical design ... practical need to identify its minimal unsatisfiable subsets, which pinpoint the reasons for the infeasibility ... computation, existing tools for the extraction of unsatisfiable subformulas do not guarantee the minimality ... practical algorithm that decides the minimal unsatisfiability of any CNF formula through BDD manipulation. This...

dReal
 Referenced in 26 articles
[sw07157]
 solution) and unsat answers (a proof of unsatisfiability...

DCTP
 Referenced in 21 articles
[sw06621]
 DCTP will attempt to prove either the unsatisfiability of the input formula or, alternatively, prove...

HAMPI
 Referenced in 19 articles
[sw09864]
 constraints, or reports that the constraints are unsatisfiable...

MUSer2
 Referenced in 12 articles
[sw13403]
 extractor. Algorithms for extraction of Minimally Unsatisfiable Subformulas (MUSes) of CNF formulas find a wide...

Skyblue
 Referenced in 9 articles
[sw07280]
 cannot be satisfied, SkyBlue leaves weaker constraints unsatisfied in order to satisfy stronger constraints (maintaining...

CRC 3
 Referenced in 9 articles
[sw09782]
 cannot be joined have often an intuitively unsatisfiable condition or seem intuitively joinable, so that...

EL2MCS
 Referenced in 6 articles
[sw28624]
 axiom pinpointing based on the analysis of unsatisfiable propositional formulas. Building on this earlier work ... relationship between minimal axiom sets and minimal unsatisfiable subformulas in the propositional domain. Experimental evaluation...

kcnfs
 Referenced in 8 articles
[sw00484]
 variable heuristic devoted essentially to prove the unsatisfiability of random ksat formulae and which...

ChainSAT
 Referenced in 7 articles
[sw09444]
 that it focuses on variables occurring in unsatisfied clauses. We show by extensive numerical investigations...

PASS
 Referenced in 7 articles
[sw21858]
 efficiency. In particular, it can identify unsatisfiable cases quickly. Our solver (named PASS) supports most...

SensorDCSP
 Referenced in 7 articles
[sw30992]
 these algorithms on both satisfiable and unsatisfiable instances of SensorDCSP. We found that random delays...

CLIN
 Referenced in 6 articles
[sw19618]
 found if the ground clause set is unsatisfiable. We describe the system architecture and major...

Hornlog
 Referenced in 6 articles
[sw21362]
 lineartime algorithm for showing the unsatisfiability of ground Horn clauses. The method (called Hornlog...

RSATCHMO
 Referenced in 3 articles
[sw06620]
 SATCHMO can be used to generate minimal unsatisfiable subsets of an unsatisfiable set of clauses...

MSUnCore
 Referenced in 3 articles
[sw09733]
 MSUnCore  Maximum Satisfiability with UNsatisfiable COREs. MSUnCore is a software system for solving (Weighted) (Partial ... MSUnCore are based on iterative identification of unsatisfiable cores...