public static void checkVariableStats() {
		System.out.println("Checking variable stats");
		for(int i = 1; i < variables.size(); i++) {
			//gather information about the variable
			int timesPos = 0;
			int timesNeg = 0;
			boolean isUnit = false;
			Variable v = variables.get(i);
			for(Clause c : clauses) {
				if(c.isSatisfied()) continue;

				Literal l = c.getLiteral(v);
				if(l == null) continue;

				if(l.getSign()) timesPos++;
				else timesNeg++;

				//count up the number of unassigned literals
				int numUnassignedLits = 0;
				for(Literal lit : c.getLiterals()) {
					if(lit.getVariable().getAssignment() == Variable.UNASSIGNED)
						numUnassignedLits++;
				}

				if(numUnassignedLits == 1 && v.getAssignment() == Variable.UNASSIGNED) 
					isUnit = true;
			}
			//make sure they match what the variable knows
			if(v.getTimesPositive() != timesPos || v.getTimesNegative() != timesNeg) {
				System.out.println("Variable " + v.getName() + " has wrong times pos/neg stats");
				printFormulaInfo();
				System.exit(4);
			} else if(isUnit && v.getUnitClauses().size() == 0) {
				System.out.println("Variable " + v.getName() + " thinks it is not unit, but is actually unit");
				printFormulaInfo();
				System.exit(4);
			} else if(!isUnit && v.getUnitClauses().size() > 0) {
				System.out.println("Variblae " + v.getName() + " thinks it is unit, but actually is not unit");
				printFormulaInfo();
				System.exit(4);
			}
			//check purity
			if(v.isPure() == 0) {
				//thinks it is not pure
				if(timesPos == 0 || timesNeg == 0) {
					System.out.println("Variable " + v.getName() + " thinks it is not pure, but actually is");
					printFormulaInfo();
					System.exit(4);
				}
			} else {
				//thinks it is pure
				if(timesPos > 0 && timesNeg > 0) {
					System.out.println("Variable " + v.getName() + " thinks it is pure, but actually is not");
					printFormulaInfo();
					System.exit(4);
				}
			}
		}
	}