public static Vector<Assignment> DPLL() {

		if(DEBUG) System.out.println("\nStarting DPLL()"); 

		//see if the formula is satisfied
		if(Clause.isFormulaSAT(clauses)) {
			if(DEBUG) System.out.println("Formula is SAT - returning the assignment");
			//make sure we have assigned all the chance variables, so we know the probability of each possible plan
			return assignNextChance();
		}

		//see if the formula is un-satisfied
		if(Clause.isFormulaUnSAT(clauses)) {
			if(DEBUG) System.out.println("Formula is UNSAT - returning the assignment");
			//make sure we have assigned all the chance variables, so we know the probability of each possible plan
			return assignNextChance();
		}

		//try to find a variable to assign.

		//first, look for a unit clause
		for(int i = 1; i < variables.size(); i++) {
			Variable v = variables.get(i);

			//only consider variables that are unassigned
			if(v.getAssignment() == Variable.UNASSIGNED) {

				//see if it is unit
				if(v.isUnit()) {
					if(SsatSolver.DEBUG) System.out.println("Variable " + v.getName() + " is unit");
					Clause unitClause = v.getFirstUnitClause();
					assert unitClause != null;
					Literal unitLiteral = unitClause.getLiteral(v);

					//try the assignment, based on if it appears positively or negatively unit.
					//return different vectors of assignments if it is choice or chance.
					Vector<Assignment> unitAssignments;
					if(unitLiteral.getSign()) {
						if(SsatSolver.DEBUG) System.out.println("Assigning var " + v.getName() + " to true");
						unitAssignments = tryAssign(unitLiteral.getVariable(), Variable.TRUE);
						//depending on if v is choice or chance, we may need to adjust things
						if(v.isChoice()) {
							//v is choice, so we don't need to adjust the probability of success.
							return unitAssignments;
						} else {
							//v is chance, so we need to adjust the probability of success for all
							//the assignments we got back.
							assert v.isChance();
							for(Assignment a : unitAssignments) {
								a.adjustProbability(v.getChanceTrue());
							}
							return unitAssignments;
						}
						//Do the same, but with assigning the variable to FALSE
					} else {
						if(SsatSolver.DEBUG) System.out.println("Assigning var " + v.getName() + " to false");
						unitAssignments = tryAssign(unitLiteral.getVariable(), Variable.FALSE);
						//depending on if v is choice or chance, we may need to adjust things
						if(v.isChoice()) {
							return unitAssignments;
						} else {
							assert v.isChance();
							for(Assignment a : unitAssignments) {
								a.adjustProbability(v.getChanceFalse());
							}
							return unitAssignments;
						}
					}
				}
			}
		}

		//Next, look for a pure variable
		for(int i = 1; i < variables.size(); i++) {
			Variable v = variables.get(i);
			//only consider variables that are choice variables and unassigned
			if(v.isChoice() && v.getAssignment() == Variable.UNASSIGNED) {
				//purity will be positive if v only appears positively,
				//negative if v only appears negatively, or 0 otherwise.
				int purity = v.isPure();
				if(purity != 0) {
					if(SsatSolver.DEBUG) System.out.println("Variable " + v.getName() + " is pure");
					//we have a pure variable
					//assign it accordingly
					Vector<Assignment> pureAssignments;
					if(purity > 0) {
						if(SsatSolver.DEBUG) System.out.println("Assigning it true");
						pureAssignments = tryAssign(v, Variable.TRUE);
						return pureAssignments;
					}
					else { 
						if(SsatSolver.DEBUG) System.out.println("Assigning it false");
						pureAssignments = tryAssign(v, Variable.FALSE);
						return pureAssignments;
					}
				}
			}
		}

		//We weren't able to find a pure or unit variable, so go to the next unassigned variable
		Variable nextAssignee = null;
		for(int i = 1; i < variables.size(); i++) {
			Variable v = variables.get(i);
			if(v.getAssignment() == Variable.UNASSIGNED) {
				nextAssignee = v;
				break;
			}
		}

		assert nextAssignee != null;

		if(SsatSolver.DEBUG) System.out.println("No pure or unit variables - trying to assign variable " + nextAssignee.getName());

		//try assigning the variable to true and to false
		if(SsatSolver.DEBUG) System.out.println("Trying variable " + nextAssignee.getName() + " assigned to TRUE");
		Vector<Assignment> trueAssignments = tryAssign(nextAssignee, Variable.TRUE);
		if(SsatSolver.DEBUG) System.out.println("Trying variable " + nextAssignee.getName() + " assigned to FALSE");
		Vector<Assignment> falseAssignments = tryAssign(nextAssignee, Variable.FALSE); 

		//depending on if the variable is chance or choice, do different things
		if(nextAssignee.isChoice()) {
			//for a choice variable, return the set of assignments with the higher probability of sucess
			//since we get to choose the assignment of choice variables to maximize success.
			if(Assignment.getTotalProbability(trueAssignments) >= Assignment.getTotalProbability(falseAssignments))
				return trueAssignments;
			else 
				return falseAssignments;
		} else {
			//it is a chance variable
			assert nextAssignee.isChance();

			//adjust the probabilities of the true assignments by the chance that the variable is true
			//and adjust the probabilities of the false assignmetns by the chance that the varible is false.
			for(Assignment a : trueAssignments) {
				a.adjustProbability(nextAssignee.getChanceTrue());
			}

			for(Assignment a : falseAssignments) {
				a.adjustProbability(nextAssignee.getChanceFalse());
			}

			//now, return a Vector containing the false and true assignments.
			Vector<Assignment> allAssignmetns = new Vector<Assignment>(trueAssignments.size() + falseAssignments.size());
			allAssignmetns.addAll(trueAssignments);
			allAssignmetns.addAll(falseAssignments);

			return allAssignmetns;
		}
	}