Corrigendum to “Mining Closed High Utility Itemsets based on Propositional Satisfiability” [Data Knowl. Eng. 136C (2021) 101927] (Data & Knowledge Engineering (2021) 136, (S0169023X21000549), (10.1016/j.datak.2021.101927))

The authors would like to make the following clarification to their article: Algorithm 1 is an extension of the DPLL procedure [1]. It enumerates the set of all models of a given CNF formula [Formula presented]. In fact, the traditional DPLL procedure, introduced since 1962, allows to find (if exists) one model of [Formula presented]. In our case, we need to enumerate all models of the formula [Formula presented]. So, when a model is found we perform a simple backtracking to look for the next models. To be precise, the traditional DPLL procedure checks only the satisfiability of [Formula presented] without computing the models of [Formula presented]. However, Algorithm 1 checks first the satisfiability of [Formula presented], i.e., all the variables of [Formula presented] are assigned (line 11). If so, it returns the set of all models of [Formula presented] (line 16). All these elements are provided by the algorithm description. We note that Algorithm 1 in the original paper has a careless mistake. Notice that this has no influence on any results in the paper. This small mistake concerns line 1 where [Formula presented] means that [Formula presented] is a unit literal (e.g., [Formula presented] since [Formula presented] is unit and [Formula presented] becomes unit due to [Formula presented]). In other words, the formula [Formula presented] is simplified by unit propagation. So, [Formula presented] is not chosen but it is deduced from [Formula presented]. In Algorithm 1, we recover the models with [Formula presented] and those with [Formula presented], and we return their union (line 16), i.e., the set of all models of [Formula presented] (return [Formula presented]). [Formula presented] The SAT solver engine (i.e., Algorithm 1) is used to enumerate all the models of our proposed encoding of the problem of (closed) high utility itemset mining. Each output model corresponds to a (closed) high utility itemset in the database [Formula presented] w.r.t. the minimum utility threshold [Formula presented]. The results of the mining process using a SAT solver are presented in the experiment section. Our implementation is also available on the git repository at: https://github.com/amel-hidouri/SATCHUIM