Why cube-and-conquer works so good for CDCL? #27
Description
| Metric | OB-SAT | march_cu | Ratio |
|---|---|---|---|
| Cubes | 412–741 | 1894–3967 | 5× fewer |
| Avg cube size | ~762 literals | ~13 literals | 59× larger |
| Decisions / cube | ~1347 | ~167 | 8× harder |
| Conflicts / cube | ~808 | ~124 | 6.5× more |
| Cubing time | 5–13 s | 1–2 s | 5× slower |
Total CDCL work:
OB-SAT = 1,445,559 vs march_cu = 893,115
OB-SAT does 1.62× MORE total CDCL work!