This repository contains an implementation of the DPLL (Davis–Putnam–Logemann–Loveland) algorithm designed to decide the satisfiability of CNF formulae.
It is also optimized with several heuristics (2-Clause, Jeroslow-Wang, Dynamic Largest Individual Sum) which allow it to make decisions faster on large formula inputs.
To test the performance of the DPLL solver using each of three heuristics, it is evaluated on random formulas generated on the fixed-clause-length model. For a given N (number of variables) and L (number of clauses), a 3-CNF formula is generated by randomly choosing a set of three distinct literals from the set of N variables and negating each one with probability 0.5. The dependence of the performance of the solver on the ratio L/N for a fixed N is investigated.
For the report, the experiments were run for N = 100 and N = 130. The L/N ratio is varied from 3.0 to 6.0 in increments of 0.2, and 100 formulas are tested for each ratio value. The 3-CNF formulas are generated in DIMACS format, detailed here.
The code for generating random 3-CNFs is in cnfgenerator.py. For a given N and a directory string (e.g. “n100_cnf_formulas”), the code creates 16 folders (= number of 0.2-increments between 3.0 and 6.0 including both), each named the <directory name> appended with the ratio value (“3.2”, “4.4”, etc.) and populates each folder with 100 ‘.cnf’ files, each containing a 3-CNF formula of that L/N ratio.
The code for the DPLL solver is in dpllrunner.py, which goes through some of these folders (given the N value), runs the algorithm on all 100 of the test formulas for each ratio increment from 3.0 to 6.0, and dumps the results into a .json file. The results file will be named as <heuristic><N value>.json.
The results dumped in the .json files is structured as a large dictionary of dictionaries. For the ‘outer’ dictionary, the keys are the ratio increment values, i.e., ‘3.0’, ‘3.2’, and so on till ‘6.0’. These keys are mapped to an ‘inner’ dictionary containing the results of the 100 test formulas of that ratio. This inner dictionary has the formula number as the key, i.e., ‘0’, ‘1’, and so on up till ‘99’. These keys are mapped to a value which is a tuple. This tuple consists of a string, “SAT” or “UNSAT”, and an integer value denoting the steps (DPLL calls) it took to reach the satisfiability result.
Example: {"3.0": {"0": ["UNSAT", 1], "1": ["UNSAT", 1] ...
At L/N ratio = 3.0, the first random 3-CNF was unsatisfiable, decided in 1 step, the second had the same result, etc.
For all files, simply replace the filenames in the script with the .json result of the heuristic/N value that you want to analyze.
satprob_plotter.py: Probability of a formula being satisfiable ("SAT") as a function of L/N ratio.stepstoratio_plotter.py: Average number of steps taken to decide satisfiability ("SAT"/"UNSAT") as a function of L/N ratio.compare_plotter.py: Comparison of steps taken to decide staisfiability between two heuristics as a function of L/N ratio.