SAT and MaxSAT Encodings for Trees Applied to the Steiner Tree Problem

In this paper we present some SAT and MaxSAT codifications for trees in graphs. We review two known encodings and suggest four new ones. We categorize the encodings into three categories: Absolute encodings state that each vertex must be in a fixed position in some structure, Relative encodings state the relative positions between the vertices in some structure, Counting-based encodings use theoretical graph properties to hardcode the degree of each vertex in a tree. We use these encodings to reduce the Steiner Tree Problem in Graphs to (Partial Weighted) MaxSAT and compare their efficiency to solve random instances and ones from the SteinLib benchmark. The experiments strongly suggest that relative encodings are more efficient than absolute ones, but there is not an overall best encoding between relative and counting-based ones.