2015-09-16 3 views
2

Lorsque l'on parle de solveurs SAT, du type de minisat par exemple, que signifient les valeurs "0-depth" et "CNF"? Ces valeurs font généralement partie de la sortie d'information de divers solveurs SAT.Solveurs SAT, affectations 0-profondeur

Répondre

2

Une affectation de profondeur nulle définit la valeur d'une variable avant que la recherche DPLL ait commencé. Le prétraitement de la formule que fait MiniSAT (subsumption, self subsumption, etc.) peut parfois prouver qu'une variable doit avoir une certaine valeur. Si cela est possible, MiniSAT fixera la valeur de ces variables avant de commencer la procédure DPLL.