Package edu.neu.ccs.satsolver

Sample use of interface:


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:

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:

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.