Preferred Usage of Transition System
====================================
version 1.2, Nov. 20, 2006

CSP:

We define a regular expression that gives the preferred sequencing
of the transition rules of our transition system for CSP.

UP = UnitPropagate
D  = Decide
SSR= Semi-Superresolution

UPD = (UP* D)* UP*
(UPD ((SSR [Fail]) | Success) Restart )* 

Currently best:
UPD = (UP* D)* UP*
(UPD ((SSR | Success) (Fail | Restart ))*


Christine's proposal:
(UPD ((SSR | Success) [Fail] Restart )*
because it allows a nicer generalization to MaxCSP (see below):
(UPD ((SSR | Update) [Finale] Restart )*

Refined view:
* means repetition (0 or more times)
[...] means optional
Fail and Success are stop states
Both | and [...] imply a checkpoint.

The UPD part (loop) we exit when a constraint is unsatisfied
or all constraints are satisfied. In the first case, we learn with SSR.
If we learn the empty clause, we fail.
In the second case, we succeed.

Fail: if semi-superresolvent is empty.
Success: if all constraints satisfied

===========
Generalization to MaxCSP:

UPD = (UP* D)* UP*
(UPD ((SSR [Finale]) | Update ) Restart )*

Note: UP and SSR need to be updated to maintain and use
a "currently" best assignment N. State becomes M || F || N
where the third component N is a complete assignment.

After UPD we check whether more than or equal to unsat(N)
clauses are unsatisfied or whether we have a complete assignment better than N.
After SSR we check whether we have learned the empty clause -> Finale.
If not, we restart.
In the second case, we update N and restart.

It is important to notice that SSR and Update are mutually
exclusive. 
Either we have a complete assignment that is better
or that is worse or the same as the currently best N.
If it is worse or the same then we learn (SSR)
and otherwise we do Update.

Finale is the only stop state.

Update means: we have a complete assignment. Two subcases: 

1. better complete assignment found.
2. all constraints are satisfied  and we stop.

We use this organization because the first assignment N could already be the
maximum assignment.

Finale means: there is no better assignment.

===========
Christine's proposal:
(UPD ((SSR | Update) [Finale] Restart )*
to keep Update simpler and Finale more complex.
This makes Finale the only clean stop state.
(note that before Update was also a stop state)
===========

compare to (CSP):

(UPD ((SSR [Fail]) | Success) Restart )* 

N is the the best assignment found so far.

Next step:

how can we find all maximum assignments? Can we add more super resolvents?
This should also work to find all models, as a special case (all constraints
satisfied).