The algorithm for the first example reads just like an implementation of a SAT solver. Set a variable, propogate clauses, backtrack on conflict (learn new 'rule' from conflict).