NoGood Forgetting

[AntoniusW]

Alpha uses a CDNL-based solving component which learns new nogoods after running into conflicts. Over time, the number of nogoods becomes very large and many of the learned ones are not helpful to later search. The search almost grinds to a halt due to the massive number of superflous nogoods, which need to be treated during propagation. SAT solvers and other APS solvers therefore implement some form of nogood forgetting in order to speed-up the search and only keep those nogoods that are useful. There is a variety of literature on this topic and Alpha needs some form of nogood forgetting in order to solve the harder instances from the ASP competition.

[lorenzleutgeb]

1. Entry point of forgetting in clasp
2. Entry point of forgetting in SAT4J (this is about variable forgetting, not clause/nogood forgetting)
3. A Bird’s-Eye View of Forgetting in Answer-Set Programming
4. Forgetting in ASP: The Forgotten Properties
5. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

[AntoniusW]

Note: the SAT4J link points to variable forgetting, not clause/nogood forgetting. Those are different things.

[AntoniusW]

6. Predicting Learnt Clauses Quality in Modern SAT Solvers introduces glue clauses and LBD measure as used in the Glucose SAT solver.

[jblaszczyk]

Good idea but keep in mind forgetting leads to incompleteness.

[lorenzleutgeb]

Good idea but keep in mind forgetting leads to incompleteness.

@jblaszczyk No, it does not. Learned nogoods that do not imply anything for the current partial assignment can be forgotten without making the search incomplete.

General note regading this issue: We should not forget that we are grounding lazily, so we might not only forget nogoods, but also datastructures in the grounder. This interferes with grounding heuristics.

[rtaupe]

Is this implemented by #197?

[lorenzleutgeb]

Is this implemented by #197?

Ping @AntoniusW