Candidate Test with Conflict Extraction procedure Test Candidate(C, M,obs) 1. Assert candidate assignment c 2. Propagate obs through model m using unit propagation 3. If inconsistent clause return Conflict(c) 4. Else search for satisfying solution using DPLL fE inconsistent return c as a conflict se return consistent 10/03/03 copyright Brian Williams, 200310/03/03 copyright Brian Williams, 2003 14 Candidate Test with Conflict Extraction procedure Test_Candidate(c,M,obs) 1. Assert candidate assignment c 2. Propagate obs through model M using unit propagation. 3. If inconsistent clause return Conflict(c) 4. Else search for satisfying solution using DPLL • If inconsistent return c as a conflict. • Else return “consistent