
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 linearsized CNF formula that selects lexleaders (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 selfcontained ... 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 pseudoBoolean constraints into CNF formulae. PseudoBoolean 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 bitlevel simplifications a Boolean CNF formula is generated...

Sparrow2011
 Referenced in 2 articles
[sw12927]
 local search (SLS) solver for SAT formulae in CNF format...

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 3CNF...

HQSpre
 Referenced in 2 articles
[sw28634]
 circuit structure of the formula when a nonCNF solver backend 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 pseudoBoolean (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...