Preferred Usage of Transition System
====================================
version 1.1, Nov. 17, 2006
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 )*
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 MaxSAT:
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.
compare to (SAT):
(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).