CSG 260 
Fall 2006							Karl Lieberherr

Assignment 1:
Writing simple interpreters

Due: Tuesday, Sep. 19, 2006, beginning of class.
Please hand in a paper copy.

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. an assignment J to the variables.
Output: 
The total weight of the clauses satisfied by J.

Example: 
a or not b or c or not d : 3
and
a or     b or not c      : 4
and
not a                    : 100
      
Assignment: J = a=true, b=c=d=false
The weight is 7.

Find a better assignment that has a higher weight.

Turn in your program and test cases with output.
Turn in a maximum assignment for the above example.


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. An assignment J to the variables.
Output:
The total weight of the equations satisfied by J.

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

Assignment: J = x1=1, x2=x3=x4=0
The weight is 60.

Find a better assignment that has a higher weight.

Turn in your program and test cases with output.
Turn in a maximum assignment for the above example.


Part C:
===============================================================
An important doctrine in software development is to avoid code duplication.
Identify code pieces in the solutions for A and B that are similar and that
could be abstracted out.

Turn in a discussion of the code duplications.

Part D:
===============================================================
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 value v for the variable

Output:
(f v)

Example:
polynomial f = 4 * x^3 + 5 * x^2 + 7
(f 2) = 4 * 8 + 5 * 4 + 7 = 59

Turn in your program and test cases with output.

Part E:
=================================================================
Parts A,B and D are all about writing interpreters for little languages.
Apply the principles about writing interpreters that you learned in
Principles of Programming Languages or in Fundamentals of Computer Science.
Discuss at least one principle or recipe that you applied.

Turn in your discussion. 

Part F:
=====================================================================

Read the survey paper:
The Quest for Efficient Satisfiability Solvers
http://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf

The Quest for Efficient Boolean Satisfiability Solvers, 
by L. Zhang and S. Malik, Invited Paper, 
Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002) 
and also in Proceedings of 14th Conference on Computer Aided Verification (CAV2002), 
Copenhagen, Denmark, July 2002 

The goal of this course is to learn enough about Advanced Software
Development and Satisfiability algorithms so that we can hopefully improve 
the state-of-the-art of Satisfiability Solvers in two ways:
1. Make the algorithms faster so that we win in SAT competitions
2. Make the software organization better so that we can more easily
   maintain the software and adapt it.

Study the following SAT solvers, one in Java and the other in C++.

http://www.sat4j.org/

http://www.sat4j.org/doc/

zchaff from Princeton University (you can also get chaff directly from Princeton)
https://www.ccs.neu.edu/course/csg260/ssl/zchaff/

Let's start with a very modest improvement: Find 2 violations of the Law of Demeter
in the two implementations.
Turn in the violations with an explanation.

Compare with:
http://www.ccs.neu.edu/home/lieber/courses/csu670/f06/coupling-blog/690.aspx.htm

Do you agree with the statement:
Low Coupling Can Cause Unnecessary Complexity?
Turn in your opinion.
==================
General rules:
Your are responsible for choosing suitable data structures,
input formats and algorithms.
Use your programming language of choice. In the lectures we will use Java.

Your algorithms should use computing resources wisely because we want to apply
them later to large problem instances.