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

Implement a recursive backtrack algorithm for finding
a maximal interpretation (satisfying the maximum weight)
for the standard satisfiability problem. Use
the OR relations (OR1, OR2 and OR3).

I suggest a simple algorithm of the form:

P(f) :
f is a cnf.
  if f has at least one unassigned variable x
    P(f[x=1])
    P(f(x=0])

This algorithm would explore the entire search tree of size 2**n
where n is the number of variables in f.

For efficiency reasons, we use the following variant of
the above algorithm that will explore a smaller search space.

I = random interpretation; // currently best interpretation
current_min_weight_unsat = weight of unsatisfied clauses by I;

Precise(f) returns interpretation I 
if f has at least one unassigned variable x
 consider f reduced for x = 1;
 if weight_unsat(f) < current_min_weight_unsat then 
   Precise(f[x=1]);
   update current_min_weight_unsat and I

 consider f reduced for x = 0; 
 if weight_unsat(f) < current_min_weight_unsat then 
   Precise(f[x=0]);
   update current_min_weight_unsat and I

You are welcome to add improvements to this algorithm
but this is not needed. 

Does this algorithm work for any CSP problem captured in
/home/lieber/.www/courses/csu670/f06/hw/2/csp ?