• 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, Pseudo-Boolean, 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 minimally-unsatisfiable 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 k-sat 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]
  • linear-time algorithm for showing the unsatisfiability of ground Horn clauses. The method (called Hornlog...
  • R-SATCHMO

  • 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...