SEERC 2015 A : Equivalence

問題リンク : https://icpcarchive.ecs.baylor.edu/external/71/7173.pdf

問題概要　：
２つの論理式が与えられる
それらが等価か判定せよ

論理式は論理変数、論理和、論理積、否定から構成される
論理演算の優先度は気にしなくても良い（適切に括弧がつけられている）
論理式に含まれる論理変数は高々５１個

解法：
BDDで解いた
最悪ケースが大丈夫なのか謎ではあったが、、
BDD自体は北大の授業のスライドを参考に作成
codeforcesのGYMで他の人のコードを見たら皆乱数で適当に変数に値を割り当てて評価し、適当な回数だけ繰り返し評価を行い全て一致するかどうかで判定していた
LiveArchiveはまだジャッジが用意されていないようなのでジャッジ待ち

コード:

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


class BinaryOperatorMemoState implements Comparable<BinaryOperatorMemoState> {
	public char op;
	public int F, G;

	public BinaryOperatorMemoState() {

	}

	public BinaryOperatorMemoState(char op, int F, int G) {
		this.op = op;
		this.F = F;
		this.G = G;
	}

	@Override
	public int compareTo(BinaryOperatorMemoState o) {
		int result = new Character(this.op).compareTo(o.op);
		if (result == 0) {
			result = new Integer(this.F).compareTo(o.F);
			if (result == 0) {
				result = new Integer(this.G).compareTo(o.G);
			}
		}
		return result;
	}
}

class BooleanExpression {
	public BooleanExpression deepCopy() {
		System.out.println("WARNING");
		return this.deepCopy();
	}

	public BooleanExpression assignBooleanValueToLogicVariable(boolean booleanValue, LogicVariable logicVariable) {
		System.out.println("WARNING");
		return this.assignBooleanValueToLogicVariable(booleanValue, logicVariable);
	}

	public int traverse() {
		System.out.println("WARNING");
		return -1;
	}

	public boolean eval(HashSet<State> F, HashSet<State> L) {
		System.out.println("WARNING");
		return false;
	}

	public BooleanExpression recoverPredicate() {
		System.out.println("WARNING");
		return this.recoverPredicate();
	}

}


class And extends BooleanExpression {
	public BooleanExpression left, right;

	public And() {

	}

	public And(BooleanExpression left, BooleanExpression right) {
		this.left = left;
		this.right = right;
	}

	@Override
	public int traverse() {
		int F = this.left.traverse();
		int G = this.right.traverse();
		return BDD.apply('&', F, G);
	}

	@Override
	public And deepCopy() {
		return new And(left.deepCopy(), right.deepCopy());
	}

	@Override
	public And recoverPredicate() {
		return new And(left.recoverPredicate(), right.recoverPredicate());
	}

	@Override
	public BooleanExpression assignBooleanValueToLogicVariable(boolean booleanValue, LogicVariable logicVariable) {
		BooleanExpression tmp_left = left.assignBooleanValueToLogicVariable(booleanValue, logicVariable);
		BooleanExpression tmp_right = right.assignBooleanValueToLogicVariable(booleanValue, logicVariable);
		if ((tmp_left instanceof LogicVariable) && (tmp_right instanceof LogicVariable)) {
			boolean leftHasValue = ((LogicVariable) tmp_left).hasValue();
			boolean rightHasValue = ((LogicVariable) tmp_right).hasValue();
			if (leftHasValue && rightHasValue) {
				return new LogicVariable(-1, ((LogicVariable) tmp_left).getValue() && ((LogicVariable) tmp_right).getValue());
			} else if (leftHasValue) {
				if (!((LogicVariable) tmp_left).getValue()) {
					return new LogicVariable(-1, false);
				} else {
					return tmp_right;
				}
			} else if (rightHasValue) {
				if (!((LogicVariable) tmp_right).getValue()) {
					return new LogicVariable(-1, false);
				} else {
					return tmp_left;
				}
			} else {
				return new And(tmp_left, tmp_right);
			}
		} else if (tmp_left instanceof LogicVariable) {
			if (((LogicVariable) tmp_left).hasValue()) {
				if (!((LogicVariable) tmp_left).getValue()) {
					return new LogicVariable(-1, false);
				} else {
					return tmp_right;
				}
			} else {
				return new And(tmp_left, tmp_right);
			}
		} else if (tmp_right instanceof LogicVariable) {
			if (((LogicVariable) tmp_right).hasValue()) {
				if (!((LogicVariable) tmp_right).getValue()) {
					return new LogicVariable(-1, false);
				} else {
					return tmp_left;
				}
			} else {
				return new And(tmp_left, tmp_right);
			}
		} else {
			return new And(tmp_left, tmp_right);
		}
	}

	@Override
	public boolean eval(HashSet<State> F, HashSet<State> L) {
		return left.eval(F, L) && right.eval(F, L);
	}

	@Override
	public String toString() {
		return "(" + left + "&" + right + ")";
	}

}

class LogicVariable extends BooleanExpression {
	int ID;
	byte value;

	public LogicVariable() {
		this.value = -1;
	}

	public LogicVariable(int ID) {
		this.ID = ID;
		this.value = -1;
	}

	public LogicVariable(int ID, byte value) {
		this.ID = ID;
		this.value = value;
	}

	public LogicVariable(int ID, boolean value) {
		this.ID = ID;
		this.value = (byte) ((value == true) ? 1 : 0);
	}

	@Override
	public int traverse() {
		if (this.hasValue()) {
			return this.getValue() ? 1 : 0;
		}
		return BDD.getNode(new BDDNode(this.ID, 0, 1));
	}

	@Override
	public LogicVariable deepCopy() {
		return new LogicVariable(ID, value);
	}

	@Override
	public LogicVariable recoverPredicate() {
		return new LogicVariable(((ID < 0) ? -ID : ID), value);
	}

	@Override
	public BooleanExpression assignBooleanValueToLogicVariable(boolean booleanValue, LogicVariable logicVariable) {
		if (ID == logicVariable.getID()) {
			return new LogicVariable(-1, booleanValue);
		}
		return this.deepCopy();
	}

	public boolean hasValue() {
		return this.value != -1;
	}

	public boolean getValue() {
		return this.value == 1;
	}

	public boolean isFalse() {
		return this.hasValue() && !getValue();
	}

	public boolean isTrue() {
		return this.hasValue() && getValue();
	}

	public void setValue(boolean value) {
		this.value = (byte) (value ? 1 : 0);
	}

	public void reverseValue() {
		if (this.value != -1) {
			this.value = (byte) ((this.value == 1) ? 0 : 1);
		}
	}

	public int getID() {
		return this.ID;
	}

	@Override
	public boolean eval(HashSet<State> F, HashSet<State> L) {
		if (ID == -1) {
			if (value == -1) {
				System.out.println("What is this Logic Variable");
			}
			if (value == 1) {
				return true;
			} else {
				return false;
			}
		}
		return F.contains(new State(ID)) || L.contains(new State(ID));
	}

	@Override
	public String toString() {
		if (ID == -1) {
			if (value == -1) {
				System.out.println("What is this Logic Variable");
			}
			if (value == 1) {
				return "true";
			} else {
				return "false";
			}
		}
		return String.valueOf(ID);
	}

}

class Not extends BooleanExpression {
	public BooleanExpression inner;

	public Not() {

	}

	public Not(BooleanExpression inner) {
		this.inner = inner;
	}

	@Override
	public int traverse() {
		int address = inner.traverse();
		return this.notApply(address);
	}

	public int notApply(int address) {
		if (address == 0 || address == 1) {
			return (address == 0) ? 1 : 0;
		}
		BDDNode bn = BDD.nodeTable[address];
		int H0 = notApply(bn.zeroID);
		int H1 = notApply(bn.oneID);
		return BDD.getNode(new BDDNode(bn.variableID, H0, H1));
	}

	@Override
	public Not deepCopy() {
		return new Not(inner.deepCopy());
	}

	@Override
	public Not recoverPredicate() {
		return new Not(inner.recoverPredicate());
	}

	@Override
	public BooleanExpression assignBooleanValueToLogicVariable(boolean booleanValue, LogicVariable logicVariable) {
		BooleanExpression tmp = inner.assignBooleanValueToLogicVariable(booleanValue, logicVariable);
		if (tmp instanceof LogicVariable) {
			if (((LogicVariable) tmp).hasValue()) {
				((LogicVariable) tmp).reverseValue();
				return tmp;
			}
		}
		return new Not(tmp);
	}

	@Override
	public boolean eval(HashSet<State> F, HashSet<State> L) {
		return !inner.eval(F, L);
	}

	@Override
	public String toString() {
		return "!(" + inner + ")";
	}
}

class Or extends BooleanExpression {
	public BooleanExpression left, right;

	public Or() {

	}

	public Or(BooleanExpression left, BooleanExpression right) {
		this.left = left;
		this.right = right;
	}

	@Override
	public int traverse() {
		int F = left.traverse();
		int G = right.traverse();
		return BDD.apply('|', F, G);
	}

	@Override
	public Or deepCopy() {
		return new Or(left.deepCopy(), right.deepCopy());
	}

	@Override
	public Or recoverPredicate() {
		return new Or(left.recoverPredicate(), right.recoverPredicate());
	}

	@Override
	public BooleanExpression assignBooleanValueToLogicVariable(boolean booleanValue, LogicVariable logicVariable) {
		BooleanExpression tmp_left = left.assignBooleanValueToLogicVariable(booleanValue, logicVariable);
		BooleanExpression tmp_right = right.assignBooleanValueToLogicVariable(booleanValue, logicVariable);
		if ((tmp_left instanceof LogicVariable) && (tmp_right instanceof LogicVariable)) {
			boolean leftHasValue = ((LogicVariable) tmp_left).hasValue();
			boolean rightHasValue = ((LogicVariable) tmp_right).hasValue();
			if (leftHasValue && rightHasValue) {
				return new LogicVariable(-1, ((LogicVariable) tmp_left).getValue() || ((LogicVariable) tmp_right).getValue());
			} else if (leftHasValue) {
				if (((LogicVariable) tmp_left).getValue()) {
					return new LogicVariable(-1, true);
				} else {
					return tmp_right;
				}
			} else if (rightHasValue) {
				if (((LogicVariable) tmp_right).getValue()) {
					return new LogicVariable(-1, true);
				} else {
					return tmp_left;
				}
			} else {
				return new Or(tmp_left, tmp_right);
			}
		} else if (tmp_left instanceof LogicVariable) {
			if (((LogicVariable) tmp_left).hasValue()) {
				if (((LogicVariable) tmp_left).getValue()) {
					return new LogicVariable(-1, true);
				} else {
					return tmp_right;
				}
			} else {
				return new Or(tmp_left, tmp_right);
			}
		} else if (tmp_right instanceof LogicVariable) {
			if (((LogicVariable) tmp_right).hasValue()) {
				if (((LogicVariable) tmp_right).getValue()) {
					return new LogicVariable(-1, true);
				} else {
					return tmp_left;
				}
			} else {
				return new Or(tmp_left, tmp_right);
			}
		} else {
			return new Or(tmp_left, tmp_right);
		}
	}

	@Override
	public boolean eval(HashSet<State> F, HashSet<State> L) {
		return left.eval(F, L) || right.eval(F, L);
	}

	@Override
	public String toString() {
		return "(" + left + "|" + right + ")";
	}
}

class BDDNode implements Comparable<BDDNode> {
	public int variableID, zeroID, oneID;

	public BDDNode() {
	}

	public BDDNode(int variableID, int zeroID, int oneID) {
		this.variableID = variableID;
		this.zeroID = zeroID;
		this.oneID = oneID;
	}

	public BDDNode deepCopy() {
		return new BDDNode(this.variableID, this.zeroID, this.oneID);
	}

	public boolean equals(BDDNode o) {
		return variableID == o.variableID && zeroID == o.zeroID && oneID == o.oneID;
	}

	@Override
	public int compareTo(BDDNode o) {
		int result = new Integer(this.variableID).compareTo(o.variableID);
		if (result == 0) {
			result = new Integer(this.zeroID).compareTo(o.zeroID);
			if (result == 0) {
				result = new Integer(this.oneID).compareTo(o.oneID);
			}
		}
		return result;
	}

	@Override
	public String toString() {
		return "(" + variableID + "," + zeroID + "," + oneID + ")";
	}
}

//Reference : http://www-erato.ist.hokudai.ac.jp/html/php/seminar5_docs/minato_alg2010-5.pdf
class BDD {
	public static int MAX_TABLE_SIZE = 10000000;
	private static int topOfNodeTable;
	public static BDDNode[] nodeTable = null; // 0番地は0定数節点,1番地は1定数節点
	public static TreeMap<BDDNode, Integer> nodeTableCache;
	public static TreeMap<BinaryOperatorMemoState, Integer> binaryOperatorCache;

	public int addressOfNodeTable;

	public BDD() {
		if (nodeTable == null) {
			nodeTable = new BDDNode[MAX_TABLE_SIZE];
			nodeTable[0] = new BDDNode(-1, -1, -1);
			nodeTable[1] = new BDDNode(-1, -1, -1);
			topOfNodeTable = 2;
			nodeTableCache = new TreeMap<BDDNode, Integer>();
			binaryOperatorCache = new TreeMap<BinaryOperatorMemoState, Integer>();
		}
	}

	public BDD(BooleanExpression be) {
		this();
		addressOfNodeTable = build(be);
	}

	public int build(BooleanExpression be) {
		return be.traverse();
	}

	public static int getNode(BDDNode bn) {
		if (bn.zeroID == bn.oneID) {
			return bn.zeroID;
		}

		if (nodeTableCache.containsKey(bn.deepCopy())) {
			return nodeTableCache.get(bn.deepCopy());
		}
		if (topOfNodeTable >= MAX_TABLE_SIZE) {
			System.out.println("FATAL ERROR : NODE TABLE => OVERFLOW : size : " + topOfNodeTable + " capacity : " + MAX_TABLE_SIZE);
		}

		nodeTable[topOfNodeTable] = bn.deepCopy();
		nodeTableCache.put(bn.deepCopy(), topOfNodeTable);
		return topOfNodeTable++;
	}

	public static boolean isConst(int address) {
		return address == 0 || address == 1;
	}

	public static int apply(char op, int F, int G) {
		// 1. F,Gのいずれかが定数のとき、およびF=Gのとき
		if (isConst(F) || isConst(G) || F == G) {
			if (F == G) {
				return F;
			}
			if (op == '|') {
				if (isConst(F) && isConst(G))
					return F | G;
				if (isConst(F)) {
					int tmp = F;
					F = G;
					G = tmp;
				}
				if (G == 0) {
					return F;
				} else {
					return 1;
				}
			} else if (op == '&') {
				if (isConst(F) && isConst(G))
					return F & G;
				if (isConst(F)) {
					int tmp = F;
					F = G;
					G = tmp;
				}
				if (G == 0) {
					return 0;
				} else {
					return F;
				}
			} else {
				System.out.println("INVALID OPERATOR : WHAT IS " + op + "?");
			}
		}

		BinaryOperatorMemoState boms = new BinaryOperatorMemoState(op, F, G);
		if (binaryOperatorCache.containsKey(boms)) {
			return binaryOperatorCache.get(boms);
		}

		// 2.両者の最上位変数F.vとG.vが同じとき
		BDDNode bnF = nodeTable[F].deepCopy(); // deepCopyでないと手順４を実行した場合にnodeTableの値が書きかわるので注意
		BDDNode bnG = nodeTable[G].deepCopy();
		if (bnF.variableID == bnG.variableID) {
			int H0 = apply(op, bnF.zeroID, bnG.zeroID);
			int H1 = apply(op, bnF.oneID, bnG.oneID);
			if (H0 == H1) {
				binaryOperatorCache.put(boms, H0);
				return H0;
			}
			int address = getNode(new BDDNode(bnF.variableID, H0, H1));
			binaryOperatorCache.put(boms, address);
			return address;
		}
		// 変数の番号が大きいほど下位であることに注意
		// 4.F.vがG.vよりも下位のとき
		// FとGを入れ替えて、3.と同様に処理
		if (bnF.variableID > bnG.variableID) {
			int tmp = F;
			F = G;
			G = tmp;
			bnF = nodeTable[F].deepCopy();
			bnG = nodeTable[G].deepCopy();
		}

		// 3.F.vがG.vよりも上位のとき
		int H0 = apply(op, bnF.zeroID, G);
		int H1 = apply(op, bnF.oneID, G);
		if (H0 == H1) {
			binaryOperatorCache.put(boms, H0);
			return H0;
		}
		int address = getNode(new BDDNode(bnF.variableID, H0, H1));
		binaryOperatorCache.put(boms, address);
		return address;
	}

	public static void printNodeTable() {
		System.out.println("table size = " + topOfNodeTable);
		for (int i = 0; i < topOfNodeTable; i++) {
			BDDNode bn = nodeTable[i];
			System.out.println(i + "-th : " + bn);
		}
	}

	public boolean equals(BDD bdd) {
		// System.out.println("bdd1 = " + this.addressOfNodeTable);
		// System.out.println("bdd2 = " + bdd.addressOfNodeTable);
		return this.addressOfNodeTable == bdd.addressOfNodeTable;
	}

	public static int getNodeTableSize() {
		return topOfNodeTable;
	}

}

class State {
	private int ID;

	public State() {

	}

	public State(int ID) {
		this.ID = ID;
	}

	public void setID(int ID) {
		this.ID = ID;
	}

	public int getID() {
		return this.ID;
	}

	@Override
	public String toString() {
		return String.valueOf(ID);
	}

	@Override
	public int hashCode() {
		return new Integer(ID).hashCode();
	}

	@Override
	public boolean equals(Object obj) {
		if (obj != null && obj instanceof State) {
			final State state = (State) obj;
			return this.getID() == state.getID();
		}
		return false;
	}

	public int compareTo(State state) {
		return new Integer(ID).compareTo(state.getID());
	}

}

class BooleanExpressionEvaluator {
	private String context;
	private int currentPosition;

	public BooleanExpressionEvaluator(String context) {
		this.context = context;
		currentPosition = 0;
	}

	BooleanExpression fact() {
		boolean not_coef = false;
		if (context.charAt(currentPosition) == '~') {
			++currentPosition;
			not_coef = true;
		}
        BooleanExpression be = null;
		if (context.charAt(currentPosition) == '(') {
			++currentPosition;
			be = exp();
			++currentPosition;
		} else {
            int ID = context.charAt(currentPosition++);
            be = new LogicVariable(ID);
		}
		if (not_coef) {
            be = new Not(be);
		}
		return be;
	}

	BooleanExpression exp() {
		BooleanExpression state1 = fact();
		while (currentPosition < context.length() && (context.charAt(currentPosition) == 'V' || context.charAt(currentPosition) == '^')) {
			char opr = context.charAt(currentPosition++);
			BooleanExpression state2 = fact();
			if (opr == 'V') {
                state1 = new Or(state1,state2);
			} else {
                state1 = new And(state1,state2);
			}
		}
		return state1;
	}

	public BooleanExpression eval() {
		return exp();
	}

}

class Main {    
    public static BooleanExpression toBooleanExpression(String s) {
        BooleanExpressionEvaluator bee = new BooleanExpressionEvaluator(s);
        return bee.eval();
    }

    public static int exec(String p1,String p2) {
        BDD bdd = new BDD();
        BooleanExpression be_p1 = toBooleanExpression(p1);
        BooleanExpression be_p2 = toBooleanExpression(p2);
        return (bdd.build(be_p1) == bdd.build(be_p2))?1:0;
    }

    public static String removeSpace(String s) {
        StringBuilder sb = new StringBuilder();
        for(int i=0;i<s.length();i++) if( s.charAt(i) != ' ' ) {
                sb.append(s.charAt(i));
        }
        return sb.toString();
    }
    
    public static void main(String args[]) throws IOException {
        BufferedReader in = new BufferedReader(new InputStreamReader(System.in));
        while(true) {
        String p1 = in.readLine();
        if( p1 == null )break;
        String p2 = in.readLine();
        p1 = removeSpace(p1);
        p2 = removeSpace(p2);
        //System.out.println(p1 + " ?= " + p2);
        System.out.println(exec(p1,p2));
        }
    }
}