Module Jumping (.ml)

module Jumping: sig .. end

random jumps within the search space

based on an extension of "A Random Jump Strategy for Combinatorial Search" by Hantao Zhang.

based on the remaining time, or just every once in a while, a jump forward in the current search space is done, in order to increase the likelihood of finding a model, and not wasting all time in a deep fruitless branch.

to keep completeness, the search space positions jumped from are recorded as guiding paths. if the search space has been exhausted modulo jumped over parts, those are revisited by replaying the guiding paths in a non-redundant way.

the downsides of this approach are

recomputation of some parts of the search space, though only unit propagation and no splitting is repeated
to remain complete, backjumping can not be used for the part of the branch that remains after a jump

Types

type config = Config.config

type statistic = Statistic.statistic

type literal = Term.literal

type state = State.state

type choice_point = State.choice_point

type bound = Bound.bound

type guiding_step =

`\|`	`Left of literal`	`(*`	replay only the left split - this split was 'above' the destination of a random jump. i.e. it was not jumped over, and it (and its corresponding right split) was left in the search space after the jump.	`*)`
`\|`	`Right of literal`	`(*`	replay only the right split - the left split has been explored before the random jump, i.e. this was already a right split when the random jump happened.	`*)`
`\|`	`Split of literal`	`(*`	replay a full split decision - this split has been jumped over when doing the random jump, so it and its corresponding right split must still be explored.	`*)`

a recorded step of a guiding path

type guiding_path = guiding_step list

replaying this guiding path in order recreates the search space remaining from the corresponding jump. each split decision of the original derivation branch is recorded in a guiding_step.

type jumping

initiates jumps, and record guiding paths.

Functions

Creation

val create : config ->
       statistic -> state -> bound -> jumping

Jumping

val jump : jumping -> choice_point option

must be called upon each left split decision. decides if a jump should occur, and returns the choice point to retract in that case. the corresponding right split must be applied to the remaining branch in order to avoid recomputing the skipped branch again.

Replay

val finished : jumping -> bool

is not guided path recorded? i.e. no jumped over search space is left to be explored.

val replay : jumping -> state -> guiding_path

reinitializes with state, bound, and the internal statistics.

returns the oldest recorded guiding path, and removes it from jumping.
Raises Not_found if not guiding path is stored.

Representation

val guiding_path_to_string : guiding_path -> string