//package GregDLLSolver;

//Author:Greg Viola
//Class: Algos
//Version: 5
//Due Date: 4/16/07
//Status: Complete up to specifications

import java.util.*;
import java.io.*;

/**
* A Solver for a basic SAT Solver.  Given a formula, generates a partial
* assignment and tests it against the formula.  Continues adding to the
* partial assignment until the formula is satisfied or unsatisfiable.
*/
public class GregDLLSolver
{

	private Formula f; // the formula to be solved
        Assignment pa;  // a partial assignment to be refined

	public GregDLLSolver(String inputFilename)
	{
		try{
		f = new Formula(inputFilename);
		}
		catch (FileNotFoundException fnfe)
		{
			System.out.println("Couldn't create formula.");
		}
        	pa = new Assignment(f.getNumVars()); // fully unassigned
	}


	public GregDLLSolver(SubProblem subProblem)
	{
		f = subProblem.getFormula();
		pa = subProblem.getAssignment();
	}
/**
 * Solves the formula.
 *
 * @param f the formula to be solved.
 * @param numVars the number of variables.
 */
 public String solve()
 {
      if (DP(f,pa))
      {
       // System.out.println("Satisfiable"); 
	return pa.toString();
      }      
      else
      {
	//System.out.println("Unsatisfiable");
        return "";
      }
 }

/**
 * Invokes the Davis Putnam algorithm.  Returns true if the formula
 * is satisfied by the given partial assignment.
 *
 * @param f the formula to be solved.
 * @param pa the partial assignment to solve the formula.
 * @return boolean true if the formula is satisfied.
 */
 //Note: Both extra credits are in this method.
 private boolean DP(Formula f, Assignment pa)
 {
      if (f.isEmpty())
         return true;
      if (f.hasEmptyClause())
         return false;
      if (f.satisfied(pa))
          return true;
      if (f.hasFalseClause(pa))
         return false;
      int unit = f.unitClause(pa);
      if (unit == 0) //There are no unit clauses
      {
        int var = chooseNextVar(pa, f);
        if (var == 0)
          return false;
        if (var < 0)
        {
          pa.assignVar(Math.abs(var),0);
        }
        else
        {
          pa.assignVar(var,1);
        }
        if (DP(f,pa))
          return true;
        else
        {
          if (var<0)
          {
            pa.assignVar(Math.abs(var),1);
          }
          else
          {
            pa.assignVar(var,0);
          }
          if (!DP(f,pa))
          {
              //Reset the variable in the assignment
              //to be unassigned.
              pa.assignVar(var,-1);
              return false;
          }
          return true;
        }
      }
      else //There is a unit clause
      {
        if (unit < 0)
        {
          unit *= -1;
          pa.assignVar(unit, 0);
          if (!DP(f,pa))
          {
              //Resets the variable to unassigned status
              pa.assignVar(unit, -1);
              return false;
          }
          return true;
        }
        else
        {
          pa.assignVar(unit, 1);
          if (!DP(f,pa))
          {
              //Resets the variable to unassigned status.
              pa.assignVar(unit, -1);
              return false;
          }
          return true;
        }
      }//end else
 }//end DP

/**
 * Chooses the next variable to be set. The variable is chosen based on
 * which term occur the most in the formula.  This method is
 * invoked only if there are no unit clauses.
 *
   * @param partial the current partial assignment.
   * @return int the term to be used next.
   */
   private int chooseNextVar(Assignment partial, Formula f)
   {
        double maxOccur = 0; //Stores the largest number of occurrences
        int next = 0;
        f.setOccurred(partial); //Updates occurrences
        double [] occur = f.getOccurrences(); // frequency counts for all literals
                                              // in f
        Vector <Integer> assign = partial.getAssignment();
        double frequency; // frequency of a literal
        for (int i=0; i<occur.length; i++)
        {
           frequency = occur[i];
           if (frequency > maxOccur)
           {
                maxOccur = occur[i];
                next = i;
           }
        }
        //Decides whether the term is true/false (positive/negative)
        //for the chosen variable.
        if (next % 2 == 0)
        {
          return ((next / 2)+1);
        }
        else
        {
          return (-1 * ((next + 1)/2));
        }
   }//end chooseNextVar


}//end Solver