concepts.dm.crow.csp_solver.dpll_sampling#

The DPLL-Sampling algorithm for solving CSPs. This algorithm is specifically designed for solving CSPs with mixed Boolean and continuous variables. At a high level, the algorithm uses DPLL-style search to find a solution to Boolean variables. After the value for all Boolean variables are fixed, the algorithm uses a sampling-based method to find a solution to the continuous variables.

Functions

dpll_apply_assignments(executor, ...)

Apply the assignments to the constraints.

dpll_apply_assignments_with_simulation(...)

dpll_filter_deterministic_clauses(executor, ...)

Filter out Boolean constraints that have been determined. For example, AND(x, y, z) == true, then

dpll_filter_deterministic_equal(executor, ...)

Filter the constraints to remove the ones that are determined to be equal.

dpll_filter_duplicated_constraints(executor, ...)

Filter out duplicated constraints.

dpll_filter_unused_rhs(executor, ...)

Filter out constraints that only appear once in the RHS of the constraints.

dpll_filter_unused_simulation_rhs(executor, ...)

Filter out simulation constraints that only appear once in the RHS of the constraints.

dpll_find_bool_variable(executor, ...)

Find a Boolean variable that is not determined.

dpll_find_gen_variable_combined(executor, ...)

Combine the generator matching in the following order:

dpll_find_grounded_function_application(...)

Find a function application whose arguments are all determined.

dpll_find_typegen_variable(executor, dtype)

dpll_simplify(executor, csp[, ...])

Simplify the CSP using DPLL algorithm.

dpll_solve(executor, csp, *[, ...])

Solve the constraint satisfaction problem using the DPLL-sampling algorithm.

Exceptions

CSPNoGenerator

An exception raised when there is no generator that can be matched in order to solve the CSP.

CSPNotSolvable

An exception raised when the CSP is not solvable.