p2/demos/misc-conf-2010/org.eclipse.equinox.p2.cudf/src/main/java/org/eclipse/equinox/p2/cudf/solver/Projector.java - gerrit/equinox/rt.equinox.incubator - Git at Google

 /*******************************************************************************
  * Copyright (c) 2007, 2009 IBM Corporation and others. All rights reserved. This
  * program and the accompanying materials are made available under the terms of
  * the Eclipse Public License v1.0 which accompanies this distribution, and is
  * available at http://www.eclipse.org/legal/epl-v10.html
  *
  * Contributors: IBM Corporation - initial API and implementation
  * Daniel Le Berre - Fix in the encoding and the optimization function
  * Alban Browaeys - Optimized string concatenation in bug 251357
  * Jed Anderson - switch from opb files to API calls to DependencyHelper in bug 200380
  ******************************************************************************/
 package org.eclipse.equinox.p2.cudf.solver;

 import java.io.PrintWriter;
 import java.util.*;
 import org.eclipse.core.runtime.*;
 import org.eclipse.core.runtime.jobs.Job;
 import org.eclipse.equinox.p2.cudf.Log;
 import org.eclipse.equinox.p2.cudf.Main;
 import org.eclipse.equinox.p2.cudf.metadata.*;
 import org.eclipse.equinox.p2.cudf.query.*;
 import org.eclipse.osgi.util.NLS;
 import org.sat4j.minisat.restarts.LubyRestarts;
 import org.sat4j.pb.*;
 import org.sat4j.pb.core.PBSolverResolution;
 import org.sat4j.pb.tools.LexicoHelper;
 import org.sat4j.pb.tools.WeightedObject;
 import org.sat4j.specs.*;

 /**
  * This class is the interface between SAT4J and the planner. It produces a
  * boolean satisfiability problem, invokes the solver, and converts the solver result
  * back into information understandable by the planner.
  */
 public class Projector {
 	private static final boolean DEBUG = false; //SET THIS TO FALSE FOR THE COMPETITION
 	private static final boolean TIMING = false; //SET THIS TO FALSE FOR THE COMPETITION
 	private static final boolean DEBUG_ENCODING = false; //SET THIS TO FALSE FOR THE COMPETITION
 	private static final boolean PURGE = true;

 	private QueryableArray picker;

 	private Map noopVariables; //key IU, value AbstractVariable
 	private List abstractVariables;

 	private TwoTierMap slice; //The IUs that have been considered to be part of the problem

 	LexicoHelper dependencyHelper;
 	private Collection solution;
 	private Collection assumptions;

 	private MultiStatus result;

 	private InstallableUnit entryPoint;

 	private SolverConfiguration configuration;
 	private OptimizationFunction optFunction;

 	private List optionalityVariables;
 	private List optionalityPairs;

 	static class AbstractVariable {
 		private String str;

 		AbstractVariable() {
 			// no value for str
 		}

 		AbstractVariable(String str) {
 			this.str = str;
 		}

 		public String toString() {
 			return "AbstractVariable: " + (str == null ? "" + hashCode() : str); //$NON-NLS-1$
 		}
 	}

 	public Projector(QueryableArray q) {
 		picker = q;
 		noopVariables = new HashMap();
 		slice = new TwoTierMap(q.getSize(), TwoTierMap.POLICY_BOTH_MAPS_PRESERVE_ORDERING);
 		abstractVariables = new ArrayList();
 		result = new MultiStatus(Main.PLUGIN_ID, IStatus.OK, Messages.Planner_Problems_resolving_plan, null);
 		assumptions = new ArrayList();
 		optionalityVariables = new ArrayList();
 		optionalityPairs = new ArrayList();
 	}

 	private void purgeIU(InstallableUnit iu) {
 		if (PURGE) {
 			iu.setCapabilities(InstallableUnit.NO_PROVIDES);
 			iu.setRequiredCapabilities(InstallableUnit.NO_REQUIRES);
 		}
 	}

 	public void encode(InstallableUnit entryPointIU, SolverConfiguration conf) {
 		this.configuration = conf;
 		this.entryPoint = entryPointIU;
 		solution = null;
 		try {
 			long start = 0;
 			if (TIMING) {
 				start = System.currentTimeMillis();
 				Tracing.debug("Starting projection ... "); //$NON-NLS-1$
 			}
 			IPBSolver solver;
 			if (DEBUG_ENCODING) {
 				solver = new UserFriendlyPBStringSolver(); //.newOPBStringSolver();
 			} else if (conf.encoding) {
 				solver = SolverFactory.newOPBStringSolver();
 			} else {
 				PBSolverResolution mysolver = SolverFactory.newCompetPBResLongWLMixedConstraintsObjectiveExpSimp();
 				mysolver.setSimplifier(mysolver.SIMPLE_SIMPLIFICATION);
 				mysolver.setRestartStrategy(new LubyRestarts(512));
 				// mysolver.setLearnedConstraintsDeletionStrategy(mysolver.memory_based);
 				// mysolver.setSearchListener(new DecisionTracing("/tmp/rand992.dat"));
 				solver = mysolver; // SolverFactory.newResolutionGlucoseSimpleSimp();// SolverFactory.newEclipseP2();
 			}
 			if ("default".equals(configuration.timeout)) {
 				solver.setTimeout(300); // 5 minutes
 			} else {
 				int number = Integer.valueOf(configuration.timeout.substring(0, configuration.timeout.length() - 1)).intValue();
 				if (configuration.timeout.endsWith("s")) {
 					solver.setTimeout(number);
 				} else {
 					solver.setTimeoutOnConflicts(number);
 				}
 			}
 			solver.setVerbose(configuration.verbose);
 			solver.setLogPrefix("# ");
 			Log.printlnNoPrefix(solver.toString("# "));
 			dependencyHelper = new LexicoHelper(solver, conf.explain);
 			if (DEBUG_ENCODING) {
 				((UserFriendlyPBStringSolver) solver).setMapping(dependencyHelper.getMappingToDomain());
 			}
 			Iterator iusToEncode = picker.iterator();
 			List iusToOrder = new ArrayList(picker.getSize());
 			while (iusToEncode.hasNext()) {
 				iusToOrder.add(iusToEncode.next());
 			}
 			Collections.sort(iusToOrder);
 			iusToEncode = iusToOrder.iterator();
 			while (iusToEncode.hasNext()) {
 				InstallableUnit iuToEncode = (InstallableUnit) iusToEncode.next();
 				if (iuToEncode != entryPointIU) {
 					processIU(iuToEncode, false);
 				}
 			}
 			createConstraintsForSingleton();

 			createMustHave(entryPointIU);

 			optFunction = getOptimizationFactory(configuration.objective);
 			setObjectiveFunction(optFunction.createOptimizationFunction(entryPointIU));
 			if (TIMING) {
 				Tracing.debug("Objective function contains " + solver.getObjectiveFunction().getVars().size() + " literals");
 				long stop = System.currentTimeMillis();
 				Tracing.debug("Projection completed: " + (stop - start) + "ms."); //$NON-NLS-1$
 			}
 			if (DEBUG_ENCODING) {
 				Log.println(solver.toString());
 			}
 		} catch (IllegalStateException e) {
 			result.add(new Status(IStatus.ERROR, Main.PLUGIN_ID, e.getMessage(), e));
 			if (configuration.verbose) {
 				Log.println("*** PBM *** " + e.getMessage());
 			}
 		} catch (ContradictionException e) {
 			result.add(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unsatisfiable_problem));
 			if (configuration.verbose) {
 				Log.println("Unsat OPB problem ");
 			}
 		}
 	}

 	private OptimizationFunction getOptimizationFactory(String optFunctionName) {
 		OptimizationFunction function = null;
 		function = new UserDefinedOptimizationFunction2012(optFunctionName);
 		Log.println("Optimization function: " + function.getName());
 		function.slice = slice;
 		function.noopVariables = noopVariables;
 		function.picker = picker;
 		function.dependencyHelper = dependencyHelper;
 		function.optionalityVariables = optionalityVariables;
 		function.optionalityPairs = optionalityPairs;
 		return function;
 	}

 	private void setObjectiveFunction(List weightedObjects) {
 		if (weightedObjects == null)
 			return;
 		if (DEBUG) {
 			StringBuffer b = new StringBuffer();
 			for (Iterator i = weightedObjects.iterator(); i.hasNext();) {
 				WeightedObject object = (WeightedObject) i.next();
 				if (b.length() > 0)
 					b.append(", "); //$NON-NLS-1$
 				b.append(object.getWeight());
 				b.append(' ');
 				b.append(object.thing);
 			}
 			Tracing.debug("objective function: " + b); //$NON-NLS-1$
 		}
 		dependencyHelper.setObjectiveFunction((WeightedObject[]) weightedObjects.toArray(new WeightedObject[weightedObjects.size()]));
 	}

 	private void createMustHave(InstallableUnit iu) throws ContradictionException {
 		processIU(iu, true);
 		if (DEBUG) {
 			Tracing.debug(iu + "=1"); //$NON-NLS-1$
 		}
 		dependencyHelper.setTrue(iu, new Explanation.IUToInstall(iu));
 		// assumptions.add(iu);
 	}

 	private void createNegation(InstallableUnit iu, IRequiredCapability req) throws ContradictionException {
 		if (DEBUG) {
 			Tracing.debug(iu + "=0"); //$NON-NLS-1$
 		}
 		dependencyHelper.setFalse(iu, new Explanation.MissingIU(iu, req));
 	}

 	private void expandNegatedRequirement(IRequiredCapability req, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
 		IRequiredCapability negatedReq = ((NotRequirement) req).getRequirement();
 		List matches = getApplicableMatches(negatedReq);
 		matches.remove(iu);
 		if (matches.isEmpty()) {
 			return;
 		}
 		Explanation explanation;
 		if (isRootIu) {
 			InstallableUnit reqIu = (InstallableUnit) matches.iterator().next();
 			explanation = new Explanation.IUToInstall(reqIu);
 		} else {
 			explanation = new Explanation.HardRequirement(iu, req);
 		}
 		createNegationImplication(iu, matches, explanation);
 	}

 	private void expandRequirement(IRequiredCapability req, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
 		if (req.isNegation()) {
 			expandNegatedRequirement(req, iu, isRootIu);
 			return;
 		}
 		List matches = getApplicableMatches(req);
 		if (!req.isOptional()) {
 			if (matches.isEmpty()) {
 				missingRequirement(iu, req);
 			} else {
 				if (req.getArity() == 1) {
 					createAtMostOne((InstallableUnit[]) matches.toArray(new InstallableUnit[matches.size()]));
 					return;
 				}
 				InstallableUnit reqIu = (InstallableUnit) matches.iterator().next();
 				Explanation explanation = new Explanation.IUToInstall(reqIu);
 				createImplication(iu, matches, explanation);
 			}
 		} else {
 			AbstractVariable abs = getAbstractVariable(iu.toString() + "->" + req.toString());
 			matches.add(abs);
 			createImplication(iu, matches, Explanation.OPTIONAL_REQUIREMENT);
 			optionalityVariables.add(abs);
 			optionalityPairs.add(new Pair(iu, abs));
 		}
 	}

 	private void expandRequirements(IRequiredCapability[] reqs, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
 		if (reqs.length == 0) {
 			return;
 		}
 		for (int i = 0; i < reqs.length; i++) {
 			expandRequirement(reqs[i], iu, isRootIu);
 		}
 	}

 	public void processIU(InstallableUnit iu, boolean isRootIU) throws ContradictionException {
 		slice.put(iu.getId(), iu.getVersion(), iu);
 		expandRequirements(getRequiredCapabilities(iu), iu, isRootIU);
 	}

 	private IRequiredCapability[] getRequiredCapabilities(InstallableUnit iu) {
 		return iu.getRequiredCapabilities();
 	}

 	private void missingRequirement(InstallableUnit iu, IRequiredCapability req) throws ContradictionException {
 		result.add(new Status(IStatus.WARNING, Main.PLUGIN_ID, NLS.bind(Messages.Planner_Unsatisfied_dependency, iu, req)));
 		createNegation(iu, req);
 	}

 	/**
 	 * @param req
 	 * @return a list of mandatory requirements if any, an empty list if req.isOptional().
 	 */
 	private List getApplicableMatches(IRequiredCapability req) {
 		List target = new ArrayList();
 		Collector matches = picker.query(new CapabilityQuery(req), new Collector(), null);
 		for (Iterator iterator = matches.iterator(); iterator.hasNext();) {
 			InstallableUnit match = (InstallableUnit) iterator.next();
 			target.add(match);
 		}
 		return target;
 	}

 	//This will create as many implication as there is element in the right argument
 	private void createNegationImplication(Object left, List right, Explanation name) throws ContradictionException {
 		if (DEBUG) {
 			Tracing.debug(name + ": " + left + "->" + right); //$NON-NLS-1$ //$NON-NLS-2$
 		}
 		for (Iterator iterator = right.iterator(); iterator.hasNext();) {
 			dependencyHelper.implication(new Object[] {left}).impliesNot(iterator.next()).named(name);
 		}

 	}

 	private void createImplication(Object left, List right, Explanation name) throws ContradictionException {
 		if (DEBUG) {
 			Tracing.debug(name + ": " + left + "->" + right); //$NON-NLS-1$ //$NON-NLS-2$
 		}
 		dependencyHelper.implication(new Object[] {left}).implies(right.toArray()).named(name);
 	}

 	//Create constraints to deal with singleton
 	//When there is a mix of singleton and non singleton, several constraints are generated
 	private void createConstraintsForSingleton() throws ContradictionException {
 		Set s = slice.entrySet();
 		for (Iterator iterator = s.iterator(); iterator.hasNext();) {
 			Map.Entry entry = (Map.Entry) iterator.next();
 			HashMap conflictingEntries = (HashMap) entry.getValue();
 			if (conflictingEntries.size() < 2)
 				continue;

 			Collection conflictingVersions = conflictingEntries.values();
 			List singletons = new ArrayList();
 			List nonSingletons = new ArrayList();
 			for (Iterator conflictIterator = conflictingVersions.iterator(); conflictIterator.hasNext();) {
 				InstallableUnit iu = (InstallableUnit) conflictIterator.next();
 				if (iu.isSingleton()) {
 					singletons.add(iu);
 				} else {
 					nonSingletons.add(iu);
 				}
 			}
 			if (singletons.isEmpty())
 				continue;

 			InstallableUnit[] singletonArray;
 			if (nonSingletons.isEmpty()) {
 				singletonArray = (InstallableUnit[]) singletons.toArray(new InstallableUnit[singletons.size()]);
 				createAtMostOne(singletonArray);
 			} else {
 				singletonArray = (InstallableUnit[]) singletons.toArray(new InstallableUnit[singletons.size() + 1]);
 				for (Iterator iterator2 = nonSingletons.iterator(); iterator2.hasNext();) {
 					singletonArray[singletonArray.length - 1] = (InstallableUnit) iterator2.next();
 					createAtMostOne(singletonArray);
 				}
 			}
 		}
 	}

 	private void createAtMostOne(InstallableUnit[] ius) throws ContradictionException {
 		if (DEBUG) {
 			StringBuffer b = new StringBuffer();
 			for (int i = 0; i < ius.length; i++) {
 				b.append(ius[i].toString());
 			}
 			Tracing.debug("At most 1 of " + b); //$NON-NLS-1$
 		}
 		dependencyHelper.atMost(1, ius).named(new Explanation.Singleton(ius));
 	}

 	private AbstractVariable getAbstractVariable(String name) {
 		AbstractVariable abstractVariable = new AbstractVariable(name);
 		abstractVariables.add(abstractVariable);
 		return abstractVariable;
 	}

 	private void purge() {
 		if (PURGE) {
 			Iterator iusToEncode = picker.iterator();
 			while (iusToEncode.hasNext()) {
 				purgeIU((InstallableUnit) iusToEncode.next());
 			}

 			picker = null;
 			noopVariables = null;
 			abstractVariables = null;
 			slice = null;
 			//		assumptions = null;
 		}
 	}

 	private boolean isSatisfiable;

 	public IStatus invokeSolver() {
 		purge();
 		isSatisfiable = false;
 		if (result.getSeverity() == IStatus.ERROR)
 			return result;
 		// CNF filename is given on the command line
 		long start = System.currentTimeMillis();
 		if (TIMING)
 			Tracing.debug("Invoking solver ..."); //$NON-NLS-1$
 		try {
 			Log.println("p cnf " + dependencyHelper.getSolver().nVars() + " " + dependencyHelper.getSolver().nConstraints());
 			if (dependencyHelper.hasASolution(assumptions)) {
 				isSatisfiable = true;
 				if (DEBUG) {
 					Tracing.debug("Satisfiable !"); //$NON-NLS-1$
 				}
 				if (TIMING)
 					Tracing.debug("Solver first solution found: " + (System.currentTimeMillis() - start) + "ms."); //$NON-NLS-1$
 				backToIU();
 				long stop = System.currentTimeMillis();
 				if (TIMING)
 					Tracing.debug("Solver best solution decoded: " + (stop - start) + "ms."); //$NON-NLS-1$
 				if (configuration.verbose)
 					dependencyHelper.getSolver().printStat(new PrintWriter(System.out, true), "# ");
 			} else {
 				long stop = System.currentTimeMillis();
 				if (DEBUG) {
 					Tracing.debug("Unsatisfiable !"); //$NON-NLS-1$
 					Tracing.debug("Solver solution NOT found: " + (stop - start)); //$NON-NLS-1$
 				}
 				result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unsatisfiable_problem));
 			}
 		} catch (TimeoutException e) {
 			result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Timeout));
 			if (configuration.verbose) {
 				Log.println("Timeout reached");
 			}
 		} catch (Exception e) {
 			result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unexpected_problem, e));
 			if (configuration.verbose) {
 				Log.println("*** PBM *** " + e.getMessage());
 			}
 		}
 		return result;
 	}

 	private void backToIU() {
 		solution = null;
 		if (!isSatisfiable)
 			return;
 		solution = new ArrayList();
 		IVec sat4jSolution = dependencyHelper.getSolution();
 		if (sat4jSolution.isEmpty())
 			return;
 		if (configuration.verbose && optFunction != null)
 			optFunction.printSolutionValue();
 		for (Iterator i = sat4jSolution.iterator(); i.hasNext();) {
 			Object var = i.next();
 			if (var instanceof InstallableUnit) {
 				InstallableUnit iu = (InstallableUnit) var;
 				if (iu == entryPoint)
 					continue;
 				solution.add(iu);
 			}
 		}
 	}

 	private void printSolution(Collection state) {
 		ArrayList l = new ArrayList(state);
 		Collections.sort(l);
 		Tracing.debug("Solution:"); //$NON-NLS-1$
 		Tracing.debug("Numbers of IUs selected: " + l.size()); //$NON-NLS-1$
 		for (Iterator iterator = l.iterator(); iterator.hasNext();) {
 			Tracing.debug(iterator.next().toString());
 		}
 	}

 	public Collection extractSolution() {
 		if (DEBUG)
 			printSolution(solution);
 		return solution;
 	}

 	public Set getExplanation() {
 		ExplanationJob job = new ExplanationJob(dependencyHelper);
 		job.schedule();
 		IProgressMonitor pm = new NullProgressMonitor();
 		pm.beginTask(Messages.Planner_NoSolution, 1000);
 		try {
 			synchronized (job) {
 				while (job.getExplanationResult() == null && job.getState() != Job.NONE) {
 					if (pm.isCanceled()) {
 						job.cancel();
 						throw new OperationCanceledException();
 					}
 					pm.worked(1);
 					try {
 						job.wait(100);
 					} catch (InterruptedException e) {
 						if (DEBUG)
 							Tracing.debug("Interrupted while computing explanations"); //$NON-NLS-1$
 					}
 				}
 			}
 		} finally {
 			pm.done();
 		}
 		return job.getExplanationResult();
 	}

 	public void stopSolver() {
 		if (dependencyHelper != null)
 			dependencyHelper.stopSolver();
 	}

 	public Collection getBestSolutionFoundSoFar() {
 		if (solution == null) {
 			backToIU();
 		}
 		if (solution == null)
 			return null;
 		return extractSolution();
 	}
 }
	/*******************************************************************************
	* Copyright (c) 2007, 2009 IBM Corporation and others. All rights reserved. This
	* program and the accompanying materials are made available under the terms of
	* the Eclipse Public License v1.0 which accompanies this distribution, and is
	* available at http://www.eclipse.org/legal/epl-v10.html
	*
	* Contributors: IBM Corporation - initial API and implementation
	* Daniel Le Berre - Fix in the encoding and the optimization function
	* Alban Browaeys - Optimized string concatenation in bug 251357
	* Jed Anderson - switch from opb files to API calls to DependencyHelper in bug 200380
	******************************************************************************/
	package org.eclipse.equinox.p2.cudf.solver;

	import java.io.PrintWriter;
	import java.util.*;
	import org.eclipse.core.runtime.*;
	import org.eclipse.core.runtime.jobs.Job;
	import org.eclipse.equinox.p2.cudf.Log;
	import org.eclipse.equinox.p2.cudf.Main;
	import org.eclipse.equinox.p2.cudf.metadata.*;
	import org.eclipse.equinox.p2.cudf.query.*;
	import org.eclipse.osgi.util.NLS;
	import org.sat4j.minisat.restarts.LubyRestarts;
	import org.sat4j.pb.*;
	import org.sat4j.pb.core.PBSolverResolution;
	import org.sat4j.pb.tools.LexicoHelper;
	import org.sat4j.pb.tools.WeightedObject;
	import org.sat4j.specs.*;

	/**
	* This class is the interface between SAT4J and the planner. It produces a
	* boolean satisfiability problem, invokes the solver, and converts the solver result
	* back into information understandable by the planner.
	*/
	public class Projector {
	private static final boolean DEBUG = false; //SET THIS TO FALSE FOR THE COMPETITION
	private static final boolean TIMING = false; //SET THIS TO FALSE FOR THE COMPETITION
	private static final boolean DEBUG_ENCODING = false; //SET THIS TO FALSE FOR THE COMPETITION
	private static final boolean PURGE = true;

	private QueryableArray picker;

	private Map noopVariables; //key IU, value AbstractVariable
	private List abstractVariables;

	private TwoTierMap slice; //The IUs that have been considered to be part of the problem

	LexicoHelper dependencyHelper;
	private Collection solution;
	private Collection assumptions;

	private MultiStatus result;

	private InstallableUnit entryPoint;

	private SolverConfiguration configuration;
	private OptimizationFunction optFunction;

	private List optionalityVariables;
	private List optionalityPairs;

	static class AbstractVariable {
	private String str;

	AbstractVariable() {
	// no value for str
	}

	AbstractVariable(String str) {
	this.str = str;
	}

	public String toString() {
	return "AbstractVariable: " + (str == null ? "" + hashCode() : str); //$NON-NLS-1$
	}
	}

	public Projector(QueryableArray q) {
	picker = q;
	noopVariables = new HashMap();
	slice = new TwoTierMap(q.getSize(), TwoTierMap.POLICY_BOTH_MAPS_PRESERVE_ORDERING);
	abstractVariables = new ArrayList();
	result = new MultiStatus(Main.PLUGIN_ID, IStatus.OK, Messages.Planner_Problems_resolving_plan, null);
	assumptions = new ArrayList();
	optionalityVariables = new ArrayList();
	optionalityPairs = new ArrayList();
	}

	private void purgeIU(InstallableUnit iu) {
	if (PURGE) {
	iu.setCapabilities(InstallableUnit.NO_PROVIDES);
	iu.setRequiredCapabilities(InstallableUnit.NO_REQUIRES);
	}
	}

	public void encode(InstallableUnit entryPointIU, SolverConfiguration conf) {
	this.configuration = conf;
	this.entryPoint = entryPointIU;
	solution = null;
	try {
	long start = 0;
	if (TIMING) {
	start = System.currentTimeMillis();
	Tracing.debug("Starting projection ... "); //$NON-NLS-1$
	}
	IPBSolver solver;
	if (DEBUG_ENCODING) {
	solver = new UserFriendlyPBStringSolver(); //.newOPBStringSolver();
	} else if (conf.encoding) {
	solver = SolverFactory.newOPBStringSolver();
	} else {
	PBSolverResolution mysolver = SolverFactory.newCompetPBResLongWLMixedConstraintsObjectiveExpSimp();
	mysolver.setSimplifier(mysolver.SIMPLE_SIMPLIFICATION);
	mysolver.setRestartStrategy(new LubyRestarts(512));
	// mysolver.setLearnedConstraintsDeletionStrategy(mysolver.memory_based);
	// mysolver.setSearchListener(new DecisionTracing("/tmp/rand992.dat"));
	solver = mysolver; // SolverFactory.newResolutionGlucoseSimpleSimp();// SolverFactory.newEclipseP2();
	}
	if ("default".equals(configuration.timeout)) {
	solver.setTimeout(300); // 5 minutes
	} else {
	int number = Integer.valueOf(configuration.timeout.substring(0, configuration.timeout.length() - 1)).intValue();
	if (configuration.timeout.endsWith("s")) {
	solver.setTimeout(number);
	} else {
	solver.setTimeoutOnConflicts(number);
	}
	}
	solver.setVerbose(configuration.verbose);
	solver.setLogPrefix("# ");
	Log.printlnNoPrefix(solver.toString("# "));
	dependencyHelper = new LexicoHelper(solver, conf.explain);
	if (DEBUG_ENCODING) {
	((UserFriendlyPBStringSolver) solver).setMapping(dependencyHelper.getMappingToDomain());
	}
	Iterator iusToEncode = picker.iterator();
	List iusToOrder = new ArrayList(picker.getSize());
	while (iusToEncode.hasNext()) {
	iusToOrder.add(iusToEncode.next());
	}
	Collections.sort(iusToOrder);
	iusToEncode = iusToOrder.iterator();
	while (iusToEncode.hasNext()) {
	InstallableUnit iuToEncode = (InstallableUnit) iusToEncode.next();
	if (iuToEncode != entryPointIU) {
	processIU(iuToEncode, false);
	}
	}
	createConstraintsForSingleton();

	createMustHave(entryPointIU);

	optFunction = getOptimizationFactory(configuration.objective);
	setObjectiveFunction(optFunction.createOptimizationFunction(entryPointIU));
	if (TIMING) {
	Tracing.debug("Objective function contains " + solver.getObjectiveFunction().getVars().size() + " literals");
	long stop = System.currentTimeMillis();
	Tracing.debug("Projection completed: " + (stop - start) + "ms."); //$NON-NLS-1$
	}
	if (DEBUG_ENCODING) {
	Log.println(solver.toString());
	}
	} catch (IllegalStateException e) {
	result.add(new Status(IStatus.ERROR, Main.PLUGIN_ID, e.getMessage(), e));
	if (configuration.verbose) {
	Log.println("* PBM * " + e.getMessage());
	}
	} catch (ContradictionException e) {
	result.add(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unsatisfiable_problem));
	if (configuration.verbose) {
	Log.println("Unsat OPB problem ");
	}
	}
	}

	private OptimizationFunction getOptimizationFactory(String optFunctionName) {
	OptimizationFunction function = null;
	function = new UserDefinedOptimizationFunction2012(optFunctionName);
	Log.println("Optimization function: " + function.getName());
	function.slice = slice;
	function.noopVariables = noopVariables;
	function.picker = picker;
	function.dependencyHelper = dependencyHelper;
	function.optionalityVariables = optionalityVariables;
	function.optionalityPairs = optionalityPairs;
	return function;
	}

	private void setObjectiveFunction(List weightedObjects) {
	if (weightedObjects == null)
	return;
	if (DEBUG) {
	StringBuffer b = new StringBuffer();
	for (Iterator i = weightedObjects.iterator(); i.hasNext();) {
	WeightedObject object = (WeightedObject) i.next();
	if (b.length() > 0)
	b.append(", "); //$NON-NLS-1$
	b.append(object.getWeight());
	b.append(' ');
	b.append(object.thing);
	}
	Tracing.debug("objective function: " + b); //$NON-NLS-1$
	}
	dependencyHelper.setObjectiveFunction((WeightedObject[]) weightedObjects.toArray(new WeightedObject[weightedObjects.size()]));
	}

	private void createMustHave(InstallableUnit iu) throws ContradictionException {
	processIU(iu, true);
	if (DEBUG) {
	Tracing.debug(iu + "=1"); //$NON-NLS-1$
	}
	dependencyHelper.setTrue(iu, new Explanation.IUToInstall(iu));
	// assumptions.add(iu);
	}

	private void createNegation(InstallableUnit iu, IRequiredCapability req) throws ContradictionException {
	if (DEBUG) {
	Tracing.debug(iu + "=0"); //$NON-NLS-1$
	}
	dependencyHelper.setFalse(iu, new Explanation.MissingIU(iu, req));
	}

	private void expandNegatedRequirement(IRequiredCapability req, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
	IRequiredCapability negatedReq = ((NotRequirement) req).getRequirement();
	List matches = getApplicableMatches(negatedReq);
	matches.remove(iu);
	if (matches.isEmpty()) {
	return;
	}
	Explanation explanation;
	if (isRootIu) {
	InstallableUnit reqIu = (InstallableUnit) matches.iterator().next();
	explanation = new Explanation.IUToInstall(reqIu);
	} else {
	explanation = new Explanation.HardRequirement(iu, req);
	}
	createNegationImplication(iu, matches, explanation);
	}

	private void expandRequirement(IRequiredCapability req, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
	if (req.isNegation()) {
	expandNegatedRequirement(req, iu, isRootIu);
	return;
	}
	List matches = getApplicableMatches(req);
	if (!req.isOptional()) {
	if (matches.isEmpty()) {
	missingRequirement(iu, req);
	} else {
	if (req.getArity() == 1) {
	createAtMostOne((InstallableUnit[]) matches.toArray(new InstallableUnit[matches.size()]));
	return;
	}
	InstallableUnit reqIu = (InstallableUnit) matches.iterator().next();
	Explanation explanation = new Explanation.IUToInstall(reqIu);
	createImplication(iu, matches, explanation);
	}
	} else {
	AbstractVariable abs = getAbstractVariable(iu.toString() + "->" + req.toString());
	matches.add(abs);
	createImplication(iu, matches, Explanation.OPTIONAL_REQUIREMENT);
	optionalityVariables.add(abs);
	optionalityPairs.add(new Pair(iu, abs));
	}
	}

	private void expandRequirements(IRequiredCapability[] reqs, InstallableUnit iu, boolean isRootIu) throws ContradictionException {
	if (reqs.length == 0) {
	return;
	}
	for (int i = 0; i < reqs.length; i++) {
	expandRequirement(reqs[i], iu, isRootIu);
	}
	}

	public void processIU(InstallableUnit iu, boolean isRootIU) throws ContradictionException {
	slice.put(iu.getId(), iu.getVersion(), iu);
	expandRequirements(getRequiredCapabilities(iu), iu, isRootIU);
	}

	private IRequiredCapability[] getRequiredCapabilities(InstallableUnit iu) {
	return iu.getRequiredCapabilities();
	}

	private void missingRequirement(InstallableUnit iu, IRequiredCapability req) throws ContradictionException {
	result.add(new Status(IStatus.WARNING, Main.PLUGIN_ID, NLS.bind(Messages.Planner_Unsatisfied_dependency, iu, req)));
	createNegation(iu, req);
	}

	/**
	* @param req
	* @return a list of mandatory requirements if any, an empty list if req.isOptional().
	*/
	private List getApplicableMatches(IRequiredCapability req) {
	List target = new ArrayList();
	Collector matches = picker.query(new CapabilityQuery(req), new Collector(), null);
	for (Iterator iterator = matches.iterator(); iterator.hasNext();) {
	InstallableUnit match = (InstallableUnit) iterator.next();
	target.add(match);
	}
	return target;
	}

	//This will create as many implication as there is element in the right argument
	private void createNegationImplication(Object left, List right, Explanation name) throws ContradictionException {
	if (DEBUG) {
	Tracing.debug(name + ": " + left + "->" + right); //$NON-NLS-1$ //$NON-NLS-2$
	}
	for (Iterator iterator = right.iterator(); iterator.hasNext();) {
	dependencyHelper.implication(new Object[] {left}).impliesNot(iterator.next()).named(name);
	}

	}

	private void createImplication(Object left, List right, Explanation name) throws ContradictionException {
	if (DEBUG) {
	Tracing.debug(name + ": " + left + "->" + right); //$NON-NLS-1$ //$NON-NLS-2$
	}
	dependencyHelper.implication(new Object[] {left}).implies(right.toArray()).named(name);
	}

	//Create constraints to deal with singleton
	//When there is a mix of singleton and non singleton, several constraints are generated
	private void createConstraintsForSingleton() throws ContradictionException {
	Set s = slice.entrySet();
	for (Iterator iterator = s.iterator(); iterator.hasNext();) {
	Map.Entry entry = (Map.Entry) iterator.next();
	HashMap conflictingEntries = (HashMap) entry.getValue();
	if (conflictingEntries.size() < 2)
	continue;

	Collection conflictingVersions = conflictingEntries.values();
	List singletons = new ArrayList();
	List nonSingletons = new ArrayList();
	for (Iterator conflictIterator = conflictingVersions.iterator(); conflictIterator.hasNext();) {
	InstallableUnit iu = (InstallableUnit) conflictIterator.next();
	if (iu.isSingleton()) {
	singletons.add(iu);
	} else {
	nonSingletons.add(iu);
	}
	}
	if (singletons.isEmpty())
	continue;

	InstallableUnit[] singletonArray;
	if (nonSingletons.isEmpty()) {
	singletonArray = (InstallableUnit[]) singletons.toArray(new InstallableUnit[singletons.size()]);
	createAtMostOne(singletonArray);
	} else {
	singletonArray = (InstallableUnit[]) singletons.toArray(new InstallableUnit[singletons.size() + 1]);
	for (Iterator iterator2 = nonSingletons.iterator(); iterator2.hasNext();) {
	singletonArray[singletonArray.length - 1] = (InstallableUnit) iterator2.next();
	createAtMostOne(singletonArray);
	}
	}
	}
	}

	private void createAtMostOne(InstallableUnit[] ius) throws ContradictionException {
	if (DEBUG) {
	StringBuffer b = new StringBuffer();
	for (int i = 0; i < ius.length; i++) {
	b.append(ius[i].toString());
	}
	Tracing.debug("At most 1 of " + b); //$NON-NLS-1$
	}
	dependencyHelper.atMost(1, ius).named(new Explanation.Singleton(ius));
	}

	private AbstractVariable getAbstractVariable(String name) {
	AbstractVariable abstractVariable = new AbstractVariable(name);
	abstractVariables.add(abstractVariable);
	return abstractVariable;
	}

	private void purge() {
	if (PURGE) {
	Iterator iusToEncode = picker.iterator();
	while (iusToEncode.hasNext()) {
	purgeIU((InstallableUnit) iusToEncode.next());
	}

	picker = null;
	noopVariables = null;
	abstractVariables = null;
	slice = null;
	// assumptions = null;
	}
	}

	private boolean isSatisfiable;

	public IStatus invokeSolver() {
	purge();
	isSatisfiable = false;
	if (result.getSeverity() == IStatus.ERROR)
	return result;
	// CNF filename is given on the command line
	long start = System.currentTimeMillis();
	if (TIMING)
	Tracing.debug("Invoking solver ..."); //$NON-NLS-1$
	try {
	Log.println("p cnf " + dependencyHelper.getSolver().nVars() + " " + dependencyHelper.getSolver().nConstraints());
	if (dependencyHelper.hasASolution(assumptions)) {
	isSatisfiable = true;
	if (DEBUG) {
	Tracing.debug("Satisfiable !"); //$NON-NLS-1$
	}
	if (TIMING)
	Tracing.debug("Solver first solution found: " + (System.currentTimeMillis() - start) + "ms."); //$NON-NLS-1$
	backToIU();
	long stop = System.currentTimeMillis();
	if (TIMING)
	Tracing.debug("Solver best solution decoded: " + (stop - start) + "ms."); //$NON-NLS-1$
	if (configuration.verbose)
	dependencyHelper.getSolver().printStat(new PrintWriter(System.out, true), "# ");
	} else {
	long stop = System.currentTimeMillis();
	if (DEBUG) {
	Tracing.debug("Unsatisfiable !"); //$NON-NLS-1$
	Tracing.debug("Solver solution NOT found: " + (stop - start)); //$NON-NLS-1$
	}
	result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unsatisfiable_problem));
	}
	} catch (TimeoutException e) {
	result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Timeout));
	if (configuration.verbose) {
	Log.println("Timeout reached");
	}
	} catch (Exception e) {
	result.merge(new Status(IStatus.ERROR, Main.PLUGIN_ID, Messages.Planner_Unexpected_problem, e));
	if (configuration.verbose) {
	Log.println("* PBM * " + e.getMessage());
	}
	}
	return result;
	}

	private void backToIU() {
	solution = null;
	if (!isSatisfiable)
	return;
	solution = new ArrayList();
	IVec sat4jSolution = dependencyHelper.getSolution();
	if (sat4jSolution.isEmpty())
	return;
	if (configuration.verbose && optFunction != null)
	optFunction.printSolutionValue();
	for (Iterator i = sat4jSolution.iterator(); i.hasNext();) {
	Object var = i.next();
	if (var instanceof InstallableUnit) {
	InstallableUnit iu = (InstallableUnit) var;
	if (iu == entryPoint)
	continue;
	solution.add(iu);
	}
	}
	}

	private void printSolution(Collection state) {
	ArrayList l = new ArrayList(state);
	Collections.sort(l);
	Tracing.debug("Solution:"); //$NON-NLS-1$
	Tracing.debug("Numbers of IUs selected: " + l.size()); //$NON-NLS-1$
	for (Iterator iterator = l.iterator(); iterator.hasNext();) {
	Tracing.debug(iterator.next().toString());
	}
	}

	public Collection extractSolution() {
	if (DEBUG)
	printSolution(solution);
	return solution;
	}

	public Set getExplanation() {
	ExplanationJob job = new ExplanationJob(dependencyHelper);
	job.schedule();
	IProgressMonitor pm = new NullProgressMonitor();
	pm.beginTask(Messages.Planner_NoSolution, 1000);
	try {
	synchronized (job) {
	while (job.getExplanationResult() == null && job.getState() != Job.NONE) {
	if (pm.isCanceled()) {
	job.cancel();
	throw new OperationCanceledException();
	}
	pm.worked(1);
	try {
	job.wait(100);
	} catch (InterruptedException e) {
	if (DEBUG)
	Tracing.debug("Interrupted while computing explanations"); //$NON-NLS-1$
	}
	}
	}
	} finally {
	pm.done();
	}
	return job.getExplanationResult();
	}

	public void stopSolver() {
	if (dependencyHelper != null)
	dependencyHelper.stopSolver();
	}

	public Collection getBestSolutionFoundSoFar() {
	if (solution == null) {
	backToIU();
	}
	if (solution == null)
	return null;
	return extractSolution();
	}
	}