Chasing Target Phases

Beschreibung

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.

Zeitraum	03 Juli 2020
Ereignistitel	23nd International Conference on Theory and Applications of Satisfiability Testing
Veranstaltungstyp	Konferenz
Ort	ÖsterreichAuf Karte anzeigen