Takehide Soh (Kobe University, Japan)

This talk about SAT encoding consists of two parts. The first part briefly explains recent our work around SAT encoding—a SAT-based CP system “scarab” and a hybrid encoding integrating the order and log encodings. In the second part, as an application of the order encoding, we detail a propositional logic based approach to solve MultiObjective Discrete Optimization Problems (MODOPs). In this approach, there exists a one-to-one correspondence between a Pareto front point of MODOP and a P-minimal model of the CNF formula obtained from MODOP. This correspondence is achieved by adopting the order encoding as encoding for multiobjective functions. Finding the Pareto front is done by enumerating all P-minimal models. The beauty of the approach is that each Pareto front point is blocked by a single clause that contains at most one literal for each objective function. We evaluate the effectiveness of this approach by empirically contrasting it to a state-of-the-art MODOP solving technique.