Explaining detectable precedences for the disjunctive constraint

Abstract

As lazy clause generation has seen much success in recent years, the generation of explanations has become the focus of much research. This paper describes how explanations can be generated for detectable precedences in the disjunctive constraint. We also provide a method to incorporate these explanations into the filtering algorithm proposed by Fahimi et al. [7] by adapting Vilím’s explanations [18]. We proposed two approaches to generating explanations: an approach using only the previously scheduled tasks to explain propagation and an approach using an even smaller subset of tasks combined with explanation lifting. An empirical evaluation of two of our approaches for generating explanations compared to a baseline with naïve explanations found that both approaches performed better in terms of conflicts, LBD, learned clause length and runtime. The most advanced approach of the two (last cluster) performed the best. We believe that using the last cluster approach to generating explanations with other propagators for the disjunctive constraint could be successful.