Partial MaxSAT computation of Conformance Checking Artefacts

Jesus Ojeda


To reason about observed behaviour of processes and their models, conformance checking techniques are rooted in the computation of artefacts. Related artefacts like alignments, multi-alignments and anti-alignments are defined over a distance function, most commonly Hamming or Levenshtein distances. In this paper we provide a new Partial MaxSAT encoding of these artefacts based on the Levenshtein distance and compare with their current state-of-the-art SAT encodings. We show a reduction in the resulting formula size for our proposed encoding, while also obtaining good performance results on the computation of the artefacts.