Closed T0nyX1ang closed 7 months ago
According to the tests on Yin-yang puzzle (of the edge test case), the former method can achieve a much better performance. [Former]
Models : 0
Calls : 1
Time : 36.029s (Solving: 36.01s 1st Model: 0.00s Unsat: 36.01s)
CPU Time : 35.984s
Choices : 1069923
Conflicts : 835664 (Analyzed: 835663)
Restarts : 2045 (Average: 408.64 Last: 22398)
Problems : 1 (Average Length: 1.00 Splits: 0)
Lemmas : 969747 (Deleted: 942197)
Binary : 1182 (Ratio: 0.12%)
Ternary : 1756 (Ratio: 0.18%)
Conflict : 835663 (Average Length: 39.9 Ratio: 86.17%)
Loop : 134084 (Average Length: 38.6 Ratio: 13.83%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 835663 (Average: 1.27 Max: 26 Sum: 1060207)
Executed : 835598 (Average: 1.27 Max: 26 Sum: 1060142 Ratio: 99.99%)
Bounded : 65 (Average: 1.00 Max: 1 Sum: 65 Ratio: 0.01%)
Rules : 10047
Choice : 91
Atoms : 5039
Bodies : 1265
Equivalences : 8277 (Atom=Atom: 4022 Body=Body: 18 Other: 4237)
Tight : No (SCCs: 2 Non-Hcfs: 0 Nodes: 790 Gammas: 0)
Variables : 921 (Eliminated: 0 Frozen: 921)
Constraints : 2689 (Binary: 69.9% Ternary: 20.8% Other: 9.3%)
[New]
Models : 0
Calls : 1
Time : 44.203s (Solving: 44.17s 1st Model: 0.00s Unsat: 44.17s)
CPU Time : 43.969s
Choices : 1224537
Conflicts : 937426 (Analyzed: 937425)
Restarts : 2092 (Average: 448.10 Last: 228)
Problems : 1 (Average Length: 1.00 Splits: 0)
Lemmas : 1095932 (Deleted: 1073908)
Binary : 805 (Ratio: 0.07%)
Ternary : 1046 (Ratio: 0.10%)
Conflict : 937425 (Average Length: 41.7 Ratio: 85.54%)
Loop : 158507 (Average Length: 38.8 Ratio: 14.46%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)
Backjumps : 937425 (Average: 1.29 Max: 14 Sum: 1213834)
Executed : 937363 (Average: 1.29 Max: 14 Sum: 1213772 Ratio: 99.99%)
Bounded : 62 (Average: 1.00 Max: 1 Sum: 62 Ratio: 0.01%)
Choice : 91
Atoms : 5345
Bodies : 1575
Equivalences : 9204 (Atom=Atom: 4344 Body=Body: 43 Other: 4817)
Tight : No (SCCs: 2 Non-Hcfs: 0 Nodes: 762 Gammas: 0)
Variables : 1191 (Eliminated: 0 Frozen: 1177)
Constraints : 3408 (Binary: 69.6% Ternary: 23.3% Other: 7.0%)
Current adjacent relationship are not tied to color, but it is possible to add a color specification on it. This process may reduce propagation time, as many branches are ignored during the adjacent calculation.