/*
 * Copyright (c) 2016-2020, the Alpha Team.
 * All rights reserved.
 *
 * Additional changes made by Siemens.
 *
 * 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;

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.common.NoGoodInterface;
import at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;

import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize;
import static at.ac.tuwien.kr.alpha.commons.util.Util.oops;
import static at.ac.tuwien.kr.alpha.core.common.NoGood.HEAD;
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.isNegated;
import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isPositive;
import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.literalToString;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.FALSE;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT;
import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.TRUE;

/**
 * NoGoodStore using for each NoGood three watches, two ordinary ones and an alpha watch.
 * The alpha watch may point to positive or negative literals but not the head of the NoGood.
 *
 * Note the following invariant for watches:
 * (Inv): For every NoGood it either holds that both watched literals are unassigned, or for one watch holds: it
 *        points to a literal that is assigned a satisfying truth value at decision level d and the other
 *        watched literal is assigned at decision level d' such that d <= d'.
 *  The second condition ensures that after backtracking the NoGood is still satisfied or both watches
 *  point to unassigned literals. Observe that for an assignment to TRUE the (potentially lower) decision level of MBT
 *  is taken.
 *
 *  Copyright (c) 2017-2020, the Alpha Team.
 */
public class NoGoodStoreAlphaRoaming implements NoGoodStore, BinaryNoGoodPropagationEstimation, Checkable {
	private static final Logger LOGGER = LoggerFactory.getLogger(NoGoodStoreAlphaRoaming.class);
	private static final int UNASSIGNED = Integer.MAX_VALUE;

	private final WritableAssignment assignment;
	private final LearnedNoGoodDeletion learnedNoGoodDeletion;
	@SuppressWarnings(value = {"rawtypes", "unchecked"})
	private ArrayList<WatchedNoGood>[] watches = new ArrayList[0];
	@SuppressWarnings(value = {"rawtypes", "unchecked"})
	private ArrayList<WatchedNoGood>[] watchesAlpha = new ArrayList[0];
	private BinaryWatchList[] binaryWatches = new BinaryWatchList[0];
	private int maxAtomId;

	private boolean checksEnabled;
	private boolean didPropagate;
	private boolean hasBinaryNoGoods;

	private final NoGoodCounter counter = new NoGoodCounter();

	public NoGoodStoreAlphaRoaming(WritableAssignment assignment, boolean checksEnabled) {
		this.assignment = assignment;
		this.checksEnabled = checksEnabled;
		this.learnedNoGoodDeletion = new LearnedNoGoodDeletion(this, assignment);
	}

	public NoGoodStoreAlphaRoaming(WritableAssignment assignment) {
		this(assignment, false);
	}

	@SuppressWarnings(value = {"rawtypes", "unchecked"})
	void clear() {
		assignment.clear();
		learnedNoGoodDeletion.reset();
		binaryWatches = new BinaryWatchList[0];
		watches = new ArrayList[0];
		watchesAlpha = new ArrayList[0];
		maxAtomId = 0;
	}

	public LearnedNoGoodDeletion getLearnedNoGoodDeletion() {
		return learnedNoGoodDeletion;
	}

	@Override
	public void backtrack() {
		didPropagate = false;
		assignment.backtrack();
		if (checksEnabled) {
			if (assignment.getAssignmentsToProcess().isEmpty()) {
				new WatchedNoGoodsChecker().doWatchesCheck();
			} else {
				LOGGER.trace("Skipping watches check since there are assignments to process first.");
			}
		}
	}

	@Override
	public void growForMaxAtomId(int maxAtomId) {
		int requiredMaxSize = 2 * (maxAtomId + 2);
		if (requiredMaxSize < binaryWatches.length) {
			return;
		}
		int newCapacity = arrayGrowthSize(binaryWatches.length);
		if (newCapacity < requiredMaxSize) {
			newCapacity = requiredMaxSize;
		}
		int oldlength = binaryWatches.length;
		binaryWatches = Arrays.copyOf(binaryWatches, newCapacity);
		for (int i = oldlength; i < binaryWatches.length; i++) {
			binaryWatches[i] = new BinaryWatchList(i);
		}
		watches = Arrays.copyOf(watches, newCapacity);
		for (int i = oldlength; i < watches.length; i++) {
			watches[i] = new ArrayList<>();
		}
		watchesAlpha = Arrays.copyOf(watchesAlpha, newCapacity);
		for (int i = oldlength; i < watchesAlpha.length; i++) {
			watchesAlpha[i] = new ArrayList<>();
		}
		this.maxAtomId = maxAtomId;
	}

	@Override
	public NoGoodCounter getNoGoodCounter() {
		return counter;
	}

	@Override
	public void cleanupLearnedNoGoods() {
		if (learnedNoGoodDeletion.needToRunNoGoodDeletion()) {
			learnedNoGoodDeletion.runNoGoodDeletion();
		}
	}

	void removeFromWatches(WatchedNoGood toRemove) {
		counter.remove(toRemove);
		int watchedLiteral1 = toRemove.getLiteral(0);
		int watchedLiteral2 = toRemove.getLiteral(1);
		if (!watches(watchedLiteral2).remove(toRemove)
			|| !watches(watchedLiteral1).remove(toRemove)) {
			throw oops("Could not remove learned NoGood from watch lists.");
		}
		if (toRemove.hasHead()) {
			throw oops("NoGood has a head.");	// If this occurs, we need to remove the alpha watch too.
		}
	}

	private ArrayList<WatchedNoGood> watches(int literal) {
		return watches[literal];
	}

	private ArrayList<WatchedNoGood> watchesAlpha(int literal) {
		return watchesAlpha[literal];
	}

	private void addOrdinaryWatch(WatchedNoGood wng, int pointer) {
		final int literal = wng.getLiteral(pointer);
		watches(literal).add(wng);
	}

	private void addAlphaWatch(WatchedNoGood wng) {
		final int literal = wng.getLiteralAtAlpha();
		watchesAlpha(literal).add(wng);
	}

	@Override
	public ConflictCause add(int id, NoGood noGood, int lbd) {
		LOGGER.trace("Adding {}", noGood);

		final ConflictCause conflictCause;
		if (noGood.isUnary()) {
			conflictCause = addUnary(noGood);
		} else if (noGood.isBinary()) {
			conflictCause = addAndWatchBinary(noGood);
		} else {
			conflictCause = addAndWatch(noGood, lbd);
		}

		if (conflictCause == null) {
			counter.add(noGood);
		}
		return conflictCause;
	}

	@Override
	public ConflictCause add(int id, NoGood noGood) {
		return add(id, noGood, -1);
	}

	/**
	 * Takes a noGood containing only a single literal and translates it into an assignment (because it
	 * is trivially unit). Still, a check for conflict is performed.
	 */
	private ConflictCause addUnary(final NoGood noGood) {
		if (noGood.hasHead()) {
			return assignStrongComplement(noGood, 0);
		} else {
			return assignWeakComplement(0, noGood, 0);
		}
	}

	private static boolean isComplementaryAssigned(int literal, ThriceTruth literalTruth) {
		return literalTruth != null && literalTruth.toBoolean() != isPositive(literal);
	}

	private int strongDecisionLevel(int atom) {
		int strongDecisionLevel = assignment.getStrongDecisionLevel(atom);
		return strongDecisionLevel == -1 ? UNASSIGNED : strongDecisionLevel;
	}

	private ConflictCause addAndWatch(final NoGood noGood, int lbd) {
		// Collect potential watch candidates.
		int posWeakUnassigned1 = -1;
		int posWeakUnassigned2 = -1;
		int posSatisfiedLiteral1 = -1;
		int posSatisfiedLiteral2 = -1;
		int posWeakHighestAssigned = -1;
		int weakDecisionLevelHighestAssigned = -1;
		int posStrongHighestAssigned = -1;
		int strongDecisionLevelHighestAssigned = -1;
		int posPotentialAlphaWatch = -1;
		int satisfiedLiteralWeakDecisionLevel = -1;

		// Used to detect always-satisfied NoGoods of form { L, -L, ... }.
		Map<Integer, Boolean> occurringAtomPolarity = new HashMap<>();

		// Iterate noGood and record satisfying/unassigned/etc positions.
		int headAtom = atomOf(noGood.getHead());
		final ThriceTruth headTruth = noGood.hasHead() ? assignment.getTruth(headAtom) : null;
		final boolean isHeadTrue = headTruth == TRUE;
		for (int i = 0; i < noGood.size(); i++) {
			final int literal = noGood.getLiteral(i);
			final int atom = atomOf(literal);
			final ThriceTruth atomTruthValue = assignment.getTruth(atom);
			final int atomWeakDecisionLevel = assignment.getWeakDecisionLevel(atom);
			final int atomStrongDecisionLevel = assignment.getStrongDecisionLevel(atom);

			// Check if NoGood can never be violated (atom occurring positive and negative)
			if (occurringAtomPolarity.containsKey(atomOf(literal))) {
				if (occurringAtomPolarity.get(atomOf(literal)) != isNegated(literal)) {
					// NoGood cannot be violated or propagate, ignore it.
					LOGGER.debug("Added NoGood can never propagate or be violated, ignoring it. NoGood is: {}", noGood);
					return null;
				}
			} else {
				occurringAtomPolarity.put(atomOf(literal), isNegated(literal));
			}

			// Check weak unassigned.
			if (atomTruthValue == null) {
				if (posWeakUnassigned1 == -1) {
					posWeakUnassigned1 = i;
				} else {
					posWeakUnassigned2 = i;
				}
			}
			// Alpha watch:
			if (posPotentialAlphaWatch == -1 && noGood.hasHead() && i != HEAD) {
				// Current literal is potential alpha watch if:
				// 1) the head of the nogood is true and the literal is assigned at a higher-or-equal decision level.
				// 2) the literal is complementary assigned and thus satisfies the nogood, or
				// 3) the literal is unassigned or assigned must-be-true.
				if (isHeadTrue && strongDecisionLevel(atomOf(literal)) >= strongDecisionLevel(headAtom)
					|| isComplementaryAssigned(noGood.getLiteral(i), atomTruthValue)
					|| strongDecisionLevel(atomOf(literal)) == Integer.MAX_VALUE) {
					posPotentialAlphaWatch = i;
				}
			}
			// Check satisfaction
			if (atomTruthValue != null && atomTruthValue.toBoolean() != isPositive(literal)) {
				if (posSatisfiedLiteral1 == -1) {
					posSatisfiedLiteral1 = i;
					satisfiedLiteralWeakDecisionLevel = atomWeakDecisionLevel;
				} else {
					posSatisfiedLiteral2 = i;
				}
			}
			// Check violation.
			if (atomTruthValue != null && atomTruthValue.toBoolean() == isPositive(literal)) {
				if (atomWeakDecisionLevel > weakDecisionLevelHighestAssigned) {
					weakDecisionLevelHighestAssigned = atomWeakDecisionLevel;
					posWeakHighestAssigned = i;
				}
				if (!atomTruthValue.isMBT() && noGood.hasHead()	// Ensure strong violation.
					&& atomStrongDecisionLevel > strongDecisionLevelHighestAssigned) {
					strongDecisionLevelHighestAssigned = atomStrongDecisionLevel;
					posStrongHighestAssigned = i;
				}
			}
		}

		// Set ordinary and alpha watches now.
		// Compute ordinary watches:
		final int watch1;
		final int watch2;


		if (posWeakUnassigned1 != -1 && posWeakUnassigned2 != -1) {
			// NoGood has two unassigned literals.
			watch1 = posWeakUnassigned1;
			watch2 = posWeakUnassigned2;
		} else if (posSatisfiedLiteral1 != -1) {
			// NoGood is satisfied.
			int bestSecondPointer = posSatisfiedLiteral2 != -1 ? posSatisfiedLiteral2
						: posWeakUnassigned1 != -1 ? posWeakUnassigned1
						: posWeakHighestAssigned;
			if (posSatisfiedLiteral2 == -1 && posWeakUnassigned1 == -1) {
				// The NoGood has only one satisfied literal and is unit without it.
				// If it is unit on lower decision level than it is satisfied, it propagates the satisfying literal on lower decision level.
				if (satisfiedLiteralWeakDecisionLevel > weakDecisionLevelHighestAssigned) {
					ConflictCause conflictCause = assignWeakComplement(posSatisfiedLiteral1, noGood, weakDecisionLevelHighestAssigned);
					if (conflictCause != null) {
						return conflictCause;
					}
				}
			}
			watch1 = posSatisfiedLiteral1;
			watch2 = bestSecondPointer;
		} else if (posWeakUnassigned1 != -1) {
			// NoGood is weakly unit; propagate.
			ConflictCause conflictCause = assignWeakComplement(posWeakUnassigned1, noGood, weakDecisionLevelHighestAssigned);
			if (conflictCause != null) {
				return conflictCause;
			}
			watch1 = posWeakUnassigned1;
			watch2 = posWeakHighestAssigned;
		} else {
			// NoGood is violated.
			return new ConflictCause(noGood.asAntecedent());
		}

		// Compute alpha watch:
		int watchAlpha = -1;
		if (noGood.hasHead()) {
			if (posPotentialAlphaWatch != -1) {
				// Found potential alpha watch.
				watchAlpha = posPotentialAlphaWatch;
			} else {
				// No potential alpha watch found: noGood must be strongly unit.
				ConflictCause conflictCause = assignStrongComplement(noGood, strongDecisionLevelHighestAssigned);
				if (conflictCause != null) {
					return conflictCause;
				}
				watchAlpha = posStrongHighestAssigned;
			}
		}
		WatchedNoGood wng = new WatchedNoGood(noGood, watch1, watch2, watchAlpha);
		LOGGER.trace("WatchedNoGood is {}.", wng);

		// Record for eventual removal if this NoGood is learned.
		if (noGood.getType() == Type.LEARNT) {
			wng.setLBD(lbd);
			learnedNoGoodDeletion.recordLearnedNoGood(wng);
		}

		if (wng.getAlphaPointer() == -1 && noGood.hasHead()) {
			throw oops("Did not set alpha watch for nogood with head.");
		}

		// Register alpha watch if present.
		if (wng.getAlphaPointer() != -1) {
			addAlphaWatch(wng);
		}
		// Set ordinary watches.
		addOrdinaryWatch(wng, 0);
		addOrdinaryWatch(wng, 1);
		return null;
	}

	private ConflictCause addAndWatchBinary(final NoGood noGood) {
		// Shorthands for viewing the nogood as { a, b }.
		final int a = noGood.getLiteral(0);
		final int b = noGood.getLiteral(1);
		final int atomA = atomOf(a);
		final int atomB = atomOf(b);

		// Ignore NoGoods of the form { -a, a }.
		if (a != b && atomA == atomB) {
			return null;
		}

		// Note: it might be faster to not check explicitly for violation but wait for conflict from assign.
		final ThriceTruth atomATruthValue = assignment.getTruth(atomA);
		final ThriceTruth atomBTruthValue = assignment.getTruth(atomB);

		final boolean isViolatedA = atomATruthValue != null && isPositive(a) == atomATruthValue.toBoolean();
		final boolean isViolatedB = atomBTruthValue != null && isPositive(b) == atomBTruthValue.toBoolean();

		// Check for violation.
		if (isViolatedA && isViolatedB) {
			return new ConflictCause(noGood.asAntecedent());
		}

		// The above violation check guarantees that adding (and propagation on other literal) results in no conflict.
		binaryWatches[a].add(noGood);
		binaryWatches[b].add(noGood);
		hasBinaryNoGoods = true;
		return null;
	}

	private ConflictCause assignWeakComplement(final int literalIndex, final NoGoodInterface impliedBy, int decisionLevel) {
		final int literal = impliedBy.getLiteral(literalIndex);
		ThriceTruth truth = isNegated(literal) ? MBT : FALSE;
		return assignTruth(atomOf(literal), truth, impliedBy.asAntecedent(), decisionLevel);
	}

	private ConflictCause assignStrongComplement(final NoGoodInterface impliedBy, int decisionLevel) {
		return assignTruth(atomOf(impliedBy.getHead()), TRUE, impliedBy.asAntecedent(), decisionLevel);
	}

	private ConflictCause assignTruth(int atom, ThriceTruth truth, Antecedent impliedBy, int decisionLevel) {
		ConflictCause cause = assignment.assign(atom, truth, impliedBy, decisionLevel);
		if (cause == null) {
			didPropagate = true;
		}
		return cause;
	}

	/**
	 * Propagates from Unassigned to MBT/FALSE.
	 * @param literal the literal that triggers the propagation.
	 */
	private ConflictCause propagateWeakly(int literal, int currentDecisionLevel, boolean restrictToBinaryNoGoods) {
		final ArrayList<WatchedNoGood> watchesOfAssignedAtom = watches(literal);

		// Propagate binary watches.
		ConflictCause conflictCause = binaryWatches[literal].propagateWeakly();
		if (conflictCause != null || restrictToBinaryNoGoods) {
			return conflictCause;
		}

		// Check all watched multi-ary NoGoods.
		Iterator<WatchedNoGood> watchIterator = watchesOfAssignedAtom.iterator();
		clearOrdinaryWatchList(literal);
		while (watchIterator.hasNext()) {
			WatchedNoGood nextNoGood = watchIterator.next();
			conflictCause = processWeaklyWatchedNoGood(literal, nextNoGood, currentDecisionLevel);
			if (conflictCause != null) {
				// Copy over all non-treated NoGoods, so that they can be treated after backtracking.
				ArrayList<WatchedNoGood> watchlist = watches(literal);
				watchlist.add(nextNoGood);
				while (watchIterator.hasNext()) {
					watchlist.add(watchIterator.next());
				}
				return conflictCause;
			}
		}
		return null;
	}

	private ConflictCause processWeaklyWatchedNoGood(int assignedLiteral, WatchedNoGood watchedNoGood, int currentDecisionLevel) {
		final int assignedWatch = watchedNoGood.getLiteral(0) == assignedLiteral ? 0 : 1;
		final int otherWatch = 1 - assignedWatch;

		final int otherLiteral = watchedNoGood.getLiteral(otherWatch);
		final ThriceTruth otherAtomTruth = assignment.getTruth(atomOf(otherLiteral));

		// Find new literal to watch.

		// Check if the other watch already satisfies the noGood.
		if (otherAtomTruth != null && otherAtomTruth.toBoolean() != isPositive(otherLiteral)) {
			// Keep this watch and return early.
			addOrdinaryWatch(watchedNoGood, assignedWatch);
			return null;
		} else {
			for (int i = 2; i < watchedNoGood.size(); i++) {
				final int currentLiteral = watchedNoGood.getLiteral(i);
				final ThriceTruth currentTruth = assignment.getTruth(atomOf(currentLiteral));

				// Break if: 1) current literal is unassigned, or 2) satisfies the nogood.
				if (currentTruth == null || currentTruth.toBoolean() != isPositive(currentLiteral)) {
					// Move pointer to new literal.
					watchedNoGood.setWatch(assignedWatch, i);
					addOrdinaryWatch(watchedNoGood, assignedWatch);
					if (LOGGER.isTraceEnabled()) {
						LOGGER.trace("Moved watch pointers of nogood:");
						logNoGoodAndAssignment(watchedNoGood, assignment);
					}
					return null;
				}
			}
		}

		// NoGood is unit, propagate the other watched literal.
		// Note: Violation is detected by Assignment.
		if (LOGGER.isTraceEnabled()) {
			LOGGER.trace("Nogood is unit:");
			logNoGoodAndAssignment(watchedNoGood, assignment);
		}
		ConflictCause conflictCause = assignWeakComplement(otherWatch, watchedNoGood, currentDecisionLevel);
		// Return conflict if noGood is violated.
		if (conflictCause != null) {
			return conflictCause;
		}
		// Watch same literal again.
		addOrdinaryWatch(watchedNoGood, assignedWatch);
		return null;
	}

	private void logNoGoodAndAssignment(WatchedNoGood noGood, Assignment assignment) {
		if (!LOGGER.isTraceEnabled()) {
			return;
		}
		StringBuilder sb = new StringBuilder("Watched NoGood is: " + noGood + "\t\t Assigned: ");
		for (Integer literal : noGood) {
			Assignment.Entry assignmentEntry = assignment.get(atomOf(literal));
			sb.append(atomOf(literal));
			sb.append("=");
			sb.append(assignmentEntry);
			sb.append(", ");
		}
		LOGGER.trace(sb.toString());
	}

	private ConflictCause propagateStrongly(int literal, int currentDecisionLevel, boolean restrictToBinaryNoGoods) {

		// Propagate binary watches.
		ConflictCause conflictCause = binaryWatches[literal].propagateStrongly();
		if (conflictCause != null || restrictToBinaryNoGoods) {
			return conflictCause;
		}

		// Check all watched multi-ary NoGoods.
		Iterator<WatchedNoGood> watchIterator = watchesAlpha(literal).iterator();
		clearAlphaWatchList(literal);
		while (watchIterator.hasNext()) {
			WatchedNoGood nextNoGood = watchIterator.next();
			if (!nextNoGood.hasHead()) {
				throw oops("Strong propagation encountered NoGood without head");
			}
			conflictCause = processStronglyWatchedNoGood(nextNoGood, currentDecisionLevel);
			if (conflictCause != null) {
				// Copy over all non-treated NoGoods, so that they can be treated after backtracking.
				ArrayList<WatchedNoGood> watchlist = watchesAlpha(literal);
				watchlist.add(nextNoGood);
				while (watchIterator.hasNext()) {
					watchlist.add(watchIterator.next());
				}
				return conflictCause;
			}
		}
		return null;
	}

	private ConflictCause processStronglyWatchedNoGood(WatchedNoGood watchedNoGood, int currentDecisionLevel) {

		final int headAtom = atomOf(watchedNoGood.getHead());
		final ThriceTruth headAtomTruth = assignment.getTruth(headAtom);
		// Check if the other watch, i.e., the head, already satisfies the noGood.
		if (headAtomTruth != null && TRUE == headAtomTruth) {
			// Keep this watch and return early.
			addAlphaWatch(watchedNoGood);
			return null;
		}

		final int assignedIndex = watchedNoGood.getAlphaPointer();

		// Find new literal to watch.
		for (int i = 0; i < watchedNoGood.size(); i++) {
			if (i == assignedIndex || i == watchedNoGood.getHeadIndex()) {
				continue;
			}
			int currentLiteral = watchedNoGood.getLiteral(i);
			int currentAtom = atomOf(currentLiteral);
			ThriceTruth currentAtomTruth = assignment.getTruth(currentAtom);

			// Break if: 1) current literal is unassigned (or MBT), or 2) satisfies the nogood.
			if (currentAtomTruth == null || currentAtomTruth.isMBT() || currentAtomTruth.toBoolean() != isPositive(currentLiteral)) {
				// Move pointer to new literal.
				watchedNoGood.setAlphaPointer(i);
				addAlphaWatch(watchedNoGood);
				return null;
			}
		}

		// NoGood is unit, propagate.
		ConflictCause conflictCause = assignStrongComplement(watchedNoGood, currentDecisionLevel);
		if (conflictCause != null) {
			return conflictCause;
		}
		// Watch same literal again.
		addAlphaWatch(watchedNoGood);
		return null;
	}

	@Override
	public ConflictCause propagate() {
		ConflictCause conflictCause = propagate(false);
		if (conflictCause != null) {
			learnedNoGoodDeletion.increaseConflictCounter();
		}
		return conflictCause;
	}

	private ConflictCause propagateOnlyBinaryNoGoods() {
		return propagate(true);
	}
	
	private ConflictCause propagate(boolean restrictToBinaryNoGoods) {
		didPropagate = false;

		Assignment.Pollable assignmentsToProcess = assignment.getAssignmentsToProcess();
		int currentDecisionLevel = assignment.getDecisionLevel();
		while (!assignmentsToProcess.isEmpty()) {
			final int atom = assignmentsToProcess.peek();
			final ThriceTruth currentTruth = assignment.getTruth(atom);
			final int literal = atomToLiteral(atom, currentTruth.toBoolean());
			if (LOGGER.isTraceEnabled()) {
				LOGGER.trace("Propagation processing atom: {}={}", atom, currentTruth);
			}

			// Propagate weakly, except if there is an earlier MBT, where propagation already took place.
			if (currentTruth != TRUE || assignment.getWeakDecisionLevel(atom) == currentDecisionLevel) {
				ConflictCause conflictCause = propagateWeakly(literal, currentDecisionLevel, restrictToBinaryNoGoods);
				if (conflictCause != null) {
					LOGGER.trace("Halting propagation due to conflict. Current assignment: {}.", assignment);
					return conflictCause;
				}
			}

			// Propagate strongly only for TRUE/FALSE assignments.
			if (currentTruth != MBT) {
				ConflictCause conflictCause = propagateStrongly(literal, currentDecisionLevel, restrictToBinaryNoGoods);
				if (conflictCause != null) {
					LOGGER.trace("Halting propagation due to conflict. Current assignment: {}.", assignment);
					return conflictCause;
				}
			}
			assignmentsToProcess.remove();
		}
		if (checksEnabled && !restrictToBinaryNoGoods) {
			runInternalChecks();
		}
		return null;
	}

	@Override
	public boolean didPropagate() {
		return didPropagate;
	}

	@Override
	public void setChecksEnabled(boolean checksEnabled) {
		this.checksEnabled = checksEnabled;
	}

	class BinaryWatchList implements ShallowAntecedent {
		private int[] noGoodsWithoutHead = new int[10];
		private int noGoodsWithoutHeadSize;
		private int[] noGoodsWithHead = new int[10];
		private int noGoodsWithHeadSize;
		private final int forLiteral;

		private BinaryWatchList(int forLiteral) {
			this.forLiteral = forLiteral;
		}

		ConflictCause add(NoGood noGood) {
			if (!noGood.isBinary()) {
				throw oops("Received noGood is not binary.");
			}
			if (noGood.hasHead() && noGood.getHead() != forLiteral) {
				return addHeadedNoGood(noGood);
			} else {
				return addOrdinaryNoGood(noGood);
			}
		}

		private ConflictCause addHeadedNoGood(NoGood noGood) {
			if (noGoodsWithHeadSize + 1 > noGoodsWithHead.length) {
				noGoodsWithHead = Arrays.copyOf(noGoodsWithHead, arrayGrowthSize(noGoodsWithHeadSize));
			}
			int otherLiteral = noGood.getLiteral(0) == forLiteral ? noGood.getLiteral(1) : noGood.getLiteral(0);
			if (isPositive(otherLiteral)) {
				throw oops("NoGood has wrong head.");
			}
			noGoodsWithHead[noGoodsWithHeadSize++] = otherLiteral;
			// Assign (weakly) otherLiteral if the newly added NoGood is unit.
			ThriceTruth literalTruth = assignment.getTruth(atomOf(forLiteral));
			if (literalTruth != null && literalTruth.toBoolean() == isPositive(forLiteral)) {
				int weakDecisionLevel = assignment.getWeakDecisionLevel(atomOf(forLiteral));
				ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this, weakDecisionLevel);
				if (conflictCause != null) {
					return conflictCause;
				}
			}
			// Assign head (strongly) if the newly added NoGood is unit.
			int strongDecisionLevel = assignment.getStrongDecisionLevel(atomOf(forLiteral));
			if (strongDecisionLevel != -1 && assignment.getTruth(atomOf(forLiteral)).toBoolean() == isPositive(forLiteral)) {
				return assignment.assign(atomOf(otherLiteral), TRUE, this, strongDecisionLevel);
			}
			return null;
		}

		private ConflictCause addOrdinaryNoGood(NoGood noGood) {
			if (noGoodsWithoutHeadSize + 1 > noGoodsWithoutHead.length) {
				noGoodsWithoutHead = Arrays.copyOf(noGoodsWithoutHead, arrayGrowthSize(noGoodsWithoutHeadSize));
			}
			int otherLiteral = noGood.getLiteral(0) == forLiteral ? noGood.getLiteral(1) : noGood.getLiteral(0);
			noGoodsWithoutHead[noGoodsWithoutHeadSize++] = otherLiteral;
			// Assign otherLiteral if the newly added NoGood is unit.
			ThriceTruth literalTruth = assignment.getTruth(atomOf(forLiteral));
			if (literalTruth != null && literalTruth.toBoolean() == isPositive(forLiteral)) {
				int weakDecisionLevel = assignment.getWeakDecisionLevel(atomOf(forLiteral));
				return assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this, weakDecisionLevel);
			}
			return null;
		}

		ConflictCause propagateWeakly() {
			didPropagate |= noGoodsWithHeadSize > 0 || noGoodsWithoutHeadSize > 0;
			for (int i = 0; i < noGoodsWithoutHeadSize; i++) {
				final int otherLiteral = noGoodsWithoutHead[i];
				ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this);
				if (conflictCause != null) {
					return conflictCause;
				}
			}
			for (int i = 0; i < noGoodsWithHeadSize; i++) {
				final int otherLiteral = noGoodsWithHead[i];
				ConflictCause conflictCause = assignment.assign(atomOf(otherLiteral), isPositive(otherLiteral) ? FALSE : MBT, this);
				if (conflictCause != null) {
					return conflictCause;
				}
			}
			return null;
		}

		ConflictCause propagateStrongly() {
			didPropagate |= noGoodsWithHeadSize > 0;
			for (int i = 0; i < noGoodsWithHeadSize; i++) {
				final int headLiteral = noGoodsWithHead[i];
				ConflictCause conflictCause = assignment.assign(atomOf(headLiteral), TRUE, this);
				if (conflictCause != null) {
					return conflictCause;
				}
			}
			return null;
		}
		
		public int size() {
			return noGoodsWithHeadSize + noGoodsWithoutHeadSize;
		}

		@Override
		public String toString() {
			return "BinaryWatchList(" + literalToString(forLiteral) + ")";
		}

		@Override
		public Antecedent instantiateAntecedent(int impliedLiteral) {
			return new BinaryAntecedent(impliedLiteral, forLiteral);
		}

		private class BinaryAntecedent implements Antecedent {
			private final int[] literals = new int[2];

			BinaryAntecedent(int lit1, int lit2) {
				literals[0] = lit1;
				literals[1] = lit2;
			}

			@Override
			public int[] getReasonLiterals() {
				return literals;
			}

			@Override
			public void bumpActivity() {
			}

			@Override
			public void decreaseActivity() {
			}

			@Override
			public String toString() {
				return "{" + literalToString(literals[0]) + ", " + literalToString(literals[1]) + "}";
			}
		}
	}

	private void clearOrdinaryWatchList(int literal) {
		watches[literal] = new ArrayList<>();
	}

	private void clearAlphaWatchList(int literal) {
		watchesAlpha[literal] = new ArrayList<>();
	}

	@Override
	public int estimate(int atom, boolean truth, BinaryNoGoodPropagationEstimationStrategy strategy) {
		if (BinaryNoGoodPropagationEstimationStrategy.BinaryNoGoodPropagation.equals(strategy)) {
			return estimateEffectsOfBinaryNoGoodPropagation(atom, truth) - 1;
		}
		return getNumberOfBinaryWatches(atom, truth);
	}

	private int getNumberOfBinaryWatches(int atom, boolean truth) {
		return binaryWatches[atomToLiteral(atom, truth)].size();
	}

	private int estimateEffectsOfBinaryNoGoodPropagation(int atom, boolean truth) {
		assignment.choose(atom, truth);
		propagateOnlyBinaryNoGoods();
		int assignedNewly = assignment.getNumberOfAtomsAssignedSinceLastDecision();
		assignment.backtrack();
		return assignedNewly;
	}

	private void runInternalChecks() {
		new WatchedNoGoodsChecker().doWatchesCheck();
	}

	/**
	 * This class provides helper methods to detect NoGoods that are not properly watched by this NoGoodStore.
	 * This should be used only during debugging since checking is costly.
	 */
	private class WatchedNoGoodsChecker {

		void doWatchesCheck() {
			LOGGER.debug("Checking watch invariant.");
			// Check all watched NoGoods, if their pointers adhere to the watch-pointer invariant.
			for (int literal = 0; literal < watches.length; literal++) {
				if (isNegated(literal)) {
					// We treat positive and negative ones at the iteration of the positive literal.
					continue;
				}
				final int atom = atomOf(literal);
				if (atom > maxAtomId) {
					break;
				}
				checkOrdinaryWatchesInvariant(atom, true);
				checkOrdinaryWatchesInvariant(atom, false);
				checkAlphaWatchesInvariant(atom, true);
				checkAlphaWatchesInvariant(atom, false);
			}
			LOGGER.debug("Checking watch invariant: all good.");
		}

		int weakDecisionLevel(Assignment.Entry entry) {
			return entry == null ? UNASSIGNED : entry.hasPreviousMBT() ? entry.getMBTDecisionLevel() : entry.getDecisionLevel();
		}

		int weakReplayLevel(int atom) {
			if (assignment instanceof TrailAssignment) {
				return ((TrailAssignment) assignment).getOutOfOrderDecisionLevel(atom);
			}
			return UNASSIGNED;
		}

		int trailAwareStrongDecisionLevel(int atom) {
			int trailStrongDecisionLevel = UNASSIGNED;
			if (assignment instanceof TrailAssignment) {
				trailStrongDecisionLevel = ((TrailAssignment) assignment).getOutOfOrderStrongDecisionLevel(atom);
			}
			int atomStrongDecisionLevel = strongDecisionLevel(atom);
			return Math.min(trailStrongDecisionLevel, atomStrongDecisionLevel);
		}

		private void checkAlphaWatchesInvariant(int atom, boolean truth) {
			Assignment.Entry atomEntry = assignment.get(atom);
			int atomLiteral = atomToLiteral(atom, truth);
			boolean atomSatisfies = atomEntry != null && isPositive(atomLiteral) != atomEntry.getTruth().toBoolean();
			int atomDecisionLevel = strongDecisionLevel(atom);
			BinaryWatchList binaryWatchList = binaryWatches[atomLiteral];
			for (int i = 0; i < binaryWatchList.noGoodsWithHeadSize; i++) {
				int headLiteral = binaryWatchList.noGoodsWithHead[i];
				if (headLiteral == atomLiteral) {
					throw oops("Watch invariant violated: alpha watch points at head.");
				}
				Assignment.Entry headEntry = assignment.get(atomOf(headLiteral));
				boolean headViolates = headEntry != null && isPositive(headLiteral) == headEntry.getTruth().toBoolean();
				int headDecisionLevel = trailAwareStrongDecisionLevel(atomOf(headLiteral));
				if (watchInvariant(atomSatisfies, atomDecisionLevel, headLiteral, headDecisionLevel, headEntry)
					|| headViolates) {	// Head "pointer" is never moved and violation is checked by weak propagation, hence a violated head is okay.
					continue;
				}
				throw oops("Watch invariant (alpha) violated");
			}
			for (WatchedNoGood watchedNoGood : watchesAlpha(atomLiteral)) {
				int headLiteral = watchedNoGood.getHead();
				if (headLiteral == atomLiteral) {
					throw oops("Watch invariant violated: alpha watch points at head.");
				}
				Assignment.Entry headEntry = assignment.get(atomOf(headLiteral));
				boolean headViolates = headEntry != null && isPositive(headLiteral) == headEntry.getTruth().toBoolean();
				int headDecisionLevel = trailAwareStrongDecisionLevel(atomOf(headLiteral));
				if (watchInvariant(atomSatisfies, atomDecisionLevel, headLiteral, headDecisionLevel, headEntry)
					|| headViolates) {	// Head "pointer" is never moved and violation is checked by weak propagation, hence a violated head is okay.
					continue;
				}
				throw oops("Watch invariant (alpha) violated");
			}
		}

		private void checkOrdinaryWatchesInvariant(int atom, boolean truth) {
			Assignment.Entry atomEntry = assignment.get(atom);
			int atomLiteral = atomToLiteral(atom, truth);
			boolean atomSatisfies = atomEntry != null && isPositive(atomLiteral) != atomEntry.getTruth().toBoolean();
			int atomDecisionLevel = weakDecisionLevel(atomEntry);
			int atomReplayLevel = weakReplayLevel(atom);
			BinaryWatchList binaryWatchList = binaryWatches[atomLiteral];
			for (int i = 0; i < binaryWatchList.noGoodsWithoutHeadSize; i++) {
				int otherLiteral = binaryWatchList.noGoodsWithoutHead[i];
				checkBinaryWatch(atomSatisfies, atomDecisionLevel, atomReplayLevel, otherLiteral);
			}
			for (int i = 0; i < binaryWatchList.noGoodsWithHeadSize; i++) {
				int otherLiteral = binaryWatchList.noGoodsWithHead[i];
				checkBinaryWatch(atomSatisfies, atomDecisionLevel, atomReplayLevel, otherLiteral);
			}
			for (WatchedNoGood watchedNoGood : watches(atomLiteral)) {
				// Ensure both watches are either unassigned, or one satisfies NoGood, or both are on highest decision level.
				int otherPointer = atom ==  atomOf(watchedNoGood.getLiteral(1)) ? 0 : 1;
				int otherLiteral = watchedNoGood.getLiteral(otherPointer);
				int otherAtom = atomOf(otherLiteral);
				int thisAtom = atomOf(watchedNoGood.getLiteral(1 - otherPointer));
				if (thisAtom != atom) {
					throw oops("Watched atom is not at first/second position in literals array.");
				}
				Assignment.Entry otherEntry = assignment.get(otherAtom);
				int otherDecisionLevel = weakDecisionLevel(otherEntry);
				int otherReplayLevel = weakReplayLevel(otherAtom);
				boolean otherSatisfies = otherEntry != null && isPositive(otherLiteral) != otherEntry.getTruth().toBoolean();
				if (watchInvariant(atomSatisfies, otherSatisfies, atomDecisionLevel, atomReplayLevel, otherDecisionLevel, otherReplayLevel)) {
					continue;
				}
				throw oops("Watch invariant violated");
			}
		}

		private void checkBinaryWatch(boolean atomSatisfies, int atomDecisionLevel, int atomReplayLevel, int otherLiteral) {
			int otherAtom = atomOf(otherLiteral);
			Assignment.Entry otherEntry = assignment.get(otherAtom);
			boolean otherSatisfies = otherEntry != null && isPositive(otherLiteral) != otherEntry.getTruth().toBoolean();
			int otherDecisionLevel = weakDecisionLevel(otherEntry);
			int otherReplayLevel = weakReplayLevel(otherAtom);
			if (watchInvariant(atomSatisfies, otherSatisfies, atomDecisionLevel, atomReplayLevel, otherDecisionLevel, otherReplayLevel)) {
				return;
			}
			throw oops("Watch invariant violated");
		}

		private boolean watchInvariant(boolean atomSatisfies, boolean otherAtomSatisfies, int atomDecisionLevel, int atomReplayLevel, int otherAtomDecisionLevel, int otherAtomReplayLevel) {
			if (atomDecisionLevel == UNASSIGNED && otherAtomDecisionLevel == UNASSIGNED) {
				// Both watches are unassigned.
				return true;
			}
			if ((atomSatisfies && (otherAtomDecisionLevel >= atomDecisionLevel || otherAtomDecisionLevel >= atomReplayLevel))
				|| (otherAtomSatisfies && (atomDecisionLevel >= otherAtomDecisionLevel || atomDecisionLevel >= otherAtomReplayLevel))) {
				// One watch satisfies the nogood and the other is assigned at higher decision level (or higher than the replay level of the satisfying one).
				return true;
			}
			return false;
		}

		private boolean watchInvariant(boolean atomSatisfies, int atomDecisionLevel, int otherLiteral, int otherDecisionLevel, Assignment.Entry otherEntry) {
			boolean otherSatisfies = otherEntry != null && isPositive(otherLiteral) != otherEntry.getTruth().toBoolean();
			if (atomDecisionLevel == Integer.MAX_VALUE && otherDecisionLevel == Integer.MAX_VALUE) {
				// Both watches are unassigned.
				return true;
			}
			if ((atomSatisfies && otherDecisionLevel >= atomDecisionLevel)
				|| (otherSatisfies && atomDecisionLevel >= otherDecisionLevel)) {
				// One watch satisfies the nogood and the other is assigned at higher decision level.
				return true;
			}
			return false;
		}
	}
}
