Extract Conflict by Tracing Support procedure Confli ict(C) /C is an inconsistent clause for each literal l in C union Support-Conflict (, support() end Conflict procedure Support-Conflict(, s) If unit-clause? (C) If mode-assignment? (teral (C) Then literal(C)1 Else Else for each literal 1 in C, other than l Union Support-Conflict(1, support (1)) end Support-Conflict 10/03/03 copyright Brian Williams, 2003 1310/03/03 copyright Brian Williams, 2003 13 procedure Conflict ( C) // C is an inconsistent clause for each literal I in C union Support-Conflict(l, support(l) ) end Conflict procedure Support-Conflict(l,S) If unit-clause?(C) If mode-assignment?(literal (C)) Then { literal(C) } Else { } Else for each literal I1 in C, other than l Union Support-Conflict(l1, support(l1)) end Support-Conflict Extract Conflict by Tracing Support