DPLL: teach solver (in generator) about variable elimination