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.


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

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

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

Simplify the CSP using DPLL algorithm.

dpll_apply_assignments(executor, ...)

Apply the assignments to the constraints.

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_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:


Find a function application whose arguments are all determined.

dpll_find_typegen_variable(executor, dtype)



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


An exception raised when the CSP is not solvable.