An example of applying MAX-SAT solver
=====================================================================
The following derivation can be further optimized by the introduction
of new rules into our MAX-SAT solver. Yet, the optimization will not 
be covered in this version.

version 1.2, Nov. 16, 2006
=====================================================================

Abbreviation used:
UP --- Unit-Propagation
SSR --- Semi-Superresolution
d* --- decision literal
+ --- or
, --- and
{} --- empty set

---------------------------------------------------------------------

F=1+2, 3+4, 5+6, !1+!3, !1+!5, !3+!5, !2+!4, !2+!6, !4+!6
M={}
------------------------------------------------------
N={!1 !2 !3 !4 !5 !6}, unsat(N;F)=3

{}||F||!1 !2 !3 !4 !5 !6

=>1*||F||!1 !2 !3 !4 !5 !6 (by Decide) 

=>1* 3*||F||!1 !2 !3 !4 !5 !6 (by Decide) 
unsat({1 3};F)=1<unsat(N;F),
unsat({1 5};F)=1<unsat(N;F)

=>1* 3* !5||F||!1 !2 !3 !4 !5 !6 (by UP) 
unsat({1 3 5};F)=3=unsat(N;F)

=>1* 3* !5 !6*||F||!1 !2 !3 !4 !5 !6 (by Decide)
unsat({1 3 !5 !6};F)=2<unsat(N;F)

=>1* 3* !5 !6* 2*||F||!1 !2 !3 !4 !5 !6 (by Decide)

=>1* 3* !5 !6* 2* !4||F||!1 !2 !3 !4 !5 !6 (by UP)
unsat({1 3 !5 !6 2 4};F)=3=unsat(N;F)

=>1* 3* !5 !6 2* !4||F||1 3 !5 !6 2 !4 (by Update)
unsat({1 3 !5 !6 2 !4};F)=2<unsat(N;F)

--------------------------------------------------------
N={1 3 !5 !6 2 !4}, unsat(N;F)=2

=>{}||F||1 3 !5 !6 2 !4 (by Restart)

=>1*||F||1 3 !5 !6 2 !4 (by Decide) 

=>1* 3*||F||1 3 !5 !6 2 !4 (by Decide) 
unsat({1 3};F)=1<unsat(N;F)

=>1* 3* !5||F||1 3 !5 !6 2 !4 (by UP) 
unsat({1 3 5};F)=3>unsat(N;F)

=>1* 3* !5 6||F||1 3 !5 !6 2 !4 (by UP)
unsat({1 3 !5 !6};F)=2=unsat(N;F)

=>1* 3* !5 6 !2||F||1 3 !5 !6 2 !4 (by UP)
unsat({1 3 !5 6 2};F)=2=unsat(N;F)

=>1* 3* !5 6 !2 !4||F||1 3 !5 !6 2 !4 (by UP)
unsat({1 3 !5 6 !2 4};F)=2=unsat(N;F)

=>1* 3* !5 6 !2 !4||F||1 3 !5 6 !2 !4 (by Update)
unsat({1 3 !5 6 !2 !4};F)=1<unsat(N;F)

------------------------------------------------------------
N={1 3 !5 6 !2 !4}, unsat(N;F)=1

=>{}||F||1 3 !5 6 !2 !4 (by Restart)

=>1*||F||1 3 !5 6 !2 !4 (by Decide) 

=>1* !3||F||1 3 !5 6 !2 !4 (by UP)
unsat({1 3};F)=1=unsat(N;F)

=>1* !3 !5||F||1 3 !5 6 !2 !4 (by UP) 
unsat({1 !3 5};F)=1=unsat(N;F)

=>1* !3 !5 4||F||1 3 !5 6 !2 !4 (by UP)
unsat({1 !3 !5 !4};F)=1=unsat(N;F)

=>1* !3 !5 4 6 ||F||1 3 !5 6 !2 !4 (by UP)
unsat({1 !3 !5 4 !6};F)=1=unsat(N;F)

=>1* !3 !5 4 6 !2||F||1 3 !5 6 !2 !4 (by UP)
unsat({1 !3 !5 4 6 2};F)=3>unsat(N;F)

=>1* !3 !5 4 6 !2||F, !1||1 3 !5 6 !2 !4 (by SSR)
unsat({1 !3 !5 4 6 !2};F)=1=unsat(N;F)

=>{}||F, !1||1 3 !5 6 !2 !4 (by Restart)

=>1||F, !1||1 3 !5 6 !2 !4 (by UP) 

=>1 !3||F, !1||1 3 !5 6 !2 !4 (by UP)
unsat({1 3};F)=1=unsat(N;F)

=>1 !3 !5||F, !1||1 3 !5 6 !2 !4 (by UP) 
unsat({1 !3 5};F)=1=unsat(N;F)

=>1 !3 !5 4||F, !1||1 3 !5 6 !2 !4 (by UP)
unsat({1 !3 !5 !4};F)=1=unsat(N;F)

=>1 !3 !5 4 6 ||F, !1||1 3 !5 6 !2 !4 (by UP)
unsat({1 !3 !5 4 !6};F)=1=unsat(N;F)

=>1 !3 !5 4 6 !2||F, !1||1 3 !5 6 !2 !4 (by UP)
unsat({1 !3 !5 4 6 2};F)=3>unsat(N;F)

=>1 !3 !5 4 6 !2||F, !1, {}||1 3 !5 6 !2 !4 (by SSR)
unsat({1 !3 !5 4 6 !2};F)=1=unsat(N;F), an empty clause is learned

=>1 !3 !5 4 6 !2||F, !1, {}||1 3 !5 6 !2 !4 (by Finale)
unsat({1 !3 !5 4 6 !2};F)=1=unsat(N;F)
the current assignment contains no decision literals

Clearly, our transition sequence above corresponds with the following
regular expression:

(UPD (SSR | Update ) [Finale] Restart )*