Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Refactor] Apply color specification in adjacent relationship #7

Closed
T0nyX1ang opened this issue Jan 25, 2024 · 1 comment
Closed

[Refactor] Apply color specification in adjacent relationship #7

T0nyX1ang opened this issue Jan 25, 2024 · 1 comment
Assignees
Labels
wontfix This will not be worked on

Comments

@T0nyX1ang
Copy link
Owner

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.

@T0nyX1ang T0nyX1ang self-assigned this Jan 25, 2024
@T0nyX1ang T0nyX1ang added the wontfix This will not be worked on label Jan 25, 2024
@T0nyX1ang
Copy link
Owner Author

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%)

@T0nyX1ang T0nyX1ang closed this as not planned Won't fix, can't repro, duplicate, stale Jan 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
wontfix This will not be worked on
Projects
None yet
Development

No branches or pull requests

1 participant