Solving error correction for large data sets by means of a SAT solver

The paper is concerned with the problem of automatic detection and correction of erroneous data into large datasets. The adopted process should therefore be computationally efficient. As usual, errors axe here defined by using a rule-based approach: all and only the data records respecting a set of rules axe declared correct. Erroneous records should afterwards be corrected, by using as much as possible the correct information contained in them. By encoding such problem into propositional logic, for each erroneous record we have a propositional logic formula, for which we want a model having particular properties. Correction problems can therefore be quickly solved by means of a customized SAT solver. Techniques for an efficient encoding of difficult cases are presented.