Je présente dans ce billet une idée qui est décrite en anglais dans cette note. Elle consiste à exploiter des séquences d’hypothèses et de déductions pour produire des clauses qui sont conséquences logiques de celles ayant servi à réaliser les déductions, comme le font les solveurs CDCL, mais avec une approche différente, permettant de produire d’autres clauses.
Par exemple, considérons cette séquence contradictoire d’hypothèses et de déductions qui pourrait être produite par un solveur SAT de type CDCL ou même DPLL. Je propose d’appeler une telle séquence AUP-séquence contradictoire (AUP pour Assumption and Unitary Propagation).
