CODEWITHSUNDEEP
algorithmsat
César Leonardo Clemente López
César Leonardo Clemente López

Reputation: 191

What is the main reason to forget clauses within a Boolean Formula when using in the CDCL algorithm solving for SAT?

The Conflict Drive Clause Learning algorithm utilizes a backtracking component which is based on the 'learning' of new clauses (derived upon reaching a conflict during the search process for a truth assignment that satisfies a Boolean formula). These new clauses represent constraints in the truth assignments of the boolean formula which avoid reaching the conflict again and also guide CDCL in backtracking to the most early decision which is part of the conflict (and thus saving computation time).

As a reference, in ALBERT OLIVERAS (https://dl.acm.org/doi/pdf/10.1145/1217856.1217859) paper, they introduce backtracking and mention the use of "learn" and "forget" functions within the CDCL algorithm with the object of detecting and erasing these new clauses.

My question is, why would forget a new learnt clause that avoids your conflict?

Upvotes: 1

Views: 73

Answers (1)

alias
alias

Reputation: 30418

The simplest way to think about this is in terms of garbage collection. There's a non-trivial cost of keeping around clauses that are implied by what you already know. If you have millions of clauses learned, it can seriously impact performance. So, mostly depending on statistical analysis, solvers tend to "forget" clauses that they determine to be irrelevant. Needless to say, this is guided by heuristics, and may end up costing you more time as you might have to re-learn some of those clauses. But, in general, forgetting helps with exploring dead-end paths that are not found to be productive.

Upvotes: 1

Related Questions