Program Design, General Course Design of CSE College, HUST for students enrolled in 2018.
This is one possible solution for the Binary Sudoku Design. Currently we uploaded our codes of core algorithms to Ver_3.0
Modularized basic algorithms and data structures.
In V1.0, we copy the whole simplified Clause Set every time we need to start a new branch in the search tree.
The core idea of this method is to replace the Clause Set in a search tree with an result array.
Improves Modularity and adds new functions:
1) Generate a Binary Sudoku puzzle and ensure its unique solution;
2) Convert a generated Binary Sudoku problem into SAT CNF format, Tseytin Transformation applied.
UIP means Unique Implication Point. In the Implication Graph, this point must satisfy:
1) In current decision level;
2) Stands on every path in current decision level to the conflict;
3) Closest to the conflict point among all points satisfy 1) and 2).
Searching for and using UIP help shrink the length of learnt clauses, boosting the solving process.
Minor Update -- Using two queues when analyzing the implication graph.
Special case modification.
As converted Binary Sudoku problems usually contains lots of single clauses, when judging the status of the dataset, because of the Advanced Simplification we used, it could waste lots of time on those clauses which could be deleted at first. Hence we add Definite Simplification and allow it to run for only once before the formal DPLL & CDCL process.