Statistic Output
Closed this issue · 7 comments
What is exactly the meaning of the added statistics.
In the clasp statistic I can see that 2 Lemmas have been added, but no conflict arised.
Does this mean that the propagator added 2 lemmas ? Where can I find this information in the stats ?
I have either Edges propagated: 0 or several thousand False Edges
Could you provide some more information for people who can not get the meaning from the source code alone ?
Thanks a lot
TIME LIMIT : 1
Models : 0+
Calls : 1
Time : 250.003s (Solving: 38.98s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 249.992s
Choices : 343574
Conflicts : 0 (Analyzed: 0)
Restarts : 0
Problems : 1 (Average Length: 1.00 Splits: 0)
Lemmas : 2 (Deleted: 0)
Binary : 0 (Ratio: 0.00%)
Ternary : 0 (Ratio: 0.00%)
Conflict : 0 (Average Length: 0.0 Ratio: 0.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 2 (Average Length: 1.0 Ratio: 100.00%)
Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0)
Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%)
Rules : 49036676 (Original: 49029858)
Choice : 125304
Minimize : 1
Atoms : 29930766 (Original: 29929639 Auxiliary: 1127)
Bodies : 36040122 (Original: 36038441)
Count : 96 (Original: 1389)
Equivalences : 43545575 (Atom=Atom: 13239556 Body=Body: 14400077 Other: 15905942)
Tight : Yes
Variables : 1398353 (Eliminated: 0 Frozen: 1217675)
Constraints : 6856999 (Binary: 75.8% Ternary: 12.1% Other: 12.1%)
DifferenceLogic
Time init(s): 4.07736
[Thread 0]
Propagation(s): 4.88383
Dijkstra(s): 0
Undo(s) : 0.0401046
True edges: 0
False edges: 0
False edges (inverse): 0
False edges (partial): 10263
False edges (partial+): 16531
Edges added: 262202
Edges skipped: 185495
Edges propagated: 0
Cost consistency: 6.58817e+06
Cost forward: 0
Cost backward: 0
I do not know how exactly lemmas are counted. This is part of clasp.
Counters for consistency check
- Cost consistency (loop iterations for consistency checks)
- Edges added
- Edges skipped (edges skipped because they cannot cause a negative cycle; for such edges neither partial nor partial+ propagation is performed)
Counters for full propagation:
- Edges propagated
- True edges (kind of a misnomer / this are don't care edges encountered by propagation)
- False edges (edges made false by propagation)
- Cost forward, Cost backward (loop iterations for propagation)
Counters for partial+ propagation
- False edges (partial+) (like False edges for full propagation)
Counters for partial propagation
- False edges (partial) (like False edges for full propagation)
Counters for inverse propagation
- False edges (inverse) (like False edges for full propagation)
Thanks a lot for the explanation.
So I can summarize that there are ~26000 Propagations, aka 26000 nogoods added by the propagator.
None of them seem to be conflicting (as they have been added by partial/partial+).
Can you guarantee that these literals are actually implied on the current decision level ?
Or would it be more likely that they can be derived on an earlier decision level, forcing clasp to undo the trail ?
So I can summarize that there are ~26000 Propagations, aka 26000 nogoods added by the propagator.
Yes, but keep in mind that the consistency check does only adds nogoods in the conflicting case. Nogoods have been added for the false edges (10263+16531). There is no counter for how often the consistency check detected a conflict.
None of them seem to be conflicting (as they have been added by partial/partial+).
Looks like.
Can you guarantee that these literals are actually implied on the current decision level ?
I guess you mean that the reason for the propagated literal contains at least one literal from the current decision level. The answer is no. Only full propagation guarantees this.
Or would it be more likely that they can be derived on an earlier decision level, forcing clasp to undo the trail ?
Yes, this can happen.
I don't quite understand how this can happen. As you do partial propagation on every decision level where at least one difference logic constraint is decided your reason should always contain at least one of those new literals. Otherwise partial propagation would have detected this propagation before, right ?
So at least the reason that you provide should contain one literal of the current decision level. (Of course this literal could be removed by resolution if it triggers a conflict, but as we do not seem to have conflicts this should also not be the case)
I don't quite understand how this can happen. As you do partial propagation on every decision level where at least one difference logic constraint is decided your reason should always contain at least one of those new literals. Otherwise partial propagation would have detected this propagation before, right ?
So at least the reason that you provide should contain one literal of the current decision level. (Of course this literal could be removed by resolution if it triggers a conflict, but as we do not seem to have conflicts this should also not be the case)
Yes, you are right partial and inverse propagation should always use the literal of the added edge in the reason. I am not sure about partial+ propagation. Anyway, I already spent too much time on this project. I am sorry but I have to stop here.
I just wanted to understand things better to find out a problem with an encoding i'm using.
I added some debugging code and partial+ adds clauses with just one literal (the rest facts).
I will try to come up with some initial lookahead strategy to capture these cases. Thanks a lot for your help.
I will try to come up with some initial lookahead strategy to capture these cases. Thanks a lot for your help.
It should be easy to change clingo-dl to do a full propagation on level 0...