//
// COMP114
// Example 4:  2-CNF Class
//              
// Paul E. Dunne 24/11/2010
//
import java.util.*;
public class CNF2
  {
  private int n;   // Number of Boolean variables in instance
  private int steps;  // Number of steps needed to determine satisfiable/unsatisfiable
  private boolean satis;  // Record whether 2-cnf is satisfiable or unsatisfiable
  private Random RandomSequence;  // Used in generating sequence of n-variable random 2-CNFs
  //*******************************************************************************************
  // The following are used in the satisfiability testing method and 
  // are not (and do not need to be) publicly accessible.
  // *************************************************************************************************
  private boolean[][] FormGraph; // Directed graph representation of Formula
  private boolean[][] ClauseSet; // Boolean representation of clause set
  private int[][] AList;         // Adjacency list form of directed graph
  private boolean[] visited;     // Control for satisfiabilty test
  //*********************************************************************//
  // Constructor
  // 2CNF representation: 0<=i<=n-1 corresponds to variable x_i
  //                      n<=i<=2n-1 is variable ¬x_{n-i}
  // so that clause {x_i,x_j} marked by ClauseSet[i][j]=ClauseSet[j][i]=T
  //                {x_i,¬x_j}  ClauseSet[i][n+j]=ClauseSet[n+j][i]=T
  //                {¬x_i,¬x_j} ClauseSet[n+i][n+j]=ClauseSet[n+j][n+i]=T
  // Always have CLauseSet[i][i]=ClauseSet[i][n+i]=ClauseSet[n+i][i]=F
  // ********************************************************************//
  public CNF2(int size)
     {
     n=size;
     FormGraph = new boolean[2*n][2*n];
     ClauseSet = new boolean[2*n][2*n];
     AList = new int[2*n][2*n];
     visited = new boolean[2*n];
     RandomSequence = new Random();
     };
  //********************************************************************//
  // Instance Methods                                                   //
  // *******************************************************************//
  //
  //********************************************************************//
  // The following two methods are employed in the 2-CNF satisfiabilty  //
  // testing algorithm. The details are not required to be public types //
  //
  // *******************************************************************//
  // Converts Matrix representation to Adjacency list.                  //
  // *******************************************************************//
  private void FormAList()
    {
    int i,j;
    for (i=0; i<2*n; i++)
      {
      AList[i][0]=0;
      for (j=0; j<2*n; j++)
        {
        if (FormGraph[i][j])
          {
          AList[i][0]++;
          AList[i][AList[i][0]]=j;
          }
        };
      };
    };
   //************************************************************************
   //  Report if there is a directed path from s to t in Formula graph      *
   //************************************************************************ 
   private boolean stpath(int s, int t)
     {
     int i,add,ct;
     boolean found=false;
     ct=1;
     while ((!found)&&(ct<=AList[s][0]))
       {
       steps++;
       visited[s]=true;
       if (!visited[AList[s][ct]])
        {
        if (AList[s][ct]==t)
          found=true;
        else
          found = stpath(AList[s][ct],t);
        };
        ct++;
       };
     return (found);
     };
   //************************************************************************ 
   // 2-CNF satisfiabilty testing Algorithm (sets value of the field satis for an instance)
   // Method uses the following:
   // F(X) is satisfiable if and only if
   // the (directed) graph FormGraph(F) as described above is such that for *every* x in X
   // EITHER: there is no directed path from x to ¬x
   //    OR:  there is no directed path from ¬x to x
   //************************************************************************ 
   // From:
   // Aspvall, B.; Plass, M. F.; and Tarjan, R. E. 1979. 
   // A linear-time algorithm for testing the truth of certain
   // quantified Boolean formulas. 
   // Information Processing Letters 8(3):121-123.
   //************************************************************************ 
   public void SatTest()
     {
     int i,j;
     boolean open =false;   // Don't know the answer yet
     steps=0;               // Reset step counter
     i=0;
     while ((i<n)&&(!open))  // Exit when discovered two paths needed, i.e. don't test remaining variables
                             // since there's no point in doing so.
       {
       for (j=0; j<2*n; j++) visited[j]=false;
       open = stpath(i,n+i);
       if (open)
         {
         for (j=0; j<2*n; j++) visited[j]=false;
         open= (open)&&(stpath(n+i,i));
         };
       i++;
       };
     satis=(i==n);           // Tested every variable and no pair of paths found - F is satisfiable
     };
  // *******************************************************************//
  // Generate next Random 2-CNF of n variables:                         //
  // *******************************************************************//
  public void nextRandomCNF(double cp)
    {
    int i;
    int j;
    for (i=0; i<2*n; i++)
      for (j=0; j<2*n; j++)
        {
        FormGraph[i][j]=false;
        ClauseSet[i][j]=false;     // Clear Previous Setting
        };
    for (i=0; i<2*n; i++)
      for (j=i+1; j<2*n; j++)
        {
        if (!(j==(i+n)))
          {
          ClauseSet[i][j] = (RandomSequence.nextDouble()<=cp);  // Each of 2n(n-1) possible clauses present independently
                                                       // with probability p.
          ClauseSet[j][i] = ClauseSet[i][j];           // Symmetric structure.
          };
        //**************************************************************************************
        // Build Formula Graph at same time
        // if {x_i,x_j} is a clause then (¬x_i,x_j) and (¬x_j,x_i) are directed edges, i.e.
        //                               Formgraph[n+i][j]=FormGraph[n+j][i]=T
        //    {x_i,¬x_j} then (¬x_i,¬x_j) and (x_j,x_i) are directed edges, i.e
        //                                 FormGraph[n+i][n+j]=Formgraph[j][i]=T
        //    {¬x_i,x_j} then (x_i,x_j) and (¬x_j,¬x_i) are directed edges, i.e
        //                                 FormGraph[i][j]=Formgraph[n+j][n+i]=T
        //    {¬x_i,¬x_j} then (x_i,¬x_j) and (x_j,¬x_i) are directed edges, i.e
        //                                FormGraph[i][n+j]=FormGraph[j][n+i]=T
        //**********************************************************************************
        if (ClauseSet[i][j])
          {
          if ((i<n)&&(j<n))
            {
            FormGraph[n+i][j]=true; FormGraph[n+j][i]=true;
            }
          else if ((i<n)&&(j>=n))
            {
            FormGraph[n+i][j]=true; FormGraph[j-n][i]=true;
            }
          else if ((i>=n)&&(j>=n))
            {
            FormGraph[i-n][j]=true; FormGraph[j-n][i]=true;
            };
            // NB Do not need explicit test of (i>=n)&&(j<n) since already included this case
            // and loop control guarantees j>i in all cases
           };
        };
        FormAList();
    };
   //*********************************************************************************************
   public boolean IsSat()
     {
     return satis;
     };
   public int StepCount()
     {
     return steps;
     };
   // *********************************************************************************************
}