content: /**
   * Copyright (c) 2018-2019 Siemens AG
   * All rights reserved.
   * 
   * Redistribution and use in source and binary forms, with or without
   * modification, are permitted provided that the following conditions are met:
   * 
   * 1) Redistributions of source code must retain the above copyright notice, this
   *    list of conditions and the following disclaimer.
   * 
   * 2) Redistributions in binary form must reproduce the above copyright notice,
   *    this list of conditions and the following disclaimer in the documentation
   *    and/or other materials provided with the distribution.
   * 
   * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
   * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
   * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
   * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
   * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
   * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
   * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
   * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
   * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
   */
  package at.ac.tuwien.kr.alpha.core.solver.heuristics;
  
  import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isPositive;
  
  import java.util.ArrayList;
  import java.util.Arrays;
  import java.util.Collection;
  
  import org.apache.commons.collections4.MultiValuedMap;
  import org.apache.commons.collections4.multimap.HashSetValuedHashMap;
  import org.slf4j.Logger;
  import org.slf4j.LoggerFactory;
  
  import at.ac.tuwien.kr.alpha.api.config.BinaryNoGoodPropagationEstimationStrategy;
  import at.ac.tuwien.kr.alpha.core.common.Assignment;
  import at.ac.tuwien.kr.alpha.core.common.NoGood;
  import at.ac.tuwien.kr.alpha.core.solver.ChoiceManager;
  import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth;
  import at.ac.tuwien.kr.alpha.core.solver.heuristics.activity.BodyActivityProvider;
  import at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult;
  
  /**
   * This implementation is inspired by the VSIDS implementation in <a href="https://github.com/potassco/clasp">clasp</a>.
   * Therefore, for example, decay is not realized by decreasing activity scores with age, but by
   * steadily increasing the increment added to the score of active atoms
   * (such that the activity score of older atoms does not have to be changed later).
   * <p/>
   * The implementation is simplified in some ways, e.g. it is not possible to specify a frequency in which the activity
   * increment is updated (which corresponds to decay), but it is updated after every conflict.
   * <p/>
   * Reference for VSIDS:
   * Moskewicz, Matthew W.; Madigan, Conor F.; Zhao, Ying; Zhang, Lintao; Malik, Sharad (2001):
   * Chaff: engineering an efficient SAT solver.
   * In: Proceedings of the 38th Design Automation Conference. IEEE, pp. 530–535.
   */
  public class VSIDS implements ActivityBasedBranchingHeuristic {
  	protected static final Logger LOGGER = LoggerFactory.getLogger(VSIDS.class);
  
  	public static final int DEFAULT_DECAY_PERIOD = 1;
  
  	/**
  	 * The default factor by which VSID's activity increment will be multiplied when the decay period has expired.
  	 * The value is taken from clasp's tweety configuration which clasp uses by default.
  	 */
  	public static final double DEFAULT_DECAY_FACTOR = 1 / 0.92;
  
  	protected final Assignment assignment;
  	protected final ChoiceManager choiceManager;
  
  	protected final HeapOfActiveAtoms heapOfActiveAtoms;
  	protected int[] signBalances = new int[0];
  
  	private final Collection<NoGood> bufferedNoGoods = new ArrayList<>();
  
  	private int nChoicesTrue;
  	private int nChoicesFalse;
  	private int nChoicesRand;
  
  	/**
  	 * Maps rule heads to atoms representing corresponding bodies.
  	 */
  	protected final MultiValuedMap<Integer, Integer> headToBodies = new HashSetValuedHashMap<>();
  
  	protected VSIDS(Assignment assignment, ChoiceManager choiceManager, HeapOfActiveAtoms heapOfActiveAtoms, BinaryNoGoodPropagationEstimationStrategy momsStrategy) {
  		this.assignment = assignment;
  		this.choiceManager = choiceManager;
  		this.heapOfActiveAtoms = heapOfActiveAtoms;
  		this.heapOfActiveAtoms.setMOMsStrategy(momsStrategy);
  	}
  
  	public VSIDS(Assignment assignment, ChoiceManager choiceManager, int decayPeriod, double decayFactor, BinaryNoGoodPropagationEstimationStrategy momsStrategy) {
  		this(assignment, choiceManager, new HeapOfActiveAtoms(decayPeriod, decayFactor, choiceManager),  momsStrategy);
  	}
  
  	public VSIDS(Assignment assignment, ChoiceManager choiceManager, BinaryNoGoodPropagationEstimationStrategy momsStrategy) {
  		this(assignment, choiceManager, DEFAULT_DECAY_PERIOD, DEFAULT_DECAY_FACTOR,  momsStrategy);
  	}
  
  	@Override
  	public void violatedNoGood(NoGood violatedNoGood) {
  	}
  
  	@Override
  	public void analyzedConflict(ConflictAnalysisResult analysisResult) {
  		ingestBufferedNoGoods();	//analysisResult may contain new atoms whose activity must be initialized
  		for (int resolutionAtom : analysisResult.resolutionAtoms) {
  			heapOfActiveAtoms.incrementActivity(resolutionAtom);
  		}
  		if (analysisResult.learnedNoGood != null) {
  			for (int literal : analysisResult.learnedNoGood) {
  				incrementSignCounter(literal);
  				heapOfActiveAtoms.incrementActivity(atomOf(literal));
  			}
  		}
  		heapOfActiveAtoms.decayIfTimeHasCome();
  	}
  
  	@Override
  	public void newNoGood(NoGood newNoGood) {
  		this.bufferedNoGoods.add(newNoGood);
  	}
  
  	@Override
  	public void newNoGoods(Collection<NoGood> newNoGoods) {
  		this.bufferedNoGoods.addAll(newNoGoods);
  	}
  
  	private void ingestBufferedNoGoods() {
  		heapOfActiveAtoms.newNoGoods(bufferedNoGoods);
  		bufferedNoGoods.clear();
  	}
  
  	/**
  	 * {@link VSIDS} manages a stack of nogoods in the fashion of {@link BerkMin}
  	 * and starts by looking at the most active atom <code>a</code> in the nogood currently at the top of the stack.
  	 * If <code>a</code> is an active choice point (i.e. representing the body of an applicable rule), it is immediately chosen;
  	 * else the most active choice point dependent on <code>a</code> is.
  	 * If there is no such atom, we continue further down the stack.
  	 * When choosing between dependent atoms, a {@link BodyActivityProvider} is employed to define the activity of a choice point.
  	 */
  	@Override
  	public int chooseLiteral() {
  		int atom = chooseAtom();
  		if (atom == DEFAULT_CHOICE_ATOM) {
  			return DEFAULT_CHOICE_LITERAL;
  		}
  		boolean sign = chooseSign(atom);
  		return atomToLiteral(atom, sign);
  	}
  
  	protected int chooseAtom() {
  		ingestBufferedNoGoods();
  		Integer mostActiveAtom;
  		while ((mostActiveAtom = heapOfActiveAtoms.getMostActiveAtom()) != null) {
  			if (choiceManager.isActiveChoiceAtom(mostActiveAtom)) {
  				return mostActiveAtom;
  			}
  		}
  		return DEFAULT_CHOICE_ATOM;
  	}
  
  	/**
  	 * Chooses a sign (truth value) to assign to the given atom.
  	 * 
  	 * To make this decision, sign counters are maintained that reflect how often an atom
  	 * occurs positively or negatively in learnt nogoods.
  	 * If the sign balance for the given atom is positive, {@code true} will be chosen.
  	 * If it is negative, {@code false} will be chosen.
  	 * If the sign balance is zero, the default sign is selected, which is {@code true}
  	 * iff the atom represents a rule body (which is currently always the case for atoms chosen in Alpha).
  	 * 
  	 * @param atom
  	 *          the chosen atom
  	 * @return the truth value to assign to the given atom
  	 */
  	protected boolean chooseSign(int atom) {
  		atom = getAtomForChooseSign(atom);
  
  		if (assignment.getTruth(atom) == ThriceTruth.MBT) {
  			return true;
  		}
  
  		int signBalance = getSignBalance(atom);
  		if (LOGGER.isDebugEnabled() && (nChoicesFalse + nChoicesTrue + nChoicesRand) % 100 == 0) {
  			LOGGER.debug("chooseSign stats: f={}, t={}, r={}", nChoicesFalse, nChoicesTrue, nChoicesRand);
  			LOGGER.debug("chooseSign stats: signBalance={}", signBalance);
  		}
  
  		if (signBalance >= 0) {
  			nChoicesTrue++;
  			return true;
  		} else {
  			nChoicesFalse++;
  			return false;
  		}
  	}
  
  	/**
  	 * This method just returns {@code atom} by default but can be overridden in subclasses.
  	 * @param atom the atom chosen by VSIDS
  	 * @return the atom to base the choice of sign upon
  	 */
  	protected int getAtomForChooseSign(int atom) {
  		return atom;
  	}
  
  	protected void incrementSignCounter(int literal) {
  		int atom = atomOf(literal);
  		boolean sign = isPositive(literal);
  		growForMaxAtomId(atom);
  		signBalances[atom] += sign ? 1 : -1;
  	}
  
  	@Override
  	public void growForMaxAtomId(int maxAtomId) {
  		// Grow arrays only if needed.
  		if (signBalances.length > maxAtomId) {
  			return;
  		}
  		// Grow to default size, except if bigger array is required due to maxAtomId.
  		int newCapacity = arrayGrowthSize(signBalances.length);
  		if (newCapacity < maxAtomId + 1) {
  			newCapacity = maxAtomId + 1;
  		}
  		signBalances = Arrays.copyOf(signBalances, newCapacity);
  		heapOfActiveAtoms.growToCapacity(newCapacity);
  	}
  
  	@Override
  	public double getActivity(int literal) {
  		return heapOfActiveAtoms.getActivity(literal);
  	}
  
  	/**
  	 * Returns the sign balance for the given atom in learnt nogoods.
  	 * @param atom
  	 * @return the number of times the given atom occurrs positively more often than negatively (which may be negative)
  	 */
  	int getSignBalance(int atom) {
  		return signBalances.length > atom ? signBalances[atom] : 0;
  	}
  
  	@Override
  	public String toString() {
  		return this.getClass().getSimpleName();
  	}
  
  }
  