CSG260 Advanced Software Development
Karl Lieberherr
Fall 2006

Homework 4
---------------------------------------------------------------------

Due date: Oct. 10, 2006

Now we want to put the pieces together. 
In a first step we want to satisfy all constraints, so we deal first with CSP 
and not MaxCSP.

We have algorithm
MAXMEAN that is useful for both variable ordering and value ordering.
For value ordering we use basically

if maxmean (S[x=0]) > maxmean (S[x=1])
  then x = 0 else x = 1

(maxmean(S) = turns S into a polynomial, maximizes it and returns the biased 
coin probability which guarantees the best result.)

For variable ordering we compute 
maxmean {S[x=0]) and maxmean (S[x=1]) for all variables x
and choose the x where maxmean is largest or where the difference between
maxmean {S[x=0]) and maxmean (S[x=1]) is largest.

We have algorithm Superresolution which learns from mistakes and adds
new clauses to the formula. The new clauses we add get a high weight
because they are implied by the original formula. If the constraints in the
original formula have weight tw then the learned clauses have weight tw+1.

The idea is that after we have learned a new superresolvent we are free
to restart MAXMEAN any way we like and we are guranteed not to fall into 
the same mistake again.

We want to integrate MAXMEAN and Superresolution as follows:
If we have a decision variable (also called a choice variable), we use MAXMEAN to
make the decision how to set the variable first.
When MAXMEAN runs into a contradition both ways, we add a superresolvent
and start from scratch.

My hope is that there will be a synergistic effect between the superresolvents 
learned and MAXMEAN. The superresolvents will influence the polynomials
that we optimize and hopefully in such a way that a satisfying example is
found faster.


Part 1:
============================================

Finish part 4 and 5 of hw 3.

Part 2:
=======

Ahmed has a good solution for this! Use his and acknowledge him 
in your solution/program.

Superresolution has been defined for CNFs (SAT) but we want to use the
idea for CSP and MaxCSP. In this part we generalize the notion of "forced"
variables from SAT to CSP with relations of at most rank 3.

Given a relation over domain {0,1} of at most rank 3, determine the variables
that are forced.
For example, Or(x) forces x to 1. if x=0 the relation is guaranteed to be unsatisfied.

The relation given by the truth table:
(nothing means 0)

xyz
000
001
010 1
100
011
101
110 1
111

forces y=1 and z=0. E.g., if y=0, the relation is guaranteed to be unsatisfied.

xyz
000 1
001
010 1
100
011
101
110 1
111

forces z=0.

Design a function forced:

int forced(int relationNumber, int variablePosition) 

which returns 0, 1 or -1. -1 means that the variable at variablePosition
is not forced. 0 or 1 means that the variable at
variablePosition is forced to 0 or 1, respectively.

Generalize the notion of superresolvent from SAT to CSP.
This is a refinement of hw 3 / Part 5.

I suggest that for hw 3 / Part 5 you first generalize 
superresolution from SAT to MaxSAT and then to MaxCSP
using the results of this homework.


Part 3:
=======

Integrate MAXMEAN and Superresolution for CSP.
Test your algorithm on some big examples that you get from the web.
What is the most popular input notation for CSP or for SAT?
Use that notation. Whoever researches this, send your examples to the class
list so that we can start an internal competition: which solver
solves them the fastest? At this point use only satisfiable examples
that come from real world applications.


Part 4:
=======

Integrate MAXMEAN and Generalized Superresolution for MaxCSP. 
Test on your own MaxCSP examples.


Part 5:
=======

Discuss ways of improving the efficiency of your solvers (in English only).
Some issues will be:

1. Can you incrementally update the polynomials rather than recumputing
   them from scratch after each reduction?

2. Go back to the paper you read in hw 1: what efficiency improvements should we
   implement?