Module core

Expand description

The core interfaces and structures used by the pumpkin solver.

Modules§

branching: Contains structures and traits to define the decision making procedure of the [Solver].
conflict_resolving: Contains algorithms for conflict analysis, core extraction, and clause minimisation. The algorithms use resolution and implement the 1uip and all decision literal learning schemes
constraints: Defines the main building blocks of constraints.
containers: Contains containers which are used by the solver.
convert_case: Converts to and from various cases.
optimisation: Contains structures related to optimissation.
options: Contains the options which can be passed to the [Solver].
predicates: Contains structures which represent certain predicates.
proof: Pumpkin supports proof logging for SAT and CP problems. During search, the solver produces a ProofLog, which is a list of deductions made by the solver.
propagation: Contains the main building blocks for propagators.
propagators
rand: Utilities for random number generation
results: Contains the outputs of solving using the [Solver].
state: Contains structures for the state containing the propagators and variables.
statistics: Contains structures related to the statistic logging of the [Solver]
termination: Contains the conditions which are used to determine when the [Solver] should terminate even when the state of the satisfaction/optimization problem is unknown.
variables: Contains the variables which are used by the [Solver].

conjunction: A macro which allows for the creation of a PropositionalConjunction.
create_statistics_struct: A macro for generating a struct for storing statistics.
declare_inference_label: Conveniently creates InferenceLabel for use in a propagator.
predicate: A macro which allows for the creation of a Predicate.

Duration: A Duration type to represent a span of time, typically used for system timeouts.
Function: A struct which represents a linear function over weighted Literals, and a constant term.
Instant: A measurement of a monotonically nondecreasing clock. Opaque and useful only with Duration.
Solver: The main interaction point which allows the creation of variables, the addition of constraints, and solving problems.
SolverStatistics: Structure responsible for storing several statistics of the solving process of the solver.
TestSolver: A container for CP variables, which can be used to test propagators.

ConstraintOperationError: Errors related to adding constraints to the [Solver].

Random: Abstraction for randomness, in order to swap out different source of randomness.

DefaultBrancher: A brancher which makes use of VSIDS [1] and solution-based phase saving (both adapted for CP).