※ 引述《chiungyu ()》之铭言：
: I am still not quite sure about how it works.
: 1. How do we choose the variable to be resolved? That is, how do we know which
: inequalities are to be summed?
The resolved variable is the implied variable. For example, in slide #101,
(1) The inequality implies (x1, 1) is (a).
(2) The inequality implies (x1, 0) is (b).
(3) Therefore, the resolved variable is x1, and we should do (a) + (b) ==> (d)
(4) Going backward, (x3, 0) is implied by (c) and therefore, the resolved
variable is x3 and we should do (c) + (d) ==> (e)
: 2. When can we be sure that no more conflicts can be introduced by resolution?
: It seems that the order that we conduct resolution operations can affect
: the slack. Is this true? And if so, when can we stop the process?
Yes, the order may affect the slack.
You should monitor the slack of each resolved inequality. When it becomes
non-negative, it is oversatisfied and you should stop the learning process.
The reason is because the slacks for the implying inequalities (except for
the conflict inequality) are smaller than their a_max's and >= 0. If the
slack for the current resolved inquality is >= 0, it is impossible to get
under 0 afterwards.