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.