DPLL Algorithm [5 points]

Short description

Write a DPLL solver which implements the basic branch and bound DPLL algorithm with unit propagation. Part of the task is also experimental evaluation of your solver on small benchmarks and a report on the results of the experiments.

Input format

Your program should be able to read two input formats

1. The simplified SMT-LIB format described in the first task.
2. The DIMACS format, also described in the first task.

Output format

• As a minimal output, the solver should write out if the formula is satisfiable (SAT) or unsatisfiable (UNSAT).
• In case of a satisfiable formula a model should be output as well. The model is printed as a set of literals
  • in case of DIMACS input format the sequence of literals should be increasing in the variable indices
  • in case of the simplified SMT-LIB format the choice of literal ordering is up to you
• Statistical information should part of the output
  • Total CPU time
  • Number of decisions
  • Number of steps of unit propagation (i.e. how many values were derived by unit propagation)

Experimental evaluation

For experimental evaluation you can use the example input files from the first task. Then you can try your solver on smaller examples from SATLIB Benchmark Problems. Select several examples from the category Uniform Random-3-SAT, measure the solving time and write a short report on how the solving time progresses with increasing complexity of the problems. Try your solver also on some non-random instances.

Extended description

The typical invocation of your program should be

   dpll [input]

Parameter input specifies the input file, the format of the input file can be either detected by the extension (.cnf for DIMACS, .sat for the simplified SMT-LIB format), or given as a special option.

• Particular choice of a decision heuristic is not important for the purpose of this exercise. You can for example take the variables in the increasing order by their indices, or you can implement a simple heuristic of your choice.
• The implementation of unit propagation is not important either, but at least it should be linear time (i.e. use at least adjacency lists). It might be interesting later how the watched literals improve the solving time.