Homework 5: CSG 270
Due: Feb. 21, 2007
=================================================================================

Reading:

Towards Understanding and Harnessing the
Potential of Clause Learning
Paul Beame beame@cs.washington.edu
Henry Kautz kautz@cs.washington.edu
Ashish Sabharwal ashish@cs.washington.edu
Computer Science and Engineering
University of Washington, Box 352350
Seattle, WA 98195-2350, USA

https://wiki.ccs.neu.edu/pages/viewpageattachments.action?pageId=1850

Read sections: 1-2.4 and section 3.


Part 1:
=======

We continue to practice the transition-system based method to software development
and we refine our system further.

Consider the following CSP instance:

It was tested in:
/home/lieber/.www/courses/csg270/sp07/hw/4/csp-input

c This is a test input for the MAX-CSP solver

c What is the maximum number of constraints that can be satisfied?
c give a proof of your claim.

p 9 8

22 : 1 2 3					0
22 :                4 5 6			0
22 :                               7 8 9	0
22 : 1              4              7		0
22 :   2              5              8		0
22 :     3              6              9	0
22 : 1                5                9	0
22 :     3            5            7		0

How do you prove that the maximum assignment only satisfies all
but one of the constraints?

One way of doing the proof would be to enumerate all 2^9 = 512 assignments
and pick a maximum one. This proof is simply too long.

A second approach is to produce an assignment that satisfies all but one
and then to reason that it is the best:

1 !2 !3 !4 5 !6  !7 !8 9
satisfies all but:
22 : 1                5                9	0

Now we can argue as follows:
Choose 1:
1 forces !2 !3 !4 !7 otherwise a constraint would be unsatisfied.
But 1 also forces 5 and !5 so we have a contradiction for which we need to
find the minimal reason. Because 1 was the only choice we made, we negate 1
and learn the constraint:
85 : 1 0

Now 1 is no longer chosen, but forced by the new constraint:
!1 
Choose 5:
5 forces !4 !6 !2 !8 !9 !3 conflict: 1. constraint is unsatisfied.
Because only 5 was chosen, that must be the mistake! We learn:
85 : 5 0

Now both !1 and !5 are forced:
!1 !5
This forces 9 !3 !6 !7 !8 conflict: last constraint is unsatisfied.

But we did not choose anything: the contradiction was forced:
So we cannot improve the assignment.

Our proof consists of the two important learning steps:

85 : 1 0
85 : 5 0
based on 1 !2 !3 !4 5 !6  !7 !8 9 = N = the currently best assignment.

To turn this proof idea into a formal proof system,  we refine
our transition system as follows:

We extend our basic system with an additional component to keep
track of the learned constraints:

M | F | N -> M | F | SR | N

where SR consists of a sequence of constraints that are learned
during the transition system execution. In the above example, SR became:

85 : 1 0
85 : 5 0

The Decide rule now keeps track of decision variables:

M | F | SR | N -> Mk* | F | SR | N

We use the * to flag the decision literals in the partial assignment,
for example:.

1* !2 !3 !4 !7  ... 

And finally we need a new rule in our transition system for learning
from our mistakes:

SSR (Semi-Superresolution):

Let NewSR be a disjunction (or) of the negation of all decision literals in M.
In general the NewSR may be of high rank.

M | F | SR | N -> M | F | SR, NewSR | N

if unsat(M,SR) > 0 or unsat(M,F) >= unsat(N,F).

SR, NewSR is the concatenation of the two argument sequences.

The update to Decide to keep track of decision literals  and the new SSR 
rule add non-chronological backtracking to our transition system.
This is a technique that I invented in the early 1970s.
http://www.ccs.neu.edu/home/lieber/clause-learning/comparison-to-newer-works.html
and it is now widely used in SAT and CSP solvers.

Note that the constraints in SR are hard (all must be satisfied), 
while the constraints in F are soft.

Implement non-chronological backtracking in your MAX-CSP solver.
Of course, this means that you keep the other features you have added
in earlier hws.

Part 2:
=======

Apply now your updated solver to the earlier test cases, 
such as the sorting test cases.
Does it solve the problems now?
How fast does it sort now?

Part 3:
=======

Consider the RelationCore class in:

/proj/demeter/evergreen/software/ir/src/edu/neu/ccs/evergreen/ir
http://www.ccs.neu.edu/evergreen/software/ir/doc/index.html

Invent a way to make it easy to use the RelationCore class.
This is an exercise in interface design.

Requirements for the interface:
1. make it easy to always work with the same relation number, for example 3,
   without having to repeat the relation number in the method calls.
2. provide a factory object that has a create method that takes the rank
   as an argument. It returns an object that satisfies a RelationI interface that
   supports the methods of RelationCore that need to be publically visible,
   such as:

   public int reduce(int relationNumber, int variablePosition,int value)
   public boolean isIrrelevant(int relationNumber, int variablePosition)
   public int numberOfRelevantVariables(int relationNumber)

   Note that rank is absent from those signatures because it is stored in the
   object returned by create.

https://wiki.ccs.neu.edu/pages/viewpageattachments.action?pageId=2820&sortBy=date&highlight=DesignJava.pdf
for design patterns.

====================================
What do you learn in this homework?
The method of aspect-oriented software development.
The method of specification-based software development.
Deepening the transition-system based method of software development.