Consider the implication graph at a stage where there is a conflict
and fix a conflict graph contained in that implication graph. Pick any
cut in the conflict graph that has all decision variables on one side,
called the reason side, and 
as well as at least one
conflict literal on the other side, called the conflict
side. All nodes on the reason side that have at least one edge going
to the conflict side form a cause of the conflict. The negations
of the corresponding literals forms the conflict clause
associated with this cut.
Journal of Artificial Intelligence Research 22 (2004). Copyright AI Access Foundation. All rights reserved.