Homework 4: CSG 270
Due: Feb. 14, 2007
=================================================================================

Reading:
You will need AspectJ knowledge: 
http://www.eclipse.org/aspectj/
http://www.eclipse.org/aspectj/doc/next/progguide/language.html

About other CSP solvers:
http://www.sat4j.org/

Read the survey paper:
The Quest for Efficient Satisfiability Solvers
http://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf

The Quest for Efficient Boolean Satisfiability Solvers,
by L. Zhang and S. Malik, Invited Paper,
Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002)
and also in Proceedings of 14th Conference on Computer Aided Verification (CAV2002),
Copenhagen, Denmark, July 2002


Part 1:
=======

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

In hw 3 we implemented value ordering: either 0-1 or 1-0.

Here we focus on variable ordering: Given an instance
where we want to apply the decide rule:
which variable do we set first? We would like to choose a variable 
where the look-ahead polynomial gives a strong indication how
to do the value ordering.

The goal of value and variable ordering is to make "good" decisions without
excessive look-ahead polynomial computations.

Here is a basic variable ordering approach:
Let N be the currently best assignment.
For a CSP instance F with n variables, compute 2*n numbers as follows:
Set variable v to d (0 or 1), and compute F'=UP(F[v=d],N), where 
UP(F,N) applies UP as often as possible for N, without doing any
additional decides. Then we compute the value of the look-ahead polynomial
for F' at a maximum bias. This gives for each variable two numbers and we retain
the larger of the two with the assignment choice.
We sort the variables which gives us the current variable ordering which is a 
sequence of pairs (variable, variable value).

We use this variable ordering to choose the next variable and its value.

After having set a few variables through unit propagation, the reduced formula
will result in a different variable ordering. We choose a probability p_var_order
to determine before a decide, whether to recompute the variable ordering.
Set initiallly p_var_order = 1, i.e., we recompute before each decide.

Upon a restart, we go back to the original variable ordering.


Part 2: Specification-based software development
================================================

In specification-based software development we formulate constraints between inputs and outputs.

Can we sort with our MAX-CSP solver? Formulate the sorting problem as follows:
permutation( x,y ) and is_sorted( y ) where x is a sequence of u distinct v-bit numbers.
x is input and y output.
We view permutation( x,y ) and is_sorted( y ) as a specification of what we want and we let the
MAX-CSP solver work out the details.

In other words, does there exist a permutation of u distinct v bit numbers so that they are sorted?
Both predicates can be expressed using our MAX-CSP input notation.

You will need to write a generator that takes as input u and v and it produces as output
a MAX-CSP instance that, after setting x, has exactly one assignment y, the sorted version of x.

We are interested in the question:
Can the MAX-CSP solver invent one of the n*log(n) sorting methods using look-ahead polynomials
without backtracking?

Sort 4, 8, 16, 32 different 6 bit numbers.
How many Decide does your MAX-CSP solver make? Does it find the solution?
Does the number of Decide grow like n! or n*n or n log n? 

Note that this is a general question beyond sorting: how can we implement a
high-level specification expressed as a predicate. There are programming languages like Prolog
and Datalog that support specification-based software development.

What to turn in:
Your generator that produces MAX-CSP-instances for permutation( x,y ) and is_sorted( y ).
The input and output for 4, 8, 16, 32 distinct 6 bit numbers.

A discussion of the output: Did the MAX-CSP solver succeed? If not: what would you add to it?
If it did succeed, what kind of sorting technique did it "invent".


Part 3:
=======

Consider the Relation class:

/home/lieber/.www/courses/csg270/sp07/code/tst/src/edu/neu/ccs/evergreen/ir

and find all the places where error checking takes place.
Write an aspect that encapsulates the error checking.

The aspect will have the advantage that if the error checking is not needed,
we can simply not compile the aspect.

Implement your aspect in AspectJ.


====================================
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.

For the application domain: MAX-CSP 
The difference between value and variable ordering.
What can be done without backtracking?