import java.io.*;
import java.util.*;
import PED_NumberIO;
//******************************************************
//  CNF_Formula class used in SAT_TPI Game Implementation
//****************************************************
//  Paul E. Dunne 
//  Dept. of Computer Science
//  Univ. of Liverpool
//****************************************************
// Version 1: 22/05/2002
// Version 2: 27/05/2002  Additional Constructors for random data
//                        generation;
// Version 3: 29/05/2002  Random sequences implemented via 
//                        java.util.Random class.
//****************************************************
// CNF Formula specified in the form
//
//   n     +ve integer giving number of variables
//   m     +ve integer giving number of clauses;
//   m lines of form
//   C-len y_1 y_2 ... y_clen
//   C_len +ve integer <= n
//    y_i integers indicating literal in clause 
//        (+/- according to whether related variable is 
//         positive or negated).
//******************************************************
class CNF_Formula
  {
  //**********************************************************************
  private int n;  // Number of variables in this instance.
  private int m;  // Number of clauses in this instance.
  private int[][] PHI;  // The CNF formula m clauses of (at most) n literals
                        // PHI[k][] the k'th clause PHI[k][0] 
                        // always give clause length
  //**********************************************************************
  // Constructor which Reads CNF defined in form
  // above from input file or Standard input.
  //**********************************************************************
  public CNF_Formula(BufferedReader istream) throws IOException
    {
    n = PED_NumberIO.get_int(istream);  // Variables
    m = PED_NumberIO.get_int(istream);  // Clauses
    PHI = new int[m+1][n+1];                  // So that can index from 1..m,1..n
    for (int i=1; i<m+1; i++)
      {
      PHI[i][0] = PED_NumberIO.get_int(istream);  // Length of i'th clause
      for (int j=1; j<=PHI[i][0]; j++)
         {
         PHI[i][j] = PED_NumberIO.get_int(istream);  // Literal
         };
      };
     };
  //**********************************************************************
  // Constructor to generate v variable, c-clause CNF:
  // Variable x occurs in a clause with probability p; +/- chosen with
  // equal probabilty. Thus expected clause length is p*v.
  //**********************************************************************
  public CNF_Formula(int v, int c, double p, long sv)
    {
    Random seq;
    int ct=0;
    n=v; m=c;
    if (sv==0)
      seq=new Random();
    else
      seq = new Random(sv);
    PHI=new int[m+1][n+1];
    for (int i=1; i<=m; i++)
      {
      ct=0;
      for (int j=1; j<=n; j++)
        {
        if (seq.nextDouble()<p)
          {
          ct++;
          if (seq.nextDouble()>0.5)
            {
            PHI[i][ct] = j;
            }
          else
            {
            PHI[i][ct] = -j;
            };
          };
        };
      PHI[i][0]=ct;
      };
    };          
  //**********************************************************************
  // Constructor to generate v variable 3-CNF:
  // Each of the possible 8(v choose 3) clauses is included u.a.r.
  // with probability p. Thus expected number of clauses is ~ 8pv^3
  //**********************************************************************
  public CNF_Formula(int v, double p, long sv)
    {
    Random seq;
    int ctr=0;
    int[][] temp = new int[1+(4*v*(v-1)*(v-2))/3][4];
    if (sv==0)
      seq=new Random();
    else
      seq = new Random(sv);
    n=v;
    for (int pol=0; pol<8; pol++)
      {
      for (int i=1; i<=n-2; i++)
        {
        for (int j=i+1; j<=n-1; j++)
          {
          for (int k=j+1; k<=n; k++)
            {
            if (seq.nextDouble()<p)
              {
              ctr++;
              switch(pol)
                {
                case 0: temp[ctr][1]=-i; temp[ctr][2]=-j; temp[ctr][3]=-k; break;
                case 1: temp[ctr][1]=-i; temp[ctr][2]=-j; temp[ctr][3]=k; break;
                case 2: temp[ctr][1]=-i; temp[ctr][2]=j; temp[ctr][3]=-k; break;
                case 3: temp[ctr][1]=-i; temp[ctr][2]=j; temp[ctr][3]=k; break;
                case 4: temp[ctr][1]=i; temp[ctr][2]=-j; temp[ctr][3]=-k; break;
                case 5: temp[ctr][1]=i; temp[ctr][2]=-j; temp[ctr][3]=k; break;
                case 6: temp[ctr][1]=i; temp[ctr][2]=j; temp[ctr][3]=-k; break;
                case 7: temp[ctr][1]=i; temp[ctr][2]=j; temp[ctr][3]=k;
                };
              };
            };
          };
        };
      };
      m=ctr;
      PHI = new int[m+1][n+1];
      for (int i=1; i<=m; i++)
        {
        PHI[i][0]=3;
        for (int j=1; j<=3; j++)
          {
          PHI[i][j]=temp[i][j];
          };
        };
    };
  //******************************************************************
  // Instance Methods
  //******************************************************************
  public int Get_n()
    {
    return n;                // Return number of variables in instance.
    };
  public int Get_m()
    {
    return m;               // Number of clauses in instance
    };
  public int[] Get_Ck(int k)
    {
    return PHI[k];          // Array defining literals in k'th clause.
    };
  //******************************************************************
  // Convert to String for output;
  //******************************************************************
  public String toString()
    {
    String res = new String();
    res=res+n+"\n"+m+"\n";
    for (int i=1; i<=m; i++)
      {
      for (int j=0; j<=PHI[i][0]; j++)
        {
        res = res+PHI[i][j]+" ";
        };
      res=res+"\n";
      };
    return res;
    };
  //******************************************************************
  // Convert to String for ntab SAT input form;
  //******************************************************************
  public String ntabString()
    {
    String res = new String();
    for (int i=1; i<=m; i++)
      {
      if (PHI[i][0]==0)
        {
        res=res+"-1"+"\n"+"1";      // Fudge because ntab does not treat
                                    // empty input line as empty clause.
        }
      else
        {
        for (int j=1; j<=PHI[i][0]; j++)
          {
          res = res+PHI[i][j]+" ";
          };
        };
      res=res+"\n";
      };
    return res;
    };
  }