Target Phases

by Armin Biere and Mathias Fleury for the 11th Pragmatics of SAT International workshop (http://www.pragmaticsofsat.org/2020/)

We discuss and evaluate the idea of target phases introduced first in CaDiCaL in 2019 and also ported to our latest SAT solver Kissat. Target phases provide a heuristic to choose the value assigned to decision variables. This technique is an extension of phase saving. It extends promising assignments derived by the solver towards full models. Combined with alternatively applying series of Glucose-style and Luby-style restart, the technique is particularly effective on satisfiable instances.