Package edu.neu.ccs.satsolver

Sample use of interface:

See:
Description

Interface Summary

InputInitialI	The first input from the csu team in the first call to the outsourcing team code will be an InputInitialI class instance.
InputUpdateI	After the first input from the csu team, all future calls to the outsourcing team code will be through InputUpdateI class instances.
OutputI	OutputI class instances are returned by the outsourcing team code back to the csu team code as a result of computations.
PairI	The PairI interface is used to encapsulate relation number/fraction pairs.
PolynomialI	The PolynomialI interface manages a polynomial.

Package edu.neu.ccs.satsolver Description

Sample use of interface:

The home team sends an object ii satisfying interface InputInitialI to the outsourcing team. The outsourcing team does not know the internal representation of the object (it could use DemeterJ datastructures) but they know that getPairs returns a set of objects satisfying interface PairI.

The outsourcing team sends back an object satisfying interface OutputI. Again the home team does not know the internal representation the outsourcing team uses but they know that there is a method getMaxBias() to get back the maximum bias. Etc.

For the update case, we use interface InputUpdateI for input to the outsourcing team and again OutputI for output from the outsourcing team.

How to use

The outsourcing team will create a class edu.neu.ccs.satsolver.SATSolverUtil with two methods that the home team will call:

• static OutputI calculateBias(InputInitialI inputInitial) - Given an initial state of relation numbers and fractions, computes the maximum bias.
  Throws a runtime IllegalArgumentException if:
  • the PairI fractions do not add to 1.0, or
  • any PairI relation number outside the range of 0 to 255 inclusive, or
  • any PairI fraction is outside of the range of 0.0 to 1.0 inclusive, or
  • two PairI objects in the set have the same relation number
• static OutputI updateBias(InputUpdateI inputUpdate) - Given a previously generated polynomial, computes an updated maximum bias based on adding and subtracting the given relation numbers and fractions.
  Throws a runtime IllegalArgumentException if:
  • the PairI added fractions do not equal the subtracted fractions (to within some amount), or
  • any PairI relation number is outside the range of 0 to 255 inclusive, or
  • any PairI fraction is outside the range of 0.0 to 1.0 inclusive, or
  • two PairI objects in the set have the same relation number

Because these are static methods, you can use them this way:

  import edu.neu.ccs.satsolver.SATSolverUtil;

  ...

  <in some method>
     ...

     InputInitialI input_initial = new InputInitial( ... );
     OutputI output = SATSolverUtil.calculateBias(input_initial);

     ... do stuffwith output ...  

     InputUpdateI input_update = new InputUpdate( ... )
     OutputI output = SATSolverUtil.updateBias(input_update);  

Relation numbers

Ahmed wrote a Relation module that the outsourcing team is using. The outsourcing code requires that the relation numbers you pass into the outsourcing code are computed the way we're expecting.

The truth table for a relation number is this:

  x2 x1 x0
  -- -- --
1  0  0  0
2  0  0  1
3  0  1  0
4  0  1  1
5  1  0  0
6  1  0  1
7  1  1  0
8  1  1  1

The way to map literals in a constraint to a column of the truth table (also known as "variable number") is this:

  Or( x  y  z )       x = x2, y = x1, z = x0
  Or( x  y )          x = x1, y = x0
  Or( x     z )       x = x1, z = x0
  Or( x )             x = x0
  Or( y )             y = x0

To compute R, you can bitwise-or the magic numbers of the literals.

Example: Given Or( !x y ) we have:

• !x is varnum x1
• y is varnum x0
• the magic number for varnum x1 value 0 is 51
• the magic number for varnum x0 value 1 is 170
• 51 bitwise-or 170 = 187

So the relation number for Or( !x y ) is 187.

For more information

For a more complete specification, refer to: CSU 670 Fall 2006 Project Description and also your email because we'll be making updating the specification based on conversations.