Practice/Real-Life Applications of Computational Algorithms, Spring 2021
0710006 KE-YU LU
make
./yasat [input_file_name]- Linux / macOS
- c++14
DIMACS
c comment
p cnf 3 4
1 2 3 0
1 -2 -3 0
-1 2 -3 0
-1 -2 3 0
Output the satisfiablity and a solution we found!
s SATISFIABLE
v 1 2 3 0
s UNSATISFIABLE
- Store clauses in Sparse Metrix using STL vector
- Conflict-Driven Clause Learning (CDCL)
- Boolean Constraint Propagation (BCP)
- 2-Literal Watching
- Non-Chronological Backtracking
- First Unique Implication Point (1UIP)
- Branching Heuristics
- Jeroslaw-Wang Score
- Dynamic Heuristic: Give higher priority to the new clauses.
- Data Structure: STL set
- Luby Restart
| Benchmark | Time (s) |
|---|---|
| aim-100-1_6-no-1.cnf | 0.012 |
| aim-100-1_6-yes1-1.cnf | 0.015 |
| aim-200-1_6-no-1.cnf | 0.012 |
| aim-200-1_6-yes1-1.cnf | 0.013 |
| aim-50-1_6-no-1.cnf | 0.009 |
| aim-50-1_6-yes1-1.cnf | 0.009 |
| dubois100.cnf | 0.023 |
| dubois20.cnf | 0.011 |
| ii16a1.cnf | |
| ii32a1.cnf | 0.272 |
| ii8a1.cnf | 0.010 |
| jnh1.cnf | 0.015 |
| jnh10.cnf | 0.015 |
| jnh11.cnf | 0.016 |
| par16-1-c.cnf | 5.176 |
| par16-1.cnf | 0.033 |
| par32-1-c.cnf | |
| par32-1.cnf | 0.055 |
| par8-1-c.cnf | 0.010 |
| par8-1.cnf | 0.014 |