• AMUSE

  • Referenced in 24 articles [sw11915]
  • unsatisfiable subformulas from a given unsatisfiable CNF formula. Such unsatisfiable ”cores” can be very helpful...
  • Sugar

  • Referenced in 24 articles [sw09758]
  • encoded to a Boolean CNF formula, and it is solved by an external SAT solver...
  • MUP

  • Referenced in 15 articles [sw11910]
  • decides the minimal unsatisfiability of any CNF formula through BDD manipulation. This algorithm ... only in the treewidth of the CNF formula. We provide an empirical evaluation...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form (NNF), which relies ... quantified variables by resolution on CNF, which causes the formula size to increase quadratically ... instead of CNF combined with expansion. In Nenofex, a formula in NNF is represented ... order to remove redundancy from the formula, limited versions of two approaches from the domain...
  • MUSer2

  • Referenced in 12 articles [sw13403]
  • Minimally Unsatisfiable Subformulas (MUSes) of CNF formulas find a wide range of practical applications, including...
  • SBSAT

  • Referenced in 10 articles [sw00828]
  • range of propositional inputs, including CNF formulas, but particularly sets of arbitrary boolean constraints, represented...
  • Shatter

  • Referenced in 6 articles [sw21225]
  • without affecting the satisfiability of the CNF formula. For symmetry breaking to be effective ... Specifically, we give a linear-sized CNF formula that selects lex-leaders (among others...
  • BREAKUP

  • Referenced in 4 articles [sw02078]
  • preprocessing algorithm for satisfiability testing of CNF formulas An algorithm called BREAKUP, which processes ... CNF formulas by separating them into “connected components”, is introduced. BREAKUP is then used...
  • SAT Solver Verification

  • Referenced in 5 articles [sw28831]
  • lemmas about propositional logic and CNF formulae are proved. This theory is self-contained ... used for further exploring of properties of CNF based SAT algorithms...
  • PrecoSAT

  • Referenced in 18 articles [sw07832]
  • assignment of a propositional formula in conjunctive normal form (CNF). The Handbook of Satisfiability gives...
  • BoolVar/PB

  • Referenced in 2 articles [sw13579]
  • translating pseudo-Boolean constraints into CNF formulae. Pseudo-Boolean constraints are linear inequations with integer ... resource allocation, circuit diagnosis... The resulting CNF formula is satisfiable if and only...
  • HGen

  • Referenced in 3 articles [sw28519]
  • hGen: A Random CNF Formula Generator for Hybrid Languages...
  • SONOLAR

  • Referenced in 2 articles [sw26291]
  • simplification rules are applied to the input formula which is then converted ... performing bit-level simplifications a Boolean CNF formula is generated...
  • cnfformula

  • Referenced in 1 article [sw25690]
  • capable to generate Conjunctive Normal Form (CNF) formulas, manipulate them and, when there...
  • hgen2

  • Referenced in 1 article [sw04455]
  • Random generator hgen2 of satisfiable formulas in 3-CNF...
  • HQSpre

  • Referenced in 2 articles [sw28634]
  • circuit structure of the formula when a non-CNF solver back-end is used. Extensive...
  • Limboole

  • Referenced in 2 articles [sw28117]
  • just satisfiability for formulas in conjunctive normal form (CNF), like the DIMACS format, which...
  • Hilberticus

  • Referenced in 2 articles [sw01264]
  • transform the propositional formulas different standard forms, e.g., conjunctive normal form (CNF...
  • PBLib

  • Referenced in 6 articles [sw13578]
  • translating pseudo-Boolean (PB) constraints into CNF. We have implemented fifteen different encodings ... efficient encodings, in terms of formula size and whether unit propagation maintains generalized arc consistency...