ioanaobreja Goto Github PK

dpll1

Implementation of the DPLL algorithm, using a list of lists for the formula and making a copy of it before splitting.

dpll2

Implementation of the DPLL algorithm . The clauses and literals have flags that are initially 0. The value changes to the level of the decision when marked as sat/true (or (-1)*level for literals that are marked as false). The literal to be branched on can be chosen in two ways, either by finding the first or the most popular one.

mapster

random_cnf

Generator of CNF formulas in DIMACS format for benchmarks.

sat-solver_cdcl

A CDCL SAT Solver in C++ with pure literal and random restarts. It has a few heuristics implemented: MOMS, Jeroslow Wang, VSIDS.