State Management

CP solvers must efficiently save and restore states during search. MaxiCP is a trail-based solver: rather than copying the entire state at each choice point, it records only the incremental changes that occur during propagation and search on a stack called the trail. When the solver backtracks, it replays those changes in reverse to restore the previous state. We refer to [1] for a comprehensive introduction to trailing and its implementation in CP solvers.

The StateManager Interface

Source: StateManager.java

public interface StateManager {
    void saveState();               // Push a new save point
    void restoreState();            // Restore to last save point
    int getLevel();                 // Current depth in the search tree

    StateInt    makeStateInt(int initValue);
    <T> State<T> makeStateRef(T initValue);
    <K,V> StateMap<K,V> makeStateMap();
}

All stateful components of the solver — variable domains, propagation queues, the DFS engine, and even the symbolic model reference — are built on top of these primitives. For instance, the domain of a CPIntVar is backed by StateInt (a reversible integer) for its minimum and maximum bounds, and by a reversible sparse set for the full set of values.

The default implementation is Trailer.java.

Usage Example

StateManager sm = new Trailer();
StateInt counter = sm.makeStateInt(0);

sm.saveState();           // Level 0 -> Level 1
counter.setValue(10);     // Trail records: (counter, old=0)

sm.saveState();           // Level 1 -> Level 2
counter.setValue(42);     // Trail records: (counter, old=10)

sm.restoreState();        // Level 2 -> Level 1: counter = 10
sm.restoreState();        // Level 1 -> Level 0: counter = 0

Every time the solver descends in the search tree it calls saveState(), pushing a new level onto the trail stack. Any modification performed at that level is automatically undone when the solver calls restoreState() on backtrack.

Reversible Data Structures

Source: state/datastructures

The org.maxicp.state.datastructures package provides higher-level reversible data structures built on top of StateManager:

• StateStack<T> — a reversible stack.

• StateSparseSet — a reversible sparse set (used for integer variable domains) [6].

• StateTriPartition — a reversible three-way partition of a universe (required / possible / excluded); used by sequence variables.

• StateMap<K,V> — a reversible map backed by a HashMap.