3/4/03
Josh Ryan

-Memo's in graphplan such as X1, X2, X3 is essentially a no good in csp of
the form: ~(x1!=# X2!=#X3!= #)

This basically means that every memo is a set of no goods! So more use and less
space used to store.
 
Each m size memo corresponds to d^m no goods.




PG0		|		PG1      All constraints of CSP0 are in  
 |              |                |       CSP1 but mutexs are added to CSP1
 |              |                |       
 |              |                |       All solutions of CSP1 are solutions of CSP0
 |              |                |
 |              |                |       CSP1 - possibly higher level of consistency
 V              |                V
                | 
CSP0	--------|------------>  CSP1
                |
                |



K consistency: if and only if every consistent assignment for k-1 of the n variables
can be extended to include any k-th variable.

Given three variables X, Y, and Z all with domains of integers from 1 to 10,
and constraints X<Y, Y<Z, Z<X 
to enforce two consistency we see that if X=10, then Y can have no value, 
so we remove 10 from X's domain.  We also see that if Y = 1 X has no values
So we remove 1 from Y's domain.  We also see that if Y = 10 then Z has no values
So we remove 10 from Y's domain, and so on.

CSP1 s basically a 3 consistant version of CSP0.

Finding the mutexs on Graph plan are faster then enforcing 3 consistency on CSP
because 3 consistecy takes n^3 time.

Graph plan mutexs are directed partial 3 consistency, which avoids extra constraints
from level to level and avoids not very useful constraints that are never actually 
encountered.

Three consistency says:

For all x, y, z that exists in Var(CSP)  
For all V1, v2 Consistant (x=v1 ^ y=v2) => There exists a v3
consistant(x=v1 ^ y=v2 ^ z=v3)

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

Alternative encodngs: csp, sat, ip

SAT:  Any CSP can be made into a sat encoding.

Each pair of variables in the csp with constraints such as x < y is converted into
a set of SAT variables such that every possible combination of x and y such that
x is < y is defined..

Actions are encoded as Action => precondition
such as: Load-A-1 => At-R-E-0 ^ At-A-E-0 

Mutex:
~in-A-1 v ~A-R-M-1     ~in-B-1 v ~At-R-M

Blackbox uses SAT to solve planning problems, converts planning to standard SAT
encoding and then feeds problem to any SAT solver.

History of SAT solvers: 
DP -> Satz which spends lot of time choosing which variable
to assign a value to next, so much so that people thought it would not reall work
but it did ok for it's day

Then came GSAT/WALKSAT which both use local search (remember hillclimbing algorithm)
In practice they solved problems much faster then the other SAT planners before
them, but because local search can get stuck in local mins they can not gaurantee
optimal solutions.

Then cam RELSAT which added relavence based learning to normal SAT solving.

Then in 2001 CHAFF came from the EE world and kills all other SAT solvers,
but has so many components all seeming to add to the performance that the
SAT community can not find which parts of CHAFF make it fast.

Blackbox re-released with chaff and performs very well.

---------------------------------------------------------------
ILP: (linear programming)

Constraints become linear inequalities

Each constraint becomes a hyper plane in the problem space

The maximums of the enclosed area are the solution(s), maximums are alwasy in corners

If the problem is inconsistent then there is no inner area formed by the
hyper planes.

Solvers: Simplex Algorithm by Danzig - exp time in worst case but usually does better

Linear programming has been shown to be polynomial time in general.

Integer Programming is taking the ILP problem and forcing variable values to be
integral, which may seem to be an easier problem, but makes the search space into an
enumeration.