he hearth of the brute-force algorithm lies here. Wwe want to
    iterate on the state-space (which can be hudge) and stop the
    first time we hit a consistant state. This means two things:
    (i) we don't want to build the full universe before iterating
    on it; (ii) we need to enumerate the states in a meaningful
    order, eg. an order which should reflect the optimization
    criteria we are intersted in.<br>
<br>
To overcome this difficulties, we use a monotonous successor
    function to compute 