// Ambrose Sterr
// 04/18/06
// This program is a solution to the SAT problem.
// Usage: java threeSat <switch> <formula source> <file2>
//      <switch>: can be either -s, -t, -cls, or -clt.
//          If <switch>= -s or -t, the program interprets <formula source> as a file.
//          If <switch>= -cls or -clt, the program interprets <formula source> as a string formula.
//          If <switch>= -s or -cls, the program outputs a solution to the formula to <file2>.
//          If <switch>= -t or -clt, the program reads a solution from <file2> and checks it on the formula.
//      <formula source>: The formula, whether string or file, must consist of a formula in CNF, with [,] or [^] representing OR and [ ] or [&] representing AND, and ! representing NOT.
//          Each clause must be encased in parenthesis.  Whitespace between clauses is only permitted in files, not the command line.
//      <file2> the file must consist of lines of exactly this form: <var> = <boolean>, where <var> is a variable name and <boolean> is "true" or "false" without quotes.
//
//
// The maximum runtime of this algorithm (in -s mode) is by nature exponential, as it my have to evaluate up to 2^n combinations of variable assignments, where n is the number of distinct symbols.
// In -t mode, however, evaluate need only be run once.

import java.util.*;
import java.io.*;
public class threeSAT
{
    static Hashtable symboltable;
    static String[] symbolarray;
    static clause[] pieces;
    
    public static void main(String args[])
    {
        String text = "";
        if (args[0].equals("-cls")||args[0].equals("-clt"))
        {
            text = args[1];
        }
        else
        {
            try
            {
            BufferedReader input = new BufferedReader(new FileReader(args[1]));
            text = input.readLine();
            }
            catch (Exception e) {}
        }
        String[] clauses = text.split("[\\(\\)\\&\\s]+");
        pieces = new clause[clauses.length-1];
        //System.out.println(pieces.length);
        symboltable = new Hashtable();
        for (int i = 1; i <= pieces.length; i++)
        {
            //System.out.println("Pieces copy "+i);
            //System.out.println(clauses[i]+ "t");
            String[] symbols = clauses[i].split("[,^]");
            //System.out.println(symbols[0]);
            pieces[i-1] = new clause(symbols);
            for (int j = 0; j < symbols.length; j++)
            {
                if (symbols[j].startsWith("!"))
                {
                    symbols[j] = symbols[j].substring(1);
                    //System.out.println(pieces[i-1].members[j]);
                }
                if (!(symboltable.containsKey(symbols[j])))
                {
                    symboltable.put(symbols[j],Boolean.FALSE);
                }
            }
        }
        Enumeration keys = symboltable.keys();
        //System.out.println("");
        symbolarray = new String[symboltable.size()];
        for (int i = 0; i < symbolarray.length; i++)
        {
            symbolarray[i] = (String)keys.nextElement();
            //System.out.println(symbolarray[i]);
        }
        if (args[0].equals("-t")||args[0].equals("-clt"))
        {
            try
            {
                BufferedReader inputtable = new BufferedReader(new FileReader(args[2]));
                for (int i = 0; i < symbolarray.length; i++)
                {
                    String[] pair = (inputtable.readLine()).split(" = ");
                    //System.out.println("T: "+pair[0]+" "+pair.length);
                    symboltable.put(pair[0], new Boolean(pair[1]));
                }
            }
            catch (Exception e)
            {
            }
            if (eval())
            {
                System.out.println("That is a valid solution.");
            }
            else
            {
                System.out.println("That solution is not valid.");
            }
        }
        else if (args[0].equals("-s")||args[0].equals("-cls"))
        {
            if (rSolve(0))
            {
                try {
                    PrintStream logger = new PrintStream(args[2]);
                    for (int i = 0; i < symbolarray.length; i++)
                    {
                        String out = symbolarray[i]+" = "+((Boolean)symboltable.get(symbolarray[i])).booleanValue();
                        //System.out.println(out+out.length());
                        logger.println(out);
                    }
                }
                catch (Exception e)
                {
                    System.out.print("Uh oh!");
                }
            }
        }
    }
    public static boolean rSolve(int n)
    {
        if (n == symbolarray.length)
        {
            return eval();
        }
        else
        {
            symboltable.put(symbolarray[n], Boolean.FALSE);
            if (rSolve(n+1))
            {
                return true;
            }
            symboltable.put(symbolarray[n], Boolean.TRUE);
            if (rSolve(n+1))
            {
                return true;
            }
            return false;
        }
    }
    public static boolean eval()
    {
        for (int i = 0; i < pieces.length; i++)
        {
            //System.out.println(i);
            if (!(pieces[i].eval(symboltable)))
            {
                return false;
            }
        }
        return true;
    }
}