Source Code for Argumentation Projects

This directory contains the following Java source files. While these constitute a full implementation of the Satisfiability Game, a number of modifications should be put in place depending on the specific student project carried out. Such modifications are suggested below.

• BoolString.java

  Defines the class BoolString (an array boolean[]) one of the basic data structures mainipulated in the game realisation.

• CNF_Formula.java

  Class definitions, constructors, and methods for propositional formulae described in CNF. There are 3 Constructors:

  • CNF_Formula(BufferedReader istream)

    Reads a CNF formula from input stream (istream which may be either a file or Standard Input).

  • CNF_Formula(int n, int m, double p, long sv).

    Generates a random CNF formula of n variables and m clauses: the literal x occurs in clause C with probability p/2; the literal -x occurs in clause C with proability p/2.

    Note: The expected length of each clause is p*n. The methods provided in java.util.Random are used with sv specifiying seed value..

  • CNF_Formula(int n, double p, long sv).

    Generate a random 3-CNF formula over n variables. Each of the possible 4*n*(n-1)*(n-2)/3 distinct clauses is included independently with proability p, so that the expected number of clauses in the resulting 3-CNF formula is approximately (4*p/3)*n³

  The class methods are self-explanatory with the exception of public String ntabString(). This constructs a (printable) String that describes the CNF formula in the input form that is used by the ntab Satisfiabilty solver.

• GamePosn.java

  Class definition for the structure indicating data relevant to a move in the game.

• GameRecord.java

  Dynamic (linked list) structure describing the entire course of a game so far. This is (currently) not used (i.e. commented out) in the full implementation, but may be useful in Projects 2 and 5, as a structure to mainipulate.

• PED_NumberIO.java

  Numerical (int and double) input from specified stream. Just saves messing about with `everything on separate line' default for COMP101 I/O.

• SAT_TPI.java

  The full implementation of the Satisfiability Dialogue Game.

  Notes:

  1. This may be configured using a number of different command line options (see code comments for details). status of the CNF formula dealt with. For projects 3 and 4 the statistical data is of more relevance (number of moves made, etc).

  2. The 2 methods
     Select_Attack(boolean[] Possible, CNF_Formula F, GamePosn G) Select_Defence(boolean[] Possible, CNF_Formula F, GamePosn G)

     are central to the length of the Satisfiability Game. Project 3 requires alternative realisations of these to be implemented and evaluated.

In addition this .tar file contains the Propositional Satisfiability Solver developed and distributed by James Crawford, CIRL, The University of Oregon, which provides an excellent basis for the comparative analyses required in Project 4.