Four algorithms for propositional forgetting

TL;DR

This paper compares four algorithms for propositional forgetting, finding that the backtracking search method generally outperforms the others, with linear resolution being less effective in this implementation.

Contribution

The paper introduces and empirically evaluates four different algorithms for propositional forgetting, highlighting the effectiveness of the backtracking search approach.

Findings

Backtracking search algorithm outperforms others in propositional forgetting.

Linear resolution performs poorly in the tested implementation.

The first and second algorithms have specific cases where they are effective.

Abstract

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.