/**
 * Multithreaded SAT solver
 *
 * @author Danielle Eckard and Dr. Lobo
 * @version 2008.01.17
 *
 * Modification Log:
 * 4. 2008/05/12 New version of splitHelper method with 2-sided-JW-style var selection
 * 3. 2008/04/20 Updated Documentation
 * 2. Changed workCompleted() method
 * 1. 2008/02/25 Added the split and split helper method
 * 0. Created 2008/Jan by Andrea Lobo (AL) and Danielle Socha (DS)
 *
 */
import java.util.*;
import java.io.*;
import java.io.FileNotFoundException;

public class Msat {
    Map<Long,Solver> solvers; // maps solverId to solver
                              //(threadId to thread)

    // List<Formula> problems; // possible future use

    private int numSubProb = 16; // default number of subproblems
    final static int NoAssignment = -1; // named const for no assignment left

    Formula formula;
    boolean solved;

    // keep track of the subproblems
    HashSet<SubProblem> needSolving; // Assignments that need solving
                                 // (have not been assigned yet).
    HashSet<SubProblem> inProgress; // Assignments that have been
                                 //assigned to solvers.
    // Assignments that have been solved are removed.
    private long startTime;  // start time used for performance studies
    private long endTime;    // end time used for performance studies
    private int progressCounter = 0;  // compared to number of subproblems
    	

    /**
     * Constructor for Msat
     *
     * @param numProcessors the number of processors
     */
    public Msat ( int numProcessors ) {

        // Create the thread pool
        solvers = new HashMap<Long,Solver> ( );
        for (int i = 0; i < numProcessors; i++) {

            Solver solver = new Solver ( this );
            solvers.put ( solver.getId(), solver );

        }

        // problems = new LinkedList<Formula> ( ); // possible future use

        // create the subproblems
        needSolving = new HashSet<SubProblem> ( );
        //for (int i = 0; i < (int) Math.pow(2, NumVars); i++ )
        //needSolving.add ( i );
        inProgress = new HashSet<SubProblem> ( );
        solved = false;
    }

    /**
     * Constructor for Msat
     *
     * @param numProcessors the number of processors
     * @param filename the file that contains the formula
     */
    public Msat ( int numProcessors, String filename ) throws FileNotFoundException 
    {

    	// Create the thread pool
        solvers = new HashMap<Long,Solver> ( );
        for (int i = 0; i < numProcessors; i++) {

            Solver solver = new Solver ( this );
            solvers.put ( solver.getId(), solver );

        }

        // problems = new LinkedList<Formula> ( ); // possible future use

        // create the subproblems
        needSolving = new HashSet<SubProblem> ( );
        //for (int i = 0; i < (int) Math.pow(2, NumVars); i++ )
        //needSolving.add ( i );
        inProgress = new HashSet<SubProblem> ( );
        solved = false;

        formula = new Formula (filename);

    }

    /**
     * Sets the formula
     *
     * @param formula the formula
     */
    public void setFormula ( Formula formula ) {
        solved = false;
        this.formula = formula;
        //for (Solver solver: solvers.values())
        //solver.setFormula(formula);

    }

    /**
     * Returns the formula
     *
     * @return formula
     */
    public Formula getFormula()
    {
    	return formula;
    }

    /**
     * Sets the number of subproblems
     *
     * @param n the number of subproblems
     */
    public void setNumSubProb ( int n ) {
        if (n > 0)
        	numSubProb = n;
        else
        	System.out.println ("number of subproblems is unchanged; can not be < 0");
    }

    /**
     * When a solver is completed solving a subproblem, it removes the subproblem
     * from the list of subproblems that are in progress, prints out that the
     * thread has completed its task and also the outcome of the threads task
     * (whether a satisfying assignment was found).
     *
     *
     * @param solver the current solver that has completed its task
     */
    synchronized public void workCompleted ( Solver solver ) {

        progressCounter++;
	assert ( inProgress.contains(solver.getAssignment ( )));
        inProgress.remove(solver.getAssignment());

        //System.out.println ("Thread " + solver.getId() + " completed it's task, Msat's " + 
	//                       progressCounter + " -th subproblem" );
        if (! solver.getAnswer ( ).equals("")) {
            // Stub: Inform all threads
            // Stub: Expand on function interface
           // System.out.println ( solver.getAnswer());
        	System.out.println("Satisfiable");
		endTime = System.nanoTime();
		System.out.println(endTime - startTime + " nanoseconds");
/* deprecated...
	    //stop threads since satisfying assignment found
	    for (Solver solver2: solvers.values())
            	solver2.stop();
*/
            solved = true;
            //System.out.println(solver.getAssignment());
        }
        else {
	    if(progressCounter == numSubProb)
	    {
		endTime = System.nanoTime();
		System.out.println("unsatisfiable");
		System.out.println("progressCounter=" + progressCounter + 
                                   " numSubProb= " + numSubProb);

		System.out.println(endTime - startTime + " nanoseconds");
	    }
        }
    }

    /**
     * Calls the split method to split the formula and then starts the solvers
     *
     */
    synchronized public void solve ( ) {

        startTime = System.nanoTime();
	System.out.println("before numSubProb =  " + numSubProb);
	needSolving = split(formula);
	System.out.println("after numSubProb =  " + numSubProb);
	System.out.println("*** we need to solve " + needSolving.size() + " problems");
      
        for (Solver solver: solvers.values())
            solver.start();

    }

    /**
     * Returns the next subproblem that needs to be solved if one exists and
     * removes the subproblem from the list of subproblems that needs solving
     *
     * @return Subproblem subproblem in the form of a partial assignment that needs to be solved
     */
    synchronized public SubProblem getSubProblem ( ) {

        if (needSolving.isEmpty() || solved)
            return null;
        else {

            SubProblem assignment = needSolving.iterator().next();
            needSolving.remove(assignment);
            return assignment;
        } // end else

    } // end getSubproblem

/*  // 2008 Jan version
    // splits a complete problem into numSubProb subproblems
    // ??? future version may want to receive a subproblem as a parameter
    public HashSet <SubProblem> split(Formula f)
    {
        HashSet<SubProblem> answer = new HashSet <SubProblem>();
        int numPresetVars = (int) Math.sqrt(numSubProb); // ??? what if not power of 2
        PartialAssignmentGen partialAssignmentGen =
        	                 new PartialAssignmentGen(f.getNumVars(), numPresetVars);
        for( int i = 0; i < numSubProb; i++)
        {
            answer.add (new SubProblem(f, partialAssignmentGen.getNext()));
        }
        return answer;
    }
*/

    /**
     * Splits a complete problem into numSubProb subproblems
     * 
     * @param f the formula that needs to be split
     * @return a set of subproblems that need solving
     */
    public HashSet <SubProblem> split(Formula f)
    {
        HashSet<SubProblem> answer = new HashSet <SubProblem>();

        int numPresetVars; // number of binary variables that will be preset in the subproblems
        numPresetVars = (int) ( Math.log(numSubProb) / Math.log(2)); // log base 2 of numSubProb
        // adjust numPresetVars when numSubProb is not a power of 2
        if ( (Math.abs(numSubProb - Math.pow (2, numPresetVars)) > 0.0001 ))
         	numPresetVars ++;

        if (numPresetVars > f.getNumVars())
        {
        	System.out.println ("You can't split this problem into " + numSubProb
        			            + " subproblems.");
        	return null;
        } // end if
        else
        {
          SubProblem s = new SubProblem (f, new Assignment (f.getNumVars()));
          List <SubProblem> list = splitHelper (s, numSubProb, numPresetVars);
          //copy list into answer
          for( SubProblem subProblem : list)
              answer.add (subProblem);
        } // end else

        return answer;
    } // end split 



     /** 
     * Takes a subproblem and returns a list of the subproblem split further into
     * the specified amount of subproblems (numSubProb). Uses chooseSplitVars.
     *
     * @param s the subproblem to be split
     * @param numSubProb the number of subproblems desired, currently disregarded
     * @param numSplitVars the number of additional variables that will be set in each subproblem 
     */
    private List <SubProblem> splitHelper(SubProblem s, int numSubProb, int numSplitVars)
    {
    	List <SubProblem> answer = new LinkedList <SubProblem> ();
    	answer.add(s);
    	if (numSubProb == 1)
    	{
    		answer.add(s);
		return answer;
    	}
    	else
    	{
                int [] splitVars = chooseSplitVars (s.getAssignment(), s.getFormula(), numSplitVars);
    		System.out.println("numSplitVars=" + numSplitVars + " and splitVars.length=" +
                                    splitVars.length );
                
    		for (int v =0; v < splitVars.length; v++)
		{
    			List <SubProblem> tmp = new LinkedList <SubProblem> ();
			
    			for( SubProblem s1 : answer)
                        {
    				//System.out.println(splitVars[v]);
				SubProblem s2 = new SubProblem (s1);
    				s1.getAssignment().assignVar(splitVars[v], 1);
	    			s2.getAssignment().assignVar(splitVars[v], 0);
				//System.out.println(s1);
				//System.out.println(s2);
    		              	tmp.add (s2);
                        }

    			for( SubProblem subP : tmp)
    	              	    answer.add (subP);

		} // for 

    		return answer;
    	} // end else
    } // end splitHelper


   /**
   * Returns the list of variables that will be used to split the problem.
   * Currently uses a variant of the two-sided JW heuristic weights.
   *
   * @param partial the current partial assignment.
   * @param f the formula
   * @param n the number of variables to choose
   *
   * @return a array of integers initialized with n variable identifiers
   */
   private int[] chooseSplitVars (Assignment partial, Formula f, int n)
   {
      double max = 0; // max in occur
      int next = 0; //index of max
      f.setOccurred(partial); //Updates occurrences
      double [] occur = f.getOccurrences(); // 2-sided JW-style weights 
                                            // for all literals in f
      Vector <Integer> assign = partial.getAssignment();
      int [] answer = new int [n]; 

      for (int numVarsFound = 0; numVarsFound < n; numVarsFound++)
      {
        // find the next var with the highest weight and store it in answer

        // find the max in occur
        max = occur[0];
        next = 0;
       	for (int i=1; i<occur.length; i++)
        {
           if (occur[i] > max)
           {
                max = occur[i];
                next = i;
           }
        }

        // obtain the variable id from the literal's index.
        // the weights are stored such that:
        // the weight for literal x_i is at index (i-1) * 2 
        // and
        // the weight for literal not-(x_i) is at index ((i-1) * 2) + 1. 
        // the variable id is stored in answer. 
        if (next % 2 == 0)
        {
          answer[numVarsFound] = ((next / 2)+1);
        }
        else
        {
          answer[numVarsFound] = ((next + 1)/2); 
        }

        // clear occur for the chosen var (in negated and non-negated form)
        occur[next] = 0;
        if (next % 2 == 0)
          occur[next+1] = 0;
        else
          occur[next-1] = 0;

      } // for (int numVarsFound...

      return answer;
   }//end chooseSplitVars




    /**
     * Takes a subproblem and returns a list of the subproblem split further into
     * the specified amount of subproblems (numSubProb).
     * This version of this method selects the first unassigned vars to split by.
     *
     * @param s the subproblem to be split
     * @param numSubProb the number of subproblems
     */
    private List <SubProblem> splitHelper1(SubProblem s, int numSubProb)
    {
    	List <SubProblem> answer = new LinkedList <SubProblem> ();
    	// return SubProblem s in list form
    	if (numSubProb == 1)
    	{
    		answer.add(s);
    		return answer;
    	}
    	else
    	{
    		//just a sanity check
    		if(s.getAssignment().getNumUnassignedVars() == false)
    		{
    			return null;
    		}
    		else
    		{
    			//pick a var v
    			int v = s.getAssignment().findFirstUnassignedVar();
    			//create s1 & s2 same as s w/ v=F and v=T
    			SubProblem s1 = new SubProblem (s);
    			SubProblem s2 = new SubProblem (s);
    			s1.getAssignment().assignVar(v, 1);
    			s2.getAssignment().assignVar(v,0);
    			int n1 = numSubProb/2;
    			int n2 = numSubProb - n1;
    			List <SubProblem> l1 = splitHelper1(s1, n1);
    			List <SubProblem> l2 = splitHelper1(s2, n2);
    			for( SubProblem subProblem : l1)
    	              	    answer.add (subProblem);
    			for( SubProblem subProblem : l2)
    	              	    answer.add (subProblem);
    			return answer;
    		}
    	} // end else
    } // end splitHelper1

} // class Msat