1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
import java.util.ArrayList;
import java.util.Collections;
import java.util.Map;
import java.util.Scanner;
import java.util.TreeMap;

public class cnf {

	private static final int MAX_VAL = 1000000007;
	private static int[] powers;
	private static int result;
	private static int n;

	public static void main(String[] args) {
		Scanner in = new Scanner(System.in);
		n = in.nextInt();
		powers = new int[n + 1];
		powers[0] = 1;
		for (int i = 1; i <= n; i++) {
			powers[i] = (powers[i - 1] * 2) % MAX_VAL;
		}
		in.nextLine();
		String formula = in.nextLine();
		String[] strclauses = formula.split("\\s\\^\\s");
		ArrayList<Clause> clauses = new ArrayList<>(n);
		for (String strclause : strclauses) {
			String[] strliterals = strclause.substring(1, strclause.length() - 1).split("\\sv\\s");
			Clause clause = new Clause();
			for (String strliteral : strliterals) {
				if (strliteral.startsWith("~")) {
					Integer val = Integer.valueOf(strliteral.substring(2));
					clause.addLiteral(val, -1);
				} else {
					Integer val = Integer.valueOf(strliteral.substring(1));
					clause.addLiteral(val, 1);
				}
			}
			clauses.add(clause);
		}
		Collections.sort(clauses);
		Node root = new Node();
		root.setVal(clauses.get(0).getLiterals().keySet().iterator().next());
		if (clauses.get(0).getLiterals().keySet().size() == 1) {
			if (clauses.get(0).getLiterals().get(root.getVal()) < 0)
				root.setRight(new Node());
			else
				root.setLeft(new Node());
		}
		for (Clause clause : clauses) {
			excludeClause(root, clause);
		}
		result = powers[n];
		actualizeResult(root, 0);
		System.out.println(result);
	}

	private static void actualizeResult(Node node, int deep) {
		if (node == null)
			return;
		if (node.getVal() == null) {
			if (result < powers[n - deep])
				result += MAX_VAL;
			result -= powers[n - deep];
		} else {
			actualizeResult(node.getLeft(), deep + 1);
			actualizeResult(node.getRight(), deep + 1);
		}
	}

	private static void excludeClause(Node node, Clause clause) {
		if (node.getVal() == null)
			return;
		Integer state = clause.getLiterals().get(node.getVal());
		if (state == null) {
			if (node.getLeft() == null) {
				Node left = new Node();
				left.setVal(clause.getLiterals().keySet().iterator().next());
				if (left.getVal() == null)
					node.setLeft(left);
			} else if (node.getRight() == null) {
				Node right = new Node();
				right.setVal(clause.getLiterals().keySet().iterator().next());
				node.setRight(right);
			}
			excludeClause(node.getLeft(), clause.copy());
			excludeClause(node.getRight(), clause.copy());
		} else {
			clause.getLiterals().remove(node.getVal());
			if (state < 0) {
				if (clause.getLiterals().size() == 0) {
					node.setRight(new Node());
					return;
				}
				if (node.getRight() == null) {
					Node right = new Node();
					right.setVal(clause.getLiterals().keySet().iterator().next());
					node.setRight(right);
				}
				excludeClause(node.getRight(), clause.copy());
			} else {
				if (clause.getLiterals().size() == 0) {
					node.setLeft(new Node());
					return;
				}
				if (node.getLeft() == null) {
					Node left = new Node();
					left.setVal(clause.getLiterals().keySet().iterator().next());
					node.setLeft(left);
				}
				excludeClause(node.getLeft(), clause.copy());
			}
		}
	}

}

class Clause implements Comparable<Clause>, Cloneable {
	private Map<Integer, Integer> literals = new TreeMap<>();

	public Map<Integer, Integer> getLiterals() {
		return literals;
	}

	public void addLiteral(int x, int state) {
		literals.put(Integer.valueOf(x), Integer.valueOf(state));
	}

	public int size() {
		return literals.size();
	}

	@Override
	public int compareTo(Clause arg0) {
		return size() - arg0.size();
	}
	
	public Clause copy() {
		Clause copy = new Clause();
		copy.getLiterals().putAll(literals);
		return copy;
	}
}

class Node {
	private Integer val;
	private Node left;
	private Node right;

	public Node getLeft() {
		return left;
	}

	public Node getRight() {
		return right;
	}

	public Integer getVal() {
		return val;
	}

	public void setLeft(Node left) {
		this.left = left;
	}

	public void setRight(Node right) {
		this.right = right;
	}

	public void setVal(Integer val) {
		this.val = val;
	}
}