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

//PRE:
//reads from standard input a file of the following form

//var1 var2 ...
//var3 ~var2 ...
//...

//each line represents a clause in a proposition.  There can be no
//blank lines.  A line consists of one or more arbitrary strings
//separated by spaces.  The strings represent the boolean variables.
//If the string is prefixed by a single ~ symbol then the variable is
//assumed to be negated in that clause.  The variables in the line are
//assumed to be "or'ed" together and each line is assumed to be
//'anded" together with the other lines.

//POST:

//If any line in the input is blank, signals an error.

//Otherwise calls the gsat algorithm on the propositional logic
//formula specified by the file with the parameters max-flips and
//max-tries.  If gsat returns a satisfying assignment, prints this
//assignment to stdout otherwise prints a failure message.


public class Formula{

  //the VarRec contains information about a variable in the CNF.  It
  //contains 1) the unique id for the variable 2) info on whether or
  //not that variable is negated

  //a formula object contains an array of arrays of VarRecs where
  //arrCNF[i][j] is the information about the jth variable in the ith
  //clause.  e.g. if the first clause is a v ~b v c then arrCNF[0][2]
  //is the varRec with values 2 for id and true for isNegated.
  VarRec arrCNF[][];
  int numVars;

  //dVar stores mappings from boolean variable names to unique integer identifiers for the names.
  //we need to keep it around to print out satisfying truth assignments
  Dictionary dVar;

public int numVars(){return numVars;}

public Dictionary getDictionary(){return dVar;}


  //PRE:  the id values in dVar are no larger than the number of elems in dVar.
  //POST: returns a string representing this
public String toString(){
  int size = dVar.size();

  //contains mapping of the keys in dVar to the strings
  String arrIDS[] = new String[size];
  
  Enumeration enum = dVar.keys();
  while(enum.hasMoreElements()){
    String sCurr = (String) enum.nextElement();
    Integer i = (Integer)dVar.get(sCurr);
    int id = i.intValue();
    arrIDS[id] = sCurr;
  }

  String sRes = "";

  for(int i=0;i<arrCNF.length;i++){
    for(int j=0;j<arrCNF[i].length;j++){
      VarRec vr = arrCNF[i][j];
      if(vr.isNegated()){
	sRes = sRes + "~";
      }
      String sVarName = arrIDS[vr.getID()];
      sRes = sRes + sVarName + " ";
    }
    sRes = sRes + "\n";
  }
  return sRes;
}


  //PRE: sLine is the current line, dVar is a mapping from the strings in the input to unique numbers
  //POST: RES is a vector of the VarRecs for each of the variables in this line
private Vector getVarsOnLine(String sLine, Dictionary dVar){
  StringTokenizer st = new StringTokenizer(sLine, " ");
  Vector vRes = new Vector(1);  
  
  while(st.hasMoreTokens()){
    String sCurrVar = st.nextToken();

    //assert sCurrVar.size()>0 
    boolean isNegated = (sCurrVar.charAt(0)=='~');
    if(isNegated){
      sCurrVar = sCurrVar.substring(1);  //get rid of the "~" char
    }

    Integer id = (Integer) dVar.get(sCurrVar);
    if(id==null){
      id = new Integer(dVar.size());
      dVar.put(sCurrVar,id);
    }
    VarRec currRec = new VarRec(id.intValue(),isNegated);
    vRes.addElement(currRec);
  }
  return vRes;
}


  //PRE:  inStrm is correctly formatted(as specified at the top of this file
  //POST: sets arrCNF and numVars appropriately.
public Formula(DataInputStream inStrm){
  
  InputStreamReader isr = new InputStreamReader(inStrm);
  LineNumberReader lnr = new LineNumberReader(isr);

  dVar = new Hashtable();
  Vector vConjuncts = new Vector();

  boolean done = false;

  String sLine = null;
  while(!done){
    try{
      sLine = lnr.readLine();
      if(sLine!=null&&sLine.length()>0){
	Vector vVars = getVarsOnLine(sLine,dVar);
	vConjuncts.addElement(vVars);
      }else{
	done = true;
      }
    }
    catch(Exception e){
      System.out.println("error in input file");
      System.exit(1);
    }
  }

  this.numVars = dVar.size();

  //now put the information that's in the vectors into arrCNF
  int numConjuncts = vConjuncts.size();
  this.arrCNF = new VarRec[numConjuncts][];

  for(int i=0;i<numConjuncts;i++){
    Vector vCurrConj = (Vector) vConjuncts.elementAt(i);
    int numVarsCurrConj = vCurrConj.size();
    this.arrCNF[i] = new VarRec[numVarsCurrConj];
    for(int j=0;j<numVarsCurrConj;j++){
      VarRec currVarRec = (VarRec) vCurrConj.elementAt(j);
      this.arrCNF[i][j] = currVarRec;
    }
  }
}


  //POST: RES is the number of conjuncts in this that are satisfied by assign.
public int numSatisfiedConj(Assignment assign){
  int numConjSat = 0;
  for(int i=0;i<arrCNF.length;i++){

    boolean currConjSat = false;
    int currConjSize = arrCNF[i].length;
    for(int j=0;j<currConjSize&&!currConjSat;j++){
      VarRec currVR = arrCNF[i][j];
      int currID = currVR.getID();
      boolean wantTrue = !(currVR.isNegated());
      boolean isTrue = assign.getVarVal(currID);
      if(isTrue==wantTrue){  //the assignment val satisfies this var
	currConjSat = true;
      }
    }
    if(currConjSat){
      numConjSat++;
    }
  }
  return numConjSat;
}


  //POST: RES is true iff this is satisfied by assign
public boolean isSatisfied(Assignment assign){
  int numConj = arrCNF.length;
  int numSat = numSatisfiedConj(assign);
  return (numConj==numSat);
}
    
  //POST: RES is the assignment with the highest number of satisfied
  //conjuncts in cnf which is different in exactly one truth value
  //from inAssign.
public static Assignment getBestVarFlip(Formula cnf, Assignment inAssign){

  int maxSat = -1;
  Assignment bestAssign = null;

  for(int i=0;i<inAssign.size();i++){
    Assignment currAssign = inAssign.flipVarVal(i);
    int numSat = cnf.numSatisfiedConj(currAssign);
    if(numSat>maxSat){
      maxSat = numSat;
      bestAssign = currAssign;
    }
  }
  return bestAssign;
}

  //POST: calls the gsat algorithm on the cnf.  If an assignment is
  //found within the bounds numTries and numFlips, returns that
  //assignment in RES otherwise RES is null

  //The GSAT algorithm is the following:
  //
  //do the following until a satisfying assignment is found
  //for i = 1 to numTries
  //r <- a random assignment
  //   for j = 1 to numFlips
  //   flip the bit of r which gives the maximal number of satisfied conjuncts (break a tie in any manner)

public static Assignment getSatAssign(Formula cnf, int numFlips, int numTries){
  boolean foundAssign = false;

  int numVars = cnf.numVars();
  Assignment currAssign = new Assignment(numVars);

  for(int i=0;i<numTries&&!foundAssign;i++){
    currAssign.randomize();
    foundAssign = cnf.isSatisfied(currAssign);

    for(int j=0;j<numFlips&&!foundAssign;j++){  
      currAssign = getBestVarFlip(cnf,currAssign);
      foundAssign = cnf.isSatisfied(currAssign);
    }
  }
  if(foundAssign){
    return currAssign;
  }else{
    return null;
  }
}

  //PRE: STDIN contains a cnf as specified
  //POST: trys GSAT, if it works prints assignment, else prints that it failed
public static void main(String[] args){
  final int numFlips = 100;
  final int numTries = 100;

  DataInputStream inStrm = new DataInputStream(System.in);
  Formula cnf = new Formula(inStrm);
  System.out.println("The given formula is:");
  System.out.println(cnf.toString());
  Assignment assign = getSatAssign(cnf,numFlips,numTries);
  if(assign!=null){
    //print the assignment
    System.out.println("A satisfying Assignment is:");
    Dictionary dVar = cnf.getDictionary();
    String sAssign = assign.toString(dVar);
    System.out.println(sAssign);
  }else{
    System.out.println("Could not find a truth assignment");
  }
}


}