Sat4j 2.3.2: on the fly solver configuration

Abstract

Taking the best of SAT (at large) technology for a given class of problems requires usually an expert knowledge of the solver used or to rely on an automatic configuration tool. The former condition is usually not satisfied as soon as the user is not a member of the SAT community, and the latter solution does not help the user to understand what is going on inside the solver. We propose an approach that allows the end users of Sat4j to configure a solver for a specific instance. Such an approach is based on both the ability to change dynamically the main settings of the solver when it is running and to display to the user several metrics that inform her about the state of the search in the solver. While the latter has been already explored in the SAT community, and the former has been explored in the constraint programming community, we believe that the combination of that two features is quite unique for SAT solvers. We believe that such a tool could also be used in the classroom to help students to understand how CDCL solvers work.