# Four algorithms for propositional forgetting

arXiv: https://arxiv.org/abs/2204.06528 · HTML: https://mlsanity.com/paper/2204.06528/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 68 references that are in the map.
- First posted on arXiv 13 Apr 2022.

## Builds on (most cited first, 5 of 5)

- [A Syntactic Operator for Forgetting that Satisfies Strong Persistence](https://mlsanity.com/paper/1907.12501/) (2019)
- [When You Must Forget: beyond strong persistence when forgetting in answer set programming](https://mlsanity.com/paper/1707.05152/) (2017)
- [On Forgetting in Tractable Propositional Fragments](https://mlsanity.com/paper/1502.02799/) (2015)
- [On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach](https://mlsanity.com/paper/2003.06492/) (2020)
- [Common equivalence and size after forgetting](https://mlsanity.com/paper/2006.11152/) (2020)

## Abstract (arXiv)

Four algorithms for propositional forgetting are compared. The first performs all possible resolutions and deletes the clauses containing a variable to forget. The second forgets a variable at time by resolving and then deleting all clauses that resolve on that variable. The third outputs the result of all possible linear resolutions on the variables to forget. The fourth generates a clause from the points of contradiction during a backtracking search. The latter emerges as the winner, with the second and first having some role in specific cases. The linear resolution algorithm performs poorly in this implementation.