modules.applications.optimization.sat.sat.SAT

class SAT

Bases: Optimization

The SAT (Satisfiability) problem plays a crucial role in the field of computational optimization. In the context of vehicle manufacturing, it is essential to test various pre-series vehicle configurations to ensure they meet specific requirements before production begins. This testing involves making sure that each vehicle configuration complies with several hard constraints related to safety, performance, and buildability while also fulfilling soft constraints such as feature combinations or specific requirements for testing. The SAT problem models these constraints in a way that enables a systematic approach to determine feasible vehicle configurations and minimize the need for excessive physical prototypes.

This problem is modeled as a Max-SAT problem, where the aim is to find a configuration that satisfies as many constraints as possible while balancing between the number of satisfied hard and soft constraints. The formulation uses a conjunctive normal form (CNF) representation of logical expressions to model the dependencies and incompatibilities between various features and components in vehicle assembly. By leveraging optimization algorithms, the SAT module aims to produce a minimal but sufficient set of configurations, ensuring that all necessary tests are performed while minimizing resource usage. This approach helps in creating a robust testing framework and reducing the overall cost of vehicle development.

To solve the SAT problem, various approaches are employed, including translating the CNF representation into different quantum and classical optimization mappings such as QUBO (Quadratic Unconstrained Binary Optimization) or Ising formulations. These mappings make the SAT problem suitable for solving on quantum computers and classical annealers. The SAT problem in this module is implemented with a flexible interface, allowing integration with a range of solvers that can exploit different computational paradigms, making it adaptable for a variety of hardware and optimization backends.

__init__()

Constructor method.

Methods

__init__()	Constructor method.
evaluate(solution)	Calculates the quality of the solution.
generate_problem(config)	Generates a vehicle configuration problem out of a given config.
get_application()	Gets the application.
get_available_submodule_options()	Gets the list of available options.
get_available_submodules(option)	If the module has submodules depending on certain options, this method should adjust the submodule_options accordingly.
get_default_submodule(option)	Returns the default submodule based on the provided option.
get_depending_parameters(option, config)	If the module has parameters depending on certain options, this method should return the parameters for the given option.
get_parameter_options()	Returns the configurable settings for this application.
get_requirements()	Return requirements of this module.
get_solution_quality_unit()	Returns the unit of the evaluation.
get_submodule(option)	Submodule is instantiated according to the information given in self.sub_options.
postprocess(input_data, config, **kwargs)	For optimization problems, we process the solution here, then validate and evaluate it.
preprocess(input_data, config, **kwargs)	For optimization problems, we generate the actual problem instance in the preprocess function.
process_solution(solution)	Most of the time the solution has to be processed before it can be validated and evaluated.
save(path, iter_count)	Save the constraints and tests to files in CNF format.
validate(solution)	Validate a given solution against the constraints.
visualize_solution(processed_solution, path)	Creates visualizations of a processed and validated solution and writes them to disk.

class Config

Bases: TypedDict

Attributes of a valid config.

variables: int
clvar_ratio_cons: float
clvar_ratio_test: float
problem_set: int
max_tries: int

clear() → None.  Remove all items from D.

copy() → a shallow copy of D

fromkeys(value=None, /)

Create a new dictionary with keys from iterable and values set to value.

get(key, default=None, /)

Return the value for key if key is in the dictionary, else default.

items() → a set-like object providing a view on D's items

keys() → a set-like object providing a view on D's keys

pop(k[, d]) → v, remove specified key and return the corresponding value.

If the key is not found, return the default if given; otherwise, raise a KeyError.

popitem()

Remove and return a (key, value) pair as a 2-tuple.

Pairs are returned in LIFO (last-in, first-out) order. Raises KeyError if the dict is empty.

setdefault(key, default=None, /)

Insert key with a value of default if key is not in the dictionary.

Return the value for key if key is in the dictionary, else default.

update([E, ]**F) → None.  Update D from mapping/iterable E and F.

If E is present and has a .keys() method, then does: for k in E.keys(): D[k] = E[k] If E is present and lacks a .keys() method, then does: for k, v in E: D[k] = v In either case, this is followed by: for k in F: D[k] = F[k]

values() → an object providing a view on D's values

evaluate(solution: dict) → tuple[float, float]

Calculates the quality of the solution.

Parameters:

solution -- Dictionary containing the solution

Returns:

Tour length, time it took to calculate the tour length

generate_problem(config: Config) → tuple[And, list]

Generates a vehicle configuration problem out of a given config. Returns buildability constraints (hard constraints) and tests (soft constraints), the successful evaluation of which we try to maximize. Both are given in nnf form, which we then convert accordingly.

Parameters:

config -- Configuration parameters for problem generation

Returns:

A tuple containing the problem, number of variables, and other details

get_application() → any

Gets the application.

Returns:

self.application

get_available_submodule_options() → list

Gets the list of available options.

Returns:

List of module options

get_available_submodules(option: list) → list

If the module has submodules depending on certain options, this method should adjust the submodule_options accordingly.

Parameters:

option -- List of chosen options

Returns:

List of available submodules

get_default_submodule(option: str) → Core

Returns the default submodule based on the provided option.

Parameters:

option -- Option specifying the submodule

Returns:

Instance of the corresponding submodule

Raises:

NotImplementedError -- If the option is not recognized

get_depending_parameters(option: str, config: dict) → dict

If the module has parameters depending on certain options, this method should return the parameters for the given option.

Parameters:

• option -- The chosen option

• config -- Current config dictionary

Returns:

The parameters for the given option

get_parameter_options() → dict

Returns the configurable settings for this application.

Returns:

Dictionary with configurable settings

return {
        "variables": {
            "values": list(range(10, 151, 10)),
            "custom_input": True,
            "allow_ranges": True,
            "postproc": int,
            "description": "How many variables do you need?"
        },
        "clvar_ratio_cons": {
            "values": [2, 3, 4, 4.2, 5],
            "custom_input": True,
            "allow_ranges": True,
            "postproc": int,
            "description": "What clause-to-variable ratio do you want for the (hard) constraints?"
        },
        "clvar_ratio_test": {
            "values": [2, 3, 4, 4.2, 5],
            "custom_input": True,
            "allow_ranges": True,
            "postproc": int,
            "description": "What clause-to-variable ratio do you want for the tests (soft con.)?"
        },
        "problem_set": {
            "values": list(range(10)),
            "description": "Which problem set do you want to use?"
        },
        "max_tries": {
            "values": [100],
            "description": "Maximum number of tries to create problem?"
        }
    }

static get_requirements() → list[dict]

Return requirements of this module.

Returns:

List of dict with requirements of this module

get_solution_quality_unit() → str

Returns the unit of the evaluation.

Returns:

String with the unit

get_submodule(option: str) → Core

Submodule is instantiated according to the information given in self.sub_options. If self.sub_options is None, get_default_submodule is called as a fallback.

Parameters:

option -- String with the options

Returns:

Instance of a module

postprocess(input_data: any, config: dict, **kwargs) → tuple[any, float]

For optimization problems, we process the solution here, then validate and evaluate it.

Parameters:

• input_data -- Data which should be evaluated for this optimization problem

• config -- Config for the problem creation

• kwargs -- Optional additional arguments

Returns:

Tuple with results and the postprocessing time

preprocess(input_data: any, config: dict, **kwargs) → tuple[any, float]

For optimization problems, we generate the actual problem instance in the preprocess function.

Parameters:

• input_data -- Input data (usually not used in this method)

• config -- Config for the problem creation

• kwargs -- Optional additional arguments

Returns:

Tuple with output and the preprocessing time

process_solution(solution: any) → tuple[any, float]

Most of the time the solution has to be processed before it can be validated and evaluated. This might not be necessary in all cases, so the default is to return the original solution.

Parameters:

solution -- Proposed solution

Returns:

Tuple with processed solution and the execution time to process it

save(path: str, iter_count: int) → None

Save the constraints and tests to files in CNF format.

Parameters:

• path -- The directory path where the files will be saved.

• iter_count -- The iteration count to include in the filenames.

validate(solution: dict) → tuple[bool, float]

Validate a given solution against the constraints.

Parameters:

solution -- The solution to validate

Returns:

True if the solution is valid, False otherwise, and time it took to complete

visualize_solution(processed_solution: any, path: str) → None

Creates visualizations of a processed and validated solution and writes them to disk. Override if applicable. Default is to do nothing.

Parameters:

• processed_solution -- A solution that was already processed by process_solution()

• path -- File path for the plot

Returns:

None