docs: public static BooleanConstraint[] createBooleanConstraints(BooleanVariable[] scope, String wff) {
  		try {
  
  			wff = wff.replace("~", "NOT ");
  			wff = wff.replace("-", "=");
  			wff = wff.replace("v", "OR");
  			wff = wff.replace("^", "AND");
  
  			MetaCSPLogging.getLogger(BooleanConstraint.class).finest("Converting WFF: " + wff);
  			
  			Converter<Symbol> sConv = new Converter<Symbol>();
  			PEParser parser = new PEParser();
  			Sentence s = (Sentence) parser.parse(wff);
  			Set<Sentence> clauses = new CNFClauseGatherer().getClausesFrom(new CNFTransformer().transform(s));
  
  	        //List<Symbol> signature = sConv.setToList(new SymbolClassifier().getSymbolsIn(s));
  	        
  			Vector<BooleanConstraint> cons = new Vector<BooleanConstraint>();
  			for (Sentence cl : clauses) {
  				HashMap<BooleanVariable,Boolean> newClause = new HashMap<BooleanVariable, Boolean>();
  		        List<Symbol> positiveSymbols = sConv.setToList(new SymbolClassifier().getPositiveSymbolsIn(cl));
  		        List<Symbol> negativeSymbols = sConv.setToList(new SymbolClassifier().getNegativeSymbolsIn(cl));
  				try {
  					for (Symbol ps : positiveSymbols) {
  						BooleanVariable bv = scope[Integer.parseInt(ps.toString().substring(1))-1];
  						newClause.put(bv,true);
  					}
  					for (Symbol ns : negativeSymbols) {
  						BooleanVariable bv = scope[Integer.parseInt(ns.toString().substring(1))-1];
  						if (newClause.containsKey(bv)) newClause.remove(bv);
  						else newClause.put(bv, false);
  					}
  				}
  				catch (ArrayIndexOutOfBoundsException e) { throw new Error("Variable numbering in WFF must be within scope"); }
  				catch (NumberFormatException e) { throw new Error("Variables in WFF must be in the format [a-z][1-MAXINT]"); }			
  				if (newClause.size() > 0) {
  					BooleanVariable[] relevantVars = new BooleanVariable[newClause.size()];
  					boolean[] positive = new boolean[newClause.size()];
  					int counter = 0;
  					for (Entry<BooleanVariable, Boolean> ent : newClause.entrySet()) {
  						relevantVars[counter] = ent.getKey();
  						positive[counter++] = ent.getValue();
  					}
  					BooleanConstraint bc = new BooleanConstraint(relevantVars, positive);
  					MetaCSPLogging.getLogger(BooleanConstraint.class).finest("Created constraint " + bc);
  					boolean subsumed = false;
  					for (BooleanConstraint otherBc : cons) {
  						if (bc.isEquivalent(otherBc)) {
  							subsumed = true;
  							break;
  						}
  					}
  					if (!subsumed) cons.add(bc);
  				}
  			}
  			MetaCSPLogging.getLogger(BooleanConstraint.class).finest("CNF(WFF): " + cons);
  			return cons.toArray(new BooleanConstraint[cons.size()]);
  		}
  		catch (java.lang.RuntimeException e) { throw new Error("Malformed BooleanConstraint - allowed logical connectives:\n\t^ : AND\n\tv : OR\n\t-> : implication\n\t<-> : iff\n\t~ : NOT"); }
  	}