Target Phases [July 3, 2020]


by Armin Biere and Mathias Fleury for the 11th Pragmatics of SAT International workshop (


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.


Added by :
Daniel Le Berre

Updated on :
July 4, 2020, 12:23 p.m.

Duration :

Number of view :
95 (Show details views)

Type :

Main language :

 Embed/Share (Draft Mode)
Please note that your video is in draft mode.
The following links contain a key allowing access. Anyone with this links can access it.
Check the box to autoplay the video.
Check the box to loop the video.
Check the box to indicate the beginning of playing desired.