CSG 260 
Fall 2006							Karl Lieberherr

Assignment 2:
Formula Reductions

In order to implement optimization algorithms for 
maximum satisfiability, we need to implement reduction algorithms:
given a set of constraints and a variable assignment to one of the variables,
we need to construct a reduced set of constraints.


Part A:
=========================================================

Write a program that solves:

Input: 
1. a propositional logic conjunctive normal form  where
each clause has a positive real weight and 
2. a variable x and an assignment to the variable x.
Output: 
The reduced conjunctive normal form where x has been
eliminated.

Example: 
a or not b or c or not d : 3
and
a or     b or not c      : 4
and
not a                    : 100
      
c = true

Reduced constraints:

true 			: 3
and
a or     b      	: 4
and
not a                   : 100
      
A second reduction step:

a = false

Reduced constraints:

true 			: 3
and
b      			: 4
and
true                    : 100
      
Turn in your program and test cases with output.


Part B:
===========================================================
Write a program that solves:

Input:
1. a system of equations of the form x1+x2+x3=1 where 
   each equation has a positive real weight.
   The variables in the equations only assume values 0 and 1. + is ordinary addition.
2. A variable x and an assignment to the variable.
Output:
The reduced system of equations where x has been eliminated.

Example:
x1 + x2 + x3      = 1 : 20
x1 + x2 +    + x4 = 1 : 20
x1 +      x3 + x4 = 1 : 20
     x2 + x3 + x4 = 1 : 100

x1 = 1

Reduced constraints:

x2 + x3      = 0 : 20
x2 +    + x4 = 0 : 20
     x3 + x4 = 0 : 20
x2 + x3 + x4 = 1 : 100

A second reduction step:

x2 = 1

false 		: 20
false  		: 20
x3 + x4 = 0 	: 20
x3 + x4 = 0 	: 100

Note that part A and B are again similar try to abstract out the commonalities.

Turn in your program and test cases with output.

Part C:
===============================================================
In the future we want to implement an optimization program that 
finds an assignment of maximum weight or close to maximum weight.

To implement the optimization program, we will need the following
subroutine:

Input:
1. a polynomial 
(lambda x (f x)) 
in one variable with real coefficients.
2. a positive integer n

Output:
The maximum value of (f k) for k ranging over the integer values from 0 to n
and a k for which the maximum is reached.

Example:
polynomial f = x *(x-4)
n = 4
The maximum is reached for x = 2.

Turn in your program and test cases with output.

Part D:
=====================================================================

====================
For this homework you are encouraged to use DemeterJ and DJ for implementation.