While doing some basic research about the new --single-shot option of clingo in this issue, I found out that not only preprocessing and frozen literals may have a performance influence, but also the step literal which seems to be added to every learnt clause.
The only reason I could think of why this learnt information is tagged with the step literal is enumeration.
I do not see any reason why information derived from non tagged clauses (or in my case, from a deterministic propagator) should be tagged with a step literal and therefore be retractable. So the question is: would it be possible to only add the step literal to enumeration relevant clauses? I think this could (partly) address the problem of the reported performance degradation when switching from the Application to the API.
After reading the paper about enumeration I could imagine that there is no such thing as "enumeration relevant clauses", but maybe you have an idea. Otherwise, this can simply be closed.
While doing some basic research about the new
--single-shotoption ofclingoin this issue, I found out that not onlypreprocessingandfrozenliterals may have a performance influence, but also thestepliteral which seems to be added to every learnt clause.The only reason I could think of why this learnt information is tagged with the
stepliteral is enumeration.I do not see any reason why information derived from non tagged clauses (or in my case, from a deterministic propagator) should be tagged with a
stepliteral and therefore be retractable. So the question is: would it be possible to only add the step literal toenumerationrelevant clauses? I think this could (partly) address the problem of the reported performance degradation when switching from the Application to the API.After reading the paper about enumeration I could imagine that there is no such thing as "enumeration relevant clauses", but maybe you have an idea. Otherwise, this can simply be closed.