CSG260 materials

This is a list of materials I've been collecting that are relevant to CSG260 and the things we're doing.

Contents:

1. CSG260 links
2. SAT Solver Interface
3. willg implementation
4. Outsourcing implementation tester
5. Notes on CSP
6. Theo's AspectJ usage doc

Most of these are links to Professor Lieberherr's directory tree.

• format for program output:

  This output format captures the data we want to compare between our individual SAT solver implementations.

  output format

• format for program input:

  There are a couple possible inputs. Ahmed wrote a .cd file which parses the CSP competition input files.

  In class, Daniel suggested we use an input format that's a lot easier to deal with that's based on the SAT competitions. Daniel's format works with DemeterJ, but not with DAJ because it uses a Line terminal which doesn't exist in DAJ.

  Ahmed's input format
  Daniel's input format (sample file)

• all the implementations for the undergrad groups to use:

  Daniel wrote an implementation. I wrote one which doesn't do a lot for input checking. Sam wrote one.

  Daniel's implementation
  Will's implementation
  Sam's implementation

• there are usage transition systems in Professor Lieberherr's project directory:

  usage-transition-system-v1.1.txt is the latest (as of 11/21/2006)

I've been looking for test inputs and looking into ways of generating test inputs. These are links related to that:

• a series of test inputs - I think some of these are the perfect size but as far as I can tell, there aren't any answer keys.
• a Princeton CS302 homework problem set - They talk about generating random inputs by generating graph-coloring problems and converting to CNF. The page also mentions that Wedding Party Seating planning can also be converted to CNF. I'm not sure whether to be excited or sad about that.

Sam and I wrote a verifier program which takes inputs in either the format that Daniel suggested or the format Ahmed created based on CSPXML and an output that we agreed upon and verifies whether the assignment in the output satisfies the formula from the input.

• Version 1.0 - verifier.1.0-install.jar (12/14/2006)

• edu.neu.ccs.satsolver package (jar | javadoc) version 1.1 - November 8, 2006
  Added an explanation for relation numbers, added a section on how to use the SATSolverUtil class methods, added details on which runtime exceptions are thrown and why.
• edu.neu.ccs.satsolver package (jar | javadoc) version 1.0
  

  Note: I need to go through and add some additional information regarding R and how to calculate R given a constraint (including the truth table).

  Note 2: (11/3/2006 8:51pm) This version now has PolynomialI instead of a Set of CoefficientI things.

[Back to the top]

README file in the .jar file explains usage and such. Makefile should build it nicely.

• edu.neu.ccs.satsolver package with my implementation (jar)

[Back to the top]

README file in the .jar file explains usage and such. Makefile should build it nicely. It requires demeterj-0.8.5 rt.jar and someone's implementation.

NOTE: You must unpack the jar in order to run the tester--you cannot run it from the jar. The problem is that DJ can't find class graph nodes. I suspect the issue is that DJ can't look inside jar files for them.

• tester package with tester code in it (jar)

The testfile grammar is like this:

TestFile = <tests> List(Test) .
Test : ComputeBiasTest | UpdateBiasTest common <result> Result .

ComputeBiasTest = "computebiastest" <testname> TestName <pairs> List(Pair) .
UpdateBiasTest = "updatebiastest" <testname> TestName <beforepoly> Polynomial <pairs> List(OPair) .

Pair = <r> Integer ":" <frac> Double .
OPair = <op> Op <r> Integer ":" <frac> Double .
Op : Added | Subtracted .
Added = "+" .
Subtracted = "-" .

Polynomial = "(" <x3> SDouble "," <x2> SDouble "," <x1> SDouble "," <x0> SDouble ")" .
TestName = <s> Ident .

Result = "result" <v> Double <poly> Polynomial .

SDouble : PDouble | NDouble common <v> Double .
PDouble = .
NDouble = "-" .

List(S) ~ S { S } .

If you're interested in adding other test types to the tester, let me know. Given the way it's organized, it shouldn't be that difficult to do.

[Back to the top]

• Version 1.6 (10/19/2006) (minor edits): tex pdf (nice version)
  Made a bunch of corrections based on Professor Lieberherr's suggestions including a rewrite of the Precise algorithm which was wrong in previous versions. Minor note: The PDF version looks awful--I'll recreate it when I get home tonight using the dvipdf on my laptop. Minor note 2: Never mind--I forgot I have dvipdfm on my server so I used that and it looks fine.
• Version 1.5 (10/13/2006) (major edits): tex pdf
  Added a TOC, moved the revision history to a new page, and significantly expanded the sections on MAXMEAN, APPMEAN, and SAT Solvers.
• Version 1.1 (10/10/2006) (minor edits): tex pdf
  Fixed an exponent that was a 5 and should have been an s. Removed a line from one of the itemized lists that was incomplete and shouldn't have been there. Moved the x = k/n to a better place in the APPMEAN explanation.
• Version 1.0 (10/06/2006) (major edits): tex pdf
  Initial writing with changes based on Professor Lieberherr's comments.

[Back to the top]

• CCS_AspectJ_Usage

[Back to the top]