@Override
	protected Constr constructClause(IVecInt v) {
		if (v == null)
			return null;
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalHTClause.brandNewClause(solver, getVocabulary(), v);
	}

	@Override
	protected Constr constructLearntClause(IVecInt resLits) {
		if (resLits.size() == 1) {
			return new UnitClause(resLits.last());
		}
		if (resLits.size() == 2) {
			return new LearntBinaryClause(resLits, getVocabulary());
		}
		return new LearntHTClause(resLits, getVocabulary());
	}

	@Override
	protected Constr constructCard(IVecInt theLits, int degree)
			throws ContradictionException {
		return MinWatchCard.minWatchCardNew(solver, getVocabulary(), theLits,
				MinWatchCard.ATLEAST, degree);
	}

	@Override
	protected Constr constructLearntCard(IDataStructurePB dspb) {
		IVecInt resLits = new VecInt();
		IVec<BigInteger> resCoefs = new Vec<BigInteger>();
		dspb.buildConstraintFromConflict(resLits, resCoefs);
		return new MinWatchCard(getVocabulary(), resLits, true, dspb
				.getDegree().intValue());
	}

}

		out.append(" ;\n");
		return FAKE_CONSTR;
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see org.sat4j.pb.IPBSolver#getExplanation()
	 */
	public String getExplanation() {
		// TODO Auto-generated method stub
		return null;
	}

	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * org.sat4j.pb.IPBSolver#setListOfVariablesForExplanation(org.sat4j.specs
	 * .IVecInt)
	 */
	public void setListOfVariablesForExplanation(IVecInt listOfVariables) {
		// TODO Auto-generated method stub

	}

	@Override
	public String toString() {
		StringBuffer out = getOut();
		if (!inserted) {
			StringBuffer tmp = new StringBuffer();
			tmp.append("* #variable= " + nVars());
			tmp.append(" #constraint= " + nbOfConstraints + " \n");
			if (obj != null) {
				tmp.append("min: ");
				tmp.append(obj);
				tmp.append(" ;\n");
			}
			out.insert(indxConstrObj, tmp.toString());
			inserted = true;
		}
		return out.toString();
	}

	@Override
	public String toString(String prefix) {
		return "OPB output solver";
	}

	@Override
	public int newVar(int howmany) {
		StringBuffer out = getOut();
		setNbVars(howmany);
		// to add later the number of constraints
		indxConstrObj = out.length();
		out.append("\n");
		return howmany;
	}

	@Override
	public void setExpectedNumberOfClauses(int nb) {
	}

	public ObjectiveFunction getObjectiveFunction() {
		return obj;
	}

}

	public OriginalHTClausePB(IVecInt ps, ILits voc) {
		super(ps, voc);
	}

	/**
     * 
     */
	private static final long serialVersionUID = 1L;

	public IVecInt computeAnImpliedClause() {
		return null;
	}

	public BigInteger getCoef(int literal) {
		return BigInteger.ONE;
	}

	public BigInteger[] getCoefs() {
		BigInteger[] tmp = new BigInteger[size()];
		for (int i = 0; i < tmp.length; i++)
			tmp[i] = BigInteger.ONE;
		return tmp;
	}

	public BigInteger getDegree() {
		return BigInteger.ONE;
	}

	/**
	 * Creates a brand new clause, presumably from external data. Performs all
	 * sanity checks.
	 * 
	 * @param s
	 *            the object responsible for unit propagation
	 * @param voc
	 *            the vocabulary
	 * @param literals
	 *            the literals to store in the clause
	 * @return the created clause or null if the clause should be ignored
	 *         (tautology for example)
	 */
	public static OriginalHTClausePB brandNewClause(UnitPropagationListener s,

	public OriginalBinaryClausePB(IVecInt ps, ILits voc) {
		super(ps, voc);
		// TODO Auto-generated constructor stub
	}

	/**
     * 
     */
	private static final long serialVersionUID = 1L;

	public IVecInt computeAnImpliedClause() {
		return null;
	}

	public BigInteger getCoef(int literal) {
		return BigInteger.ONE;
	}

	public BigInteger[] getCoefs() {
		BigInteger[] tmp = new BigInteger[size()];
		for (int i = 0; i < tmp.length; i++)
			tmp[i] = BigInteger.ONE;
		return tmp;
	}

	public BigInteger getDegree() {
		return BigInteger.ONE;
	}

		PuebloPBMinClauseCardConstrDataStructure {

	/**
     * 
     */
	private static final long serialVersionUID = 1L;

	@Override
	protected PBConstr constructCard(IVecInt theLits, int degree)
			throws ContradictionException {
		return AtLeastPB.atLeastNew(solver, getVocabulary(), theLits, degree);
	}

	@Override
	protected Constr constructLearntCard(IDataStructurePB dspb) {
		IVecInt resLits = new VecInt();
		IVec<BigInteger> resCoefs = new Vec<BigInteger>();
		dspb.buildConstraintFromConflict(resLits, resCoefs);
		return AtLeastPB.atLeastNew(getVocabulary(), resLits, dspb.getDegree()
				.intValue());
	}

}