final int n = literals.size();

		int y[] = new int[n - 1];

		for (int i = 0; i < n - 1; i++) {
			y[i] = solver.nextFreeVarId(true);
		}

		IVecInt clause = new VecInt();

		// Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
		for (int i = 1; i <= n - 2; i++) {
			clause.push(-y[i]);
			clause.push(y[i - 1]);
			group.add(solver.addClause(clause));
			clause.clear();
		}

		// Constraint \bigwedge_{i=2}{n-1} (\neg y_{i-1} \vee y_i \vee x_i)
		for (int i = 2; i <= n - 1; i++) {
			clause.push(-y[i - 2]);
			clause.push(y[i - 1]);
			clause.push(literals.get(i - 1));
			group.add(solver.addClause(clause));
			clause.clear();
		}

		// Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee y_{i-1)})
		for (int i = 2; i <= n - 1; i++) {
			clause.push(-literals.get(i - 1));
			clause.push(y[i - 2]);
			group.add(solver.addClause(clause));
			clause.clear();
		}

		// Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee \neg y_i)
		for (int i = 2; i <= n - 1; i++) {
			clause.push(-literals.get(i - 1));
			clause.push(-y[i - 1]);
			group.add(solver.addClause(clause));
			clause.clear();
		}

		// Constraint y_1 \vee x_1
		clause.push(y[0]);
		clause.push(literals.get(0));
		group.add(solver.addClause(clause));
		clause.clear();

		// Constraint \neg y_1 \vee \neg x_1
		clause.push(-y[0]);
		clause.push(-literals.get(0));
		group.add(solver.addClause(clause));
		clause.clear();

		// Constraint \neg y_{n-1} \vee x_n
		clause.push(-y[n - 2]);
		clause.push(literals.get(n - 1));

		return constrs.values();
	}

	@Override
	public int[] findModel() throws TimeoutException {
		assump = VecInt.EMPTY;
		IVecInt extraVariables = new VecInt();
		for (Integer p : constrs.keySet()) {
			extraVariables.push(-p);
		}
		return super.findModel(extraVariables);
	}

	@Override
	public int[] findModel(IVecInt assumps) throws TimeoutException {
		assump = assumps;
		IVecInt extraVariables = new VecInt();
		assumps.copyTo(extraVariables);
		for (Integer p : constrs.keySet()) {
			extraVariables.push(-p);
		}
		return super.findModel(extraVariables);
	}

	@Override
	public boolean isSatisfiable() throws TimeoutException {
		assump = VecInt.EMPTY;
		IVecInt extraVariables = new VecInt();
		for (Integer p : constrs.keySet()) {
			extraVariables.push(-p);
		}
		return super.isSatisfiable(extraVariables);
	}

	@Override
	public boolean isSatisfiable(boolean global) throws TimeoutException {
		assump = VecInt.EMPTY;
		IVecInt extraVariables = new VecInt();
		for (Integer p : constrs.keySet()) {
			extraVariables.push(-p);
		}
		return super.isSatisfiable(extraVariables, global);
	}

	@Override
	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
		assump = assumps;
		IVecInt extraVariables = new VecInt();
		assumps.copyTo(extraVariables);
		for (Integer p : constrs.keySet()) {
			extraVariables.push(-p);
		}
		return super.isSatisfiable(extraVariables);
	}

	@Override
	public boolean isSatisfiable(IVecInt assumps, boolean global)
			throws TimeoutException {
		assump = assumps;
		IVecInt extraVariables = new VecInt();
		assumps.copyTo(extraVariables);
		for (Integer p : constrs.keySet()) {
			extraVariables.push(-p);
		}
		return super.isSatisfiable(extraVariables, global);
	}

	@Override
	public int[] model() {
		int[] fullmodel = super.modelWithInternalVariables();

			results.push(-firstExplanation.get(0));
			return results;
		}
		if (solver.isVerbose()) {
			System.out.print(solver.getLogPrefix() + "initial unsat core ");
			firstExplanation.sort();
			for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
				System.out.print(constrs.get(-it.next()));
				System.out.print(" ");
			}
			System.out.println();
		}
		for (int i = 0; i < firstExplanation.size();) {
			if (assumps.contains(firstExplanation.get(i))) {
				firstExplanation.delete(i);
			} else {
				i++;
			}
		}
		Set<Integer> constraintsVariables = constrs.keySet();
		IVecInt remainingVariables = new VecInt(constraintsVariables.size());
		for (Integer v : constraintsVariables) {
			remainingVariables.push(v);
		}
		int p;
		for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
			p = it.next();
			if (p < 0) {
				p = -p;
			}
			remainingVariables.remove(p);
			encodingAssumptions.push(p);
		}

public class QuickXplainStrategy implements MinimizationStrategy {

	private boolean computationCanceled;

	public void cancelExplanationComputation() {
		computationCanceled = true;
	}

	public IVecInt explain(ISolver solver, Map<Integer, ?> constrs,
			IVecInt assumps) throws TimeoutException {
		computationCanceled = false;
		IVecInt encodingAssumptions = new VecInt(constrs.size()
				+ assumps.size());
		assumps.copyTo(encodingAssumptions);
		IVecInt firstExplanation = solver.unsatExplanation();
		IVecInt results = new VecInt(firstExplanation.size());
		if (firstExplanation.size() == 1) {
			results.push(-firstExplanation.get(0));
			return results;
		}
		if (solver.isVerbose()) {
			System.out.print(solver.getLogPrefix() + "initial unsat core ");
			firstExplanation.sort();
			for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
				System.out.print(constrs.get(-it.next()));
				System.out.print(" ");
			}
			System.out.println();

public class MixedDataStructureSingleWL extends AbstractDataStructureFactory {

	private static final long serialVersionUID = 1L;

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * org.sat4j.minisat.DataStructureFactory#createCardinalityConstraint(org
	 * .sat4j.datatype.VecInt, int)
	 */
	@Override
	public Constr createCardinalityConstraint(IVecInt literals, int degree)
			throws ContradictionException {
		return AtLeast.atLeastNew(solver, getVocabulary(), literals, degree);
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype
	 * .VecInt)
	 */
	public Constr createClause(IVecInt literals) throws ContradictionException {
		IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
		if (v == null) {
			// tautological clause
			return null;
		}
		if (v.size() == 1) {
			return new UnitClause(v.last());
		}
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);
	}

	public Constr createUnregisteredClause(IVecInt literals) {

	public Constr createClause(IVecInt literals) throws ContradictionException {
		IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
		if (v == null) {
			// tautological clause
			return null;
		}
		if (v.size() == 1) {
			return new UnitClause(v.last());
		}
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);
	}

	public Constr createUnregisteredClause(IVecInt literals) {
		return new LearntWLClause(literals, getVocabulary());
	}

	@Override
	protected ILits createLits() {
		return new Lits();
	}
}

			System.out.println();
		}
		for (int i = 0; i < firstExplanation.size();) {
			if (assumps.contains(firstExplanation.get(i))) {
				firstExplanation.delete(i);
			} else {
				i++;
			}
		}
		Set<Integer> constraintsVariables = constrs.keySet();
		IVecInt remainingVariables = new VecInt(constraintsVariables.size());
		for (Integer v : constraintsVariables) {
			remainingVariables.push(v);
		}
		int p;
		for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
			p = it.next();
			if (p < 0) {
				p = -p;
			}
			remainingVariables.remove(p);

public class MixedDataStructureDanielWL extends AbstractDataStructureFactory {

	private static final long serialVersionUID = 1L;

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * org.sat4j.minisat.DataStructureFactory#createCardinalityConstraint(org
	 * .sat4j.datatype.VecInt, int)
	 */
	@Override
	public Constr createCardinalityConstraint(IVecInt literals, int degree)
			throws ContradictionException {
		return AtLeast.atLeastNew(solver, getVocabulary(), literals, degree);
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype
	 * .VecInt)
	 */
	public Constr createClause(IVecInt literals) throws ContradictionException {
		IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
		if (v == null) {
			// tautological clause
			return null;
		}
		if (v.size() == 1) {
			return new UnitClause(v.last());
		}
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);

	}

	public void backtracking(int p) {
		// TODO Auto-generated method stub

	}

	public void beginLoop() {
		// TODO Auto-generated method stub

	}

	public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
		// TODO Auto-generated method stub

	}

	public void conflictFound(int p) {
		// TODO Auto-generated method stub

	}

	public void delete(int[] clause) {
		// TODO Auto-generated method stub

	}

	public void end(Lbool result) {
		out.close();

	}

	public void learn(IConstr c) {
		// TODO Auto-generated method stub

	}

	public void propagating(int p, IConstr reason) {
		// TODO Auto-generated method stub

	}

	public void solutionFound() {
		// TODO Auto-generated method stub

	}

	public void start() {
		updateWriter();
	}

	public void restarting() {
		// out.close();
		// restartNumber++;
		// updateWriter();
	}

	public void backjump(int backjumpLevel) {

	}

	@Override
	public String decode(int[] model) {
		StringBuffer stb = new StringBuffer();
		for (int i = 0; i < model.length; i++) {
			stb.append(model[i]);
			stb.append(" ");
		}
		stb.append("0");
		return stb.toString();
	}

	@Override
	public void decode(int[] model, PrintWriter out) {
		for (int i = 0; i < model.length; i++) {
			out.print(model[i]);
			out.print(" ");
		}
		out.print("0");
	}

	AIGReader(ISolver s) {
		solver = new GateTranslator(s);
	}

	@Override
	public String decode(int[] model) {
		StringBuffer stb = new StringBuffer();
		for (int i = 0; i < nbinputs; i++) {
			stb.append(model[i] > 0 ? 1 : 0);
		}
		return stb.toString();
	}

	@Override
	public void decode(int[] model, PrintWriter out) {
		for (int i = 0; i < nbinputs; i++) {
			out.print(model[i] > 0 ? 1 : 0);
		}
	}

	public Constr createClause(IVecInt literals) throws ContradictionException {
		IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), solver);
		if (v == null) {
			// tautological clause
			return null;
		}
		if (v.size() == 1) {
			return new UnitClause(v.last());
		}
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);
	}

	public Constr createUnregisteredClause(IVecInt literals) {

		int[] fullmodel = super.modelWithInternalVariables();
		if (fullmodel == null) {
			return null;
		}
		int[] model = new int[fullmodel.length - constrs.size()];
		int j = 0;
		for (int i = 0; i < fullmodel.length; i++) {
			if (constrs.get(Math.abs(fullmodel[i])) == null) {
				model[j++] = fullmodel[i];
			}
		}
		return model;
	}

	@Override
	public String toString(String prefix) {
		System.out.println(prefix + "Explanation (MUS) enabled solver");

	public LearnedClauseSizeTracing(String filename) {
		this.filename = filename;
		updateWriter();
	}

	private void updateWriter() {
		try {
			out = new PrintStream(new FileOutputStream(filename + ".dat"));
		} catch (FileNotFoundException e) {
			out = System.out;
		}
	}

	public void adding(int p) {
		// TODO Auto-generated method stub

	}

	public void assuming(int p) {

	}

	public void backtracking(int p) {
		// TODO Auto-generated method stub

	}

	public void beginLoop() {
		// TODO Auto-generated method stub

	}

	public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
		out.println(confl.size());