//************************************************************
// Main Implementation of SAT-TPI Game from 
// Tech. Report ULCS-02-008:
//************************************************************
// Projects 2-5 will require modification/interacting with
// the implementation given below.
//************************************************************
// Paul E. Dunne
// Dept. of Computer Science
// Univ. of Liverpool
//************************************************************
// Version 1: 20-22/05/2002;
// Version 2: 23-24//05/2002: Retracted sets held in Stack;
//                            Modification of output GamePosn string. 
// Version 3: 27/05/2002:     Input file argument;
//                            GameRecord comment out.
//                            default holds current and last position;
// Version 4: 28/05/2002:     Input flags processing.
// Version 5: 29/05/2002:     Minor changes to command line processing.
// Version 6: 30/05/2002:     Minor changes to SelectAttack,Defence param.
// Version 7: 31/05/2002:     Option to print satisfying assignment.
//************************************************************
// Summary of command line options:
//
//  java SAT_TPI [-c out_file] [-f n p]   [-i in_file] [-n out_file]
//               [-o out_file] [-p ] [-r n m p] [-s seed]    [-S -V] 
//
//    All switches are optional. Input/Output defaults to Standard if
//    none specified. 
//
//  -c Save CNF used in out_file (for use with -r and -f options)
//  -f  Generate random 3-CNF formula of n variables; clause
//      probability p. (Overrides -i and -r)
//  -i  Read CNF formula from file specified by in_file.
//  -n Save CNF in out_file using ntab format for CNF (for use with -r and -f options).
//  -o Send output to out_file.
//  -p Print SAT instantiation if instance satisfiable.
//  -r  Generate random CNF formula of n variables,
//                                     m clauses, 
//                                     probability p.
//      (Overrides -i)
//  -s Specify random seed.
//
//  -S Generate statistics only: (Result/Number of Moves/Number of retractions)
//     (Default: terse output (retractions only and outcome).
//  -V Generate verbose output (full listing of game progress);
//  
//************************************************************
import java.io.*;
import CNF_Formula;
import GamePosn;
import java.util.*;
import BoolString;
import PED_NumberIO;
//************************************************************
// This line should be included if full Game progress is required
// in single data structure. Similalrly all commented lines of
// code marked (++++) in main().
//************************************************************
// import GameRecord;          (++++)
//************************************************************
                    
public class SAT_TPI
  {
  public static FileInputStream   fname;
  public static InputStreamReader input;
  public static BufferedReader    istream;
  public static FileWriter        res_file;
  public static FileWriter        cnf_file;
  public static PrintWriter       ostream1;
  public static PrintWriter       ostream2;
  //************************************************************
  static int Ags;                     // Number of arguments = 2n+m+1
  static int n;                       // Variable count
  static int m;                       // Clause count
  static int PHI;                     // Argument corresponding to F.
  static boolean playable=true;       // Game halts when playable becomes false;
  static boolean C_play = false;      // Flag to record active player.
  static int MoveCount=0;             // Number of moves made so far;
  static int LastAttack;              // Index of Last Clause (1..m) used.
  static int lit;
  static final char Assert='A';
  static final char Counter='C';
  static final char Retract='R';
  //*******************************************************************
  // Supplementary methods used in main():
  //*******************************************************************
  // a) Find_Clauses( GamePosn G, CNF_Formula F, int n, int m)
  //    Identifies the clauses which can be used to attack F given
  //    given the Game progress so far.
  //    returns boolean[]
  //*******************************************************************
  // b) SubSetEq ( boolean[] R, boolean[] S, int y)
  //    returns true if the set indicated by R/{y} is a subset or equal
  //    to the set indicated by S.
  //*******************************************************************
  // c) CheckRetraction (Stack R, boolean[] P, int y, int Ag)
  //    returns true if y can be added to set indicated in P without
  //    committing to a set which has been retracted earlier.
  //*******************************************************************
  // d) Find_Literals( GamePosn G, CNF_Formula F, Stack X, int k, int n, int m)
  //    Identifies the set of literals which can be used to attack
  //    k'th clause, in the context of Game so far.
  //    returns boolean[]
  //*******************************************************************
  // e) Select_Attack( boolean[] Possible, CNF_Formula F, GamePosn G)
  //    Given an indication of the available clauses (identified in (a))
  //    choose 1 of these to continue attack.
  //
  //    NOTE: Current implementation is `naive': one projects involves
  //          investigating more sophisticated selection methods, and thence
  //          requires modifying this method.
  //*******************************************************************
  // f) Select_Defence( boolean[] Possible, CNF_Formula F, i GamePosn G)
  //    Given an indication of the available literal (identified in (d))
  //    choose 1 of these to continue defence.
  //
  //    NOTE: Current implementation is `naive': one projects involves
  //          investigating more sophisticated selection methods, and thence
  //          requires modifying this method.
  //*******************************************************************
  //
  //*******************************************************************
  // Return the set of clauses that are (currently) available to
  // Challenger with which to attack.    
  // if res[k]=true (1<=k<=m) then Ck can be used;
  // if res[0]=false then no avaialble clauses an Challenger has lost
  //*******************************************************************
  public static boolean[] Find_Clauses(GamePosn G,
                                       CNF_Formula F,
                                       int n, int m)
     {
     boolean[] res = new boolean[m+1];
     boolean[] CA = new boolean[2*n+m+2];
     boolean[] CD = new boolean[2*n+m+2];
     int[] clause;
     boolean flag = false;
     boolean is_ok = true;
     CA = G.GetAttack();
     CD = G.GetDefence();
     for (int k=1; k<m+1; k++)
       {
       res[k]=false;
       };
     for (int k=1; k<m+1; k++)
       {
       is_ok = !CA[2*n+k];         // Only use clauses that are not in already.
       clause = new int[n+1];
       clause = F.Get_Ck(k);
       for (int i=1; i<=clause[0]; i++)
         {
         if (clause[i]<0)
           {
           is_ok = (is_ok) && (!CD[n-clause[i]]);   // Negative literal is not in defence;
           }
         else
           {
           is_ok = (is_ok) && (!CD[clause[i]]);     // Positive literal not in defence
           };
         };
       if (is_ok)
         {
         flag=true;                                 // One good clause (at least)
         res[k]=true;
         };
       };
     res[0]=flag;
     return res;
     };
  //****************************************************************
  // Test if the literal subset indicated by R is a subset or equal
  // to the literal subset indexed by S union {y}.
  //****************************************************************
  public static boolean SubSetEq(boolean[] R,
                                 boolean[] S,
                                 int y)
    {
    boolean res=true;         // Until indicated otherwise.
    for (int i=1; i<=2*n; i++)
      {
      if ( (!(i==y)) && (R[i]) && (!S[i]) )
        {
        res=false;    // Found a literal (other than y) in R 
                      // that is not in S, hence R/{y} not a subset of S.
        };
      };
    return res;
    };
  //*****************************************************************
  // Test if the set of literals formed by current defence and y    *
  // have been retracted in an earlier round.                       *
  //                                                                *
  // true is returned if y can be added.                            *
  //*****************************************************************
  public static boolean Check_Retraction(Stack R,
                                         boolean[] P,
                                         int y, int Ag)
    {
    BoolString V;
    BoolString W;
    boolean res = true;
    Stack Save = new Stack();
    boolean [] cret = new boolean[Ag];
    while ((!R.empty())&&(res))
      {
      V = new BoolString(Ag);
      W = new BoolString(Ag);
      V = (BoolString)R.pop();
      W = (BoolString)Save.push(V);
      cret = V.convert();
      res  = !SubSetEq(cret,P,y);
      };
    while (!Save.empty())
      {
      V = new BoolString(Ag);
      W = new BoolString(Ag);
      V = (BoolString)Save.pop();
      W = (BoolString)R.push(V);
      };
    return res;
    };
  //*******************************************************************
  // Return the set of literal that can be used to attack Ck (the clause
  // invoked most recently by the Challenger).
  // The set is held as a 2n+1 element Boolean array:
  //  res[j]=true : (1<=j<=n)  x_j can be used to attack Ck;
  //  res[n+j]=true (1<=j<=n)  -x_j (negation) can be used to attack Ck.
  //  res[0]=false  No available attacks (will force Retract or game lost)
  //**********************************************************************
  public static boolean[] Find_Literals(GamePosn G,
                                        CNF_Formula F,
                                        Stack X,
                                        int k, int n, int m)
     {
     boolean[] res = new boolean[2*n+1];
     boolean[] CD  = new boolean[2*n+m+2];
     int[] clause = new int[n+1];
     boolean flag = false;
     int i;
     Stack Y=new Stack();
     Y=X;
     CD = G.GetDefence();
     clause = F.Get_Ck(k);
     //
     for (i=0; i<2*n+1; i++)
       {
       res[i]=false;
       };
     //************************************************
     // First Check off contradicted literals
     //************************************************
     for (i=1; i<=clause[0]; i++)
        {
        if (clause[i]<0)
          {
          res[n-clause[i]] = !CD[-clause[i]];
          }
        else
          {
          res[clause[i]] = !CD[n+clause[i]];
          };
        };
    //*************************************************************
    // Now remove those literals which would create a retracted set
    //*************************************************************
    for (i=1; i<=2*n; i++)
       {
       if (res[i])
         {
         res[i] = Check_Retraction(X,CD,i,2*n+m+2);
         if (res[i])
           {
           res[0]=true;          
           };
         };
       };
     return res;
    };
  //*******************************************************************
  // The next 2 methods should be customised to explore different     *
  // argument selection strategies.                                   *
  //*******************************************************************
  // Select_Attack: Given a indicator for the possible clauses,       *
  //                choose one of these as the next atttack.          *
  // `Place-holder' implementation: chooose the first available.      *
  //*******************************************************************
  public static int Select_Attack ( boolean[] Possible,
                                   CNF_Formula F, GamePosn G)
   {
   int res=0;
   for (int k=1; k<F.Get_m()+1; k++)
      {
      if ((Possible[k])&&(res==0))
        {
        res = k+2*F.Get_n();          // to get correct index in Attack record.
        };
      };
   return res;
   };
  //*******************************************************************
  // Select_Defence: Given a indicator for the possible literals,     *
  //                choose one of these as the next atttack.          *
  // `Place-holder' implementation: chooose the first available.      *
  //*******************************************************************
  public static int Select_Defence ( boolean[] Possible,
                                    CNF_Formula F,
                                    GamePosn G)
   {
   int res=0;
   for (int k=1; k<=2*F.Get_n(); k++)
      {
      if ((Possible[k])&&(res==0))
        {
        res=k;
        };
      };
   return res;
   };
//***********************************************************************
// Following for debugging not used in code
//***********************************************************************
  public static void Show_Stack(Stack X)
    {
    BoolString V;
    BoolString W;
    Stack Save = new Stack();
    boolean [] cret = new boolean[Ags];
    while ((!X.empty()))
      {
      V = new BoolString(Ags);
      W = new BoolString(Ags);
      V = (BoolString)X.pop();
      W = (BoolString)Save.push(V);
      cret = V.convert();
      for (int i=1; i<=n; i++)
        {
        if (cret[i])
          {
          System.out.print(i+" ");
          };
        if (cret[n+i])
          {
          System.out.print("-"+i+" ");
          };
        };
      System.out.println();            
      };
    while (!Save.empty())
      {
      V = new BoolString(Ags);
      W = new BoolString(Ags);
      V = (BoolString)Save.pop();
      W = (BoolString)X.push(V);
      };
   };
        
  //*******************************************************************
  public static void main( String[] args ) throws IOException
    {
    CNF_Formula F;
    GamePosn Current;
    GamePosn Last;
    Stack R;                // Linked list of retracted committment sets;
    Stack temp;  
    BoolString TOS;
    boolean[]  P;                // Array of current defence committments;
    boolean[]  Q;                // Array of current attacks
    boolean[]  B;                // Temprary structure for Retract sets.
    BoolString T;
    boolean[]  Cset;             // Array of available clauses for Challenger
    boolean[]  Lset;             // Array of available literals for Defence.
    double     p=0.5;            // Although should be overridden if used.
    long       sval=0;           // Default seed value.
    //***********************************************************************
    // Command Line flags
    //***********************************************************************
    boolean inset=false;         // Named input file
    boolean out1=false;          // Named result file.
    boolean out2=false;          // Named output CNF file (standard form)
    boolean three_cnf=false;     // Random 3-CNF
    boolean cnf=false;           // Random CNF
    boolean ntab=false;          // ntab format to save (random) CNF
    boolean verbose=false;       // Generate verbose record of game.
    boolean stats=false;         // Output Stats only.
    boolean seeded=false;        // Random seed flag.
    boolean terse=true;
    boolean show_sat =false;    
    boolean bad_opt=false;       // Unrecognised option flag.
    int ct,inarg;
//*******************************************************************
//  GameRecord G;               (++++)
//*******************************************************************
    ct = args.length;
    inarg = 0;
    if (args.length==0)
      {
      input = new InputStreamReader(System.in);
      ostream1 = new PrintWriter(System.out,true);
      ostream2 = new PrintWriter(System.out,true);
      inset=true; out1=true; out2=true;
      }
    else
      {
      //*********************************************
      // Process command line options 
      // (echoed to System.out: 
      //  diagnostics purposes commented out)
      //*********************************************
      while ((inarg < ct)&&(!bad_opt))
        {
        switch(args[inarg].charAt(1))
          {
          case 'i': fname = new FileInputStream(args[inarg+1]);
                    input = new InputStreamReader(fname);    
                    inset = true;
                    // System.out.println("Input file: "+args[inarg+1]);
                    inarg=inarg+2; break;
          case 'r': cnf=true; inset=false;
                    n=(new Integer(args[inarg+1])).intValue();
                    m=(new Integer(args[inarg+2])).intValue();
                    p=(new Double(args[inarg+3])).doubleValue();
                    // System.out.println("CNF set "+n+" "+m+" "+p);
                    inarg=inarg+4; break;
          case 'f': three_cnf=true;inset=false;
                    n=(new Integer(args[inarg+1])).intValue();
                    p=(new Double(args[inarg+2])).doubleValue();
                    // System.out.println("3CNF set "+n+" "+p);
                    inarg=inarg+3; break;
          case 'V': verbose=true; terse=false;
                    // System.out.println("Verbose set");
                    inarg=inarg+1; break;
          case 'S': stats=true; terse=false;
                    // System.out.println("Stats set");
                    inarg=inarg+1; break;
          case 'o': res_file = new FileWriter(args[inarg+1]);
                    ostream1 = new PrintWriter(res_file);
                    // System.out.println("Outfile 1: "+args[inarg+1]);
                    out1=true; inarg=inarg+2; break;
          case 'c': cnf_file = new FileWriter(args[inarg+1]);
                    // System.out.println("Outfile 2 (CNF): "+args[inarg+1]);
                    ostream2 = new PrintWriter(cnf_file);
                    out2=true; inarg=inarg+2;; break;
          case 'n': cnf_file = new FileWriter(args[inarg+1]);
                    // System.out.println("Outfile 2 (ntab): "+args[inarg+1]);
                    ostream2 = new PrintWriter(cnf_file);
                    out2=true; ntab=true; inarg=inarg+2; break;
          case 'p': show_sat=true; inarg++; break;
          case 's': sval = (new Long(args[inarg+1])).longValue();
                    inarg=inarg+2; seeded=true; break;
          default:  System.out.println("Option "+args[inarg]+" not recognised");
                    System.out.println("Summary of command line options: ");
                    System.out.println("  -c Save CNF used in out_file");
                    System.out.println("  -f  Generate random 3-CNF formula");
                    System.out.println("  -i  Read CNF formula from file specified by in_file.");
                    System.out.println("  -n Save CNF in out_file using ntab format for CNF.");
                    System.out.println("  -o Send output to out_file.");
                    System.out.println("  -p Print SAT instantiation if instance satisfiable.");
                    System.out.println("  -r  Generate random CNF formula");
                    System.out.println("  -s Random seed setting");
                    System.out.println("  -S Generate statistics only");
                    System.out.println("  -V Generate verbose output");
                    bad_opt=true;
          };
        };
      };
    if (!bad_opt)
    {
    if (!out1)
      ostream1 = new PrintWriter(System.out,true);
    if (!out2)
      ostream2 = new PrintWriter(System.out,true);
    if (!inset)
      input = new InputStreamReader(System.in);
    istream = new BufferedReader(input);

    //*****************************************************************
    // Initiation Stages                                              *
    //*****************************************************************
    if ( (!three_cnf) && (!cnf) )
      F = new CNF_Formula(istream);
    else
      if (three_cnf)
        F = new CNF_Formula(n,p,sval);
      else
        F = new CNF_Formula(n,m,p,sval);
    if (ntab)
      {
      ostream2.println(F.ntabString());
      if (out2) ostream2.close();
      }
    else
      {
      ostream2.println(F.toString());
      if ((!(args.length==0))&&(out2)) ostream2.close();
      };
    n = F.Get_n();
    m = F.Get_m();
    Ags = 2*n+m+2;                      // 1 more than needed: saves faffing about
                                        // with indexing from 0.
    PHI=2*n+m+1;
    P = new boolean[Ags];
    Q = new boolean[Ags];
    B = new boolean[Ags];
    Cset = new boolean[m+1];
    Lset = new boolean[2*n+1];
    for (int i=0; i<Ags; i++)
      {
      P[i]=false; Q[i]=false;
      };
    R = new Stack();
    Last = new GamePosn(n,m);
    Current = new GamePosn(n,m);
    Current.SetMoveNumber(MoveCount);
    Current.SetMoveMade(Assert);
    Current.SetArg(PHI);
    Current.SetDefence(P);
    Current.SetAttack(Q);
//*******************************************************************
//  G = new GameRecord();              (++++)
//  G.AddHead(Current);                (++++)
//*******************************************************************
    if (verbose)
      ostream1.println(Current.toString());
    while (playable)
      {
      Last = new GamePosn(n,m);
//*******************************************************************
//    Last = G.GetHead();              (++++)
//*******************************************************************
      Last = Current;                  // Comment out if (++++) lines in.
      Current = new GamePosn(n,m);
      MoveCount++;
      C_play = !C_play;            // Flip active player flag;
      //*****************************************************
      // Challenger's move                                  *
      //*****************************************************
      if (C_play)             
        {
        Cset = Find_Clauses(Last,F,n,m);
        //****************************************************
        // Use Cset[0] as indicator for any clauses avaialble
        //****************************************************
        if (!Cset[0])
          {
          playable = false;   // Game Over : Challenger loses
          }
        else
          {
          Current.SetMoveMade(Counter);
          Current.SetMoveNumber(MoveCount);
          Current.SetDefence(P);
          LastAttack = Select_Attack(Cset,F,Last);
          Q[LastAttack] = true;
          Current.SetAttack(Q);
          Current.SetArg(LastAttack);
//*******************************************************************
//        G.AddHead(Current);          (++++)
//*******************************************************************
          };
        }
      //***************************************************
      // Defender's Move                                  *
      //***************************************************
      else
        {
        Lset = Find_Literals(Last,F,R,LastAttack-2*n,n,m);
        if (!Lset[0])
          // Retraction forced or Game Lost by Defender.
          {       
          if (!P[0])
            // Defender has nothing to retract: Game Lost
            {
            playable = false; // Game Over;
            }
          else
            {
            Current.SetRetract(P);
            B = new boolean[Ags];
            for (int i=1; i<Ags; i++)
              {
              B[i]=P[i];
              };
            T = new BoolString(B,Ags);
            TOS = new BoolString(Ags);
            TOS = (BoolString) R.push(T);               // Record the retracted set;
            Current.SetMoveNumber(MoveCount);
            Current.SetMoveMade(Retract);
            for (int i=0; i<Ags; i++)
              {
              Q[i]=false; P[i]=false;
              };
            Current.SetDefence(P);
            Current.SetAttack(Q);
            Current.SetArg(0);          // Although it's never used.
//*******************************************************************
//          G.AddHead(Current);         (++++)
//*******************************************************************
            };
          }
        //*************************************************
        // At least one literal available.
        //*************************************************
        else
          {
          lit = Select_Defence(Lset,F,Last);
          P[0]=true;                   // Now committed to something.
          P[lit]=true;                 // Record the active attack;
          Current.SetMoveNumber(MoveCount);
          Current.SetMoveMade(Counter);
          Current.SetArg(lit);
          Current.SetDefence(P);
          Current.SetAttack(Q);
//*******************************************************************
//          G.AddHead(Current);         (++++)
//*******************************************************************
          };
        };
        if (playable)
          {
          if (!stats)
            {
            if ((verbose) || ((terse)&&(Current.GetMoveMade()==Retract)) )
               ostream1.println(Current.toString());         
            };
          };
       };
    if (C_play)
      {
      ostream1.print("SAT ");
      if (show_sat)
        {
        P = new boolean[Ags];
        P=Last.GetDefence();
        for (int i=1; i<=n; i++)
          {
          if (P[i])
            ostream1.print(i+" ");
          if (P[n+i])
            ostream1.print("-"+i+" ");
          };
        ostream1.println();
        };
      }
    else
      {
      ostream1.print("UNSAT ");
      };
    ostream1.print(MoveCount+" ");
    ostream1.println(R.size());
    ostream1.close();
    };
    };
  }