Bounds

This module solves instances with unbounded cardinalities in an incremental fashion. A max_bound is used to turn all unbounded cardinalities into bounded cardinalities. This max_bound is increased (and possibly also decreased) until a (minimal) bound is found.

This can be done using standard single-shot solving or multi-shot solving. Both approaches use a common solver class. For multi-shot solving a specific multi-shot application class is used.

The max_bound can either be increased in a linear or exponential fashion. In both approaches it is possible to supply an initial value.

Once a satisfiable max_bound has been found, solving continues to compute what the minimal satisfiable value for max_bound is.

coomsuite.bounds

General helper functions for solving unbounded cardinalities.

get_bound_iter(algorithm: str, start: int, step: Optional[int] = None, base: Optional[float] = None) -> Iterator[int]

Get an iterator over the bounds for a selected algorithm.

Note that the iterator starts after the start value.

Parameters:

Name	Type	Description	Default
algorithm	str	either "linear" or "exponential"	required
start	int	value after which the iterator starts	required
step	int	step size for linear/exponential base for iteration	None

next_bound_converge(unsat_bound: int, sat_bound: int) -> Optional[int]

Determine the next bound (between unsat_bound and sat_bound) for converging to the minimal bound

Returns:

Type	Description
Optional[int]	Optional[int]: The next bound to check, or None if sat_bound is already the minimal bound