As the goal for this solver is to produce a simplified and easy to understand, easy to change, and easy to analyze CDCL solver, there are two types of TODO's here.
First we list things to simplify or to remove.
-
Check again that all the core CDCL features are necessary.
-
Benchmark, configure and simplify preprocessors.
Second things are listed related to additional features.
-
Mapping or shrinking of external to internal variables.
-
Bounded variable addition.
There should be an ongoing process of refactoring and documenting the code and in particular remove part of the code which is not used anymore.
Friday, 30. December 2016.