node counts

[gsgs2]

is there a way to get the nodecounts for a clasp-run instead of the seconds needed ? just how often the most inner loop was executed

ithat would be more useful for benchmarks, since seconds depend on external things like operation system processor heat programs running on other threads

[BenKaufmann]

I'm not familiar with the term node count and there are no dedicated loop counters in clasp. However, from what I understand, the number of choices (or alternatively conflicts) might come close to what you want. For this, you have to call clasp with option --stats.

Please note though that these numbers are only deterministic with one solving thread. Multi-threaded solving in clasp (option --parallel-mode,-t) is inherently non-deterministic.

[gsgs2]

yes,thanks, --stats works. I was only searching --help=3 for keyword "node" I'll take the maximum value, which is "Choices"

I didn't notice that clasp -t is non-deterministic I use ./clasp4 file which calls clasp kk -t 4 on multiple instances in file and just measures the total time needed for all instances. This gave strange time increases today vs. yesterday whose reason I'm trying to figure out.

I'm currently only considering exact-cover problems.

output of clasp 3.3.5 --stat :

c Models : 1+ c Calls : 1 c Time : 0.138s (Solving: 0.14s 1st Model: 0.14s Unsat: 0.00s) c CPU Time : 0.138s c c Choices : 20196 c Conflicts : 18230 (Analyzed: 18230) c Restarts : 1 (Average: 18230.00 Last: 2222) c Model-Level : 4.0 c Problems : 1 (Average Length: 0.00 Splits: 0) c Lemmas : 18230 (Deleted: 16338) c Binary : 17 (Ratio: 0.09%) c Ternary : 317 (Ratio: 1.74%) c Conflict : 18230 (Average Length: 19.7 Ratio: 100.00%) c Loop : 0 (Average Length: 0.0 Ratio: 0.00%) c Other : 0 (Average Length: 0.0 Ratio: 0.00%) c Backjumps : 18230 (Average: 1.11 Max: 29 Sum: 20183) c Executed : 18230 (Average: 1.11 Max: 29 Sum: 20183 Ratio: 100.00%) c Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio:
0.00%) c c Variables : 300 (Eliminated: 0 Frozen: 0) c Constraints : 2216 (Binary: 89.2% Ternary: 0.0% Other:
10.8%)

==========================================================

output of Kissat 3.1.0

c conflicts: 12434 72682.00 per second c decisions: 46198 3.72 per conflict c eliminated: 19 6 %
variables c propagations: 1384073 8090493 per second c queue_decisions: 39140 85 %
decision c random_decisions: 2266 5 %
decision c random_sequences: 14 888
interval c reductions: 7 1776
interval c rephased: 4 3108
interval c restarts: 1768 7.03 interval c score_decisions: 4792 10 %
decision c strengthened: 90 3 % checks c subsumed: 10 0 % checks c switched: 7 1776
interval c vivified: 1400 21 % checks c vivify_checks: 6525 1631 per vivify c vivify_units: 0 0 %
variables c walk_improved: 1 100 % walks c walks: 1 12434
interval c c ---- [ resources ]

c c maximum-resident-set-size: 4915200 bytes 5 MB c process-time: 0.17 seconds

================================== output of Donald Knuth's "dancing links , dlx1.w" : 1 solution, 198026+1124421278 mems, 41732507 updates, 31952 bytes, 1976196 nodes.

Am 15.07.2024 10:15 schrieb Benjamin Kaufmann:

I'm not familiar with the term node count and there are no dedicated loop counters in clasp. However, from what I understand, the number of choices (or alternatively conflicts) might come close to what you want. For this, you have to call clasp with option --stats.

Please note though that these numbers are only deterministic with one solving thread. Multi-threaded solving in clasp (option --parallel-mode,-t) is inherently non-deterministic.

-- Reply to this email directly, view it on GitHub [1], or unsubscribe [2]. You are receiving this because you authored the thread.Message ID: @.***>

Links:

[1] https://github.com/potassco/clasp/issues/102#issuecomment-2227933633 [2] https://github.com/notifications/unsubscribe-auth/BCAREI7WT43MX76RDZ6NTELZMOAK3AVCNFSM6AAAAABK35AVHWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDEMRXHEZTGNRTGM