JRummikub/src/jrummikub/ai/fdsolver/constraint/ListSumConstraint.java

package jrummikub.ai.fdsolver.constraint;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.Comparator;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

import jrummikub.ai.fdsolver.Constraint;
import jrummikub.ai.fdsolver.Propagator;
import jrummikub.ai.fdsolver.Satisfiability;
import jrummikub.ai.fdsolver.Var;

public class ListSumConstraint extends Constraint {
	Var<Integer> sum;
	List<Var<Integer>> list;
	List<Var<?>> vars = new ArrayList<Var<?>>();

	public ListSumConstraint(Var<Integer> sum, List<Var<Integer>> list) {
		this.sum = sum;
		this.list = list;
		vars.add(sum);
		vars.addAll(list);
	}

	@Override
	public Collection<Var<?>> getWatchedVars() {
		return vars;
	}

	@Override
	public Collection<Propagator> getPropagators(boolean negate) {
		return Collections.emptyList();
	}
	
	@Override
	public Satisfiability getSatisfiability() {
		List<Integer> values = new ArrayList<Integer>();
		int valueSum = 0;
		boolean isTaut = sum.getRange().size()==1;
		for (Var<Integer> var : list) {
			Iterator<Integer> it = var.getRange().iterator();
			int value = it.next();
			if (it.hasNext())
				isTaut = false;
			values.add(value);
			valueSum += value;
		}
		if (isTaut) {
			if (valueSum == sum.getValue()) {
				return Satisfiability.TAUT;
			} else {
				return Satisfiability.UNSAT;
			}
		}
		
		Set<Integer> reachableValues = new HashSet<Integer>();
		Set<Integer> newValues = new HashSet<Integer>();
		reachableValues.add(valueSum);
		
		if (sum.getRange().contains(valueSum)) {
			return Satisfiability.SAT;
		}
		
		for (int i = 0; i < values.size(); i++) {
			Var<Integer> var = list.get(i);
			int offset = values.get(i);
			for (int x : var.getRange()) {
				if (x == offset)
					continue;
				newValues.clear();
				for (int y : reachableValues) {
					int newValue = x + y - offset;
					if (!reachableValues.contains(newValue)) {
						newValues.add(x + y - offset);
					}
				}
				if (!Collections.disjoint(sum.getRange(), newValues)) {
					return Satisfiability.SAT;
				}
				reachableValues.addAll(newValues);
			}
		}

		return Satisfiability.UNSAT;
	}

}