Homework 3: CSG 270
Due: 
=================================================================================

Reading:
http://www.ccs.neu.edu/home/lieber/s/sat07-sub.pdf

We switch now to a stable syntax for MAX-CSP:

http://www.ccs.neu.edu/home/lieber/courses/csg270/sp07/guaraldi/sat_input.cd.txt

Part 1:
=======

In hw 1 we implemented a verifier for CSP, in hw 2 we implemented a 
non-backtracking partial solver for MAX-CSP which 
uses an oracle to make "perfect" decisions in the decide rule.
In this homework we will use look-ahead polynomials to make "clever"
decisions in the decide rule. We will use a stochastic method 
to finding a good solution using look-ahead polynomials.
Stochastic method: no guarantee to obtain a solution.
We will later extend to a complete method.
(other such stochastic methods:
Random Walk: WalkSAT, AdaptNovelty+, g2wsat, R+AdaptNovelty+
Clause Weighting: SAPS, PAWS, DDFW, R+DDFW+
)

The state of the transition system is extended 
with the maximum bias of the look-ahead polynomial.

M | F | N ----> M | F | N | mb

We update rule X to X-la accordingly.
In addition the initial state and the rules are updated as follows:

Initial State:
{} | F | N | mb
where mb is a maximum bias la[F,N](x) and
where N is the all 0 assignment (could be any other assignment).

The maximum bias is updated with probability q in Decide-la:

Decide-la:
D: M | F | N | mb -> Mk | F | N | mb2
if k is not in M and v(k) occurs in some constraint in F
and mb2 is a maximum bias for la[F2,N](x) 
where F2 is F reduced based on the partial assignment M and 
k=!N(v(k)) with probability mb2.

N(v(k)) is the literal that represents the assignment by N to v(k). 

v(k) is the variable corresponding to the literal k.

Finale-la: (final transition)
M | F | N | mb -> M | F | N | mb
if unsat(N,F) = 0 or Restart was repeated c times (e.g., c = 20) .

Restart-la:
M | F | N | mb -> {} | F | N | mb_initial
where mb_initial is the mb of the initial state.

UPD-la = Restart-la (UP-la | D-la)*

The sequence (UP-la | D-la)* must have the property that
UP-la is given preference over D-la if UP-la is applicable.

desired sequence
(UPD-la Update-la)* Finale-la

Software to reuse:

The relation class from hw 1.

The SAT solver interface which we call the appmean interface:
http://www.ccs.neu.edu/home/lieber/courses/csg270/sp07/guaraldi/
http://www.ccs.neu.edu/home/lieber/courses/csg270/sp07/guaraldi/satsolver-1.1/api/index.html

The appmean interface gives you appmean[F](x). 
The interface has a deficiency that you need to identify and you need to produce
a better version.

The appmean interface comes with three implementations. Use the one by Daniel Rinehart.

Implementation suggestion:
n-map the formula F so that "all 0"  is always the currently best assignment.
This makes it easier to compute the look-ahead polynomial.
You can directly use appmean, what the appmean interface returns.


Part 2:
=======

Write a program that takes as input:
1. A MAX-CSP(Gamma)-instance with n variables.
2. an integer k between 0 and n.
It produces as output:
the mean(k,n) and standard deviation sd(k,n) of the fraction of satisfied constraints
over all binomial(n,k) = n!/(k!(n-k)!) [the binomial coefficient] assignments setting exactly k of n
variables to true.
For the definition of standard deviation:
http://en.wikipedia.org/wiki/Standard_deviation

Compare the look-ahead polynomial la[F,N](k/n), where N is the all 0 assignment,
with mean(k,n). How close are they?

To generate the binomial(n,k) assignments, you may want to use
the recursive definition of the binomial coefficients inherent in Pascal's triangle.


====================================
What do you learn in this homework?
The method of interface driven software development (improving the appmean interface)
The design by contract method.