Skip to content

Max 3-SAT API Reference

Data

Data model for Max 3-SAT use case.

Max3satData

Bases: UcData

Data for the Max 3-SAT use case.

Attributes:

Name Type Description
name Literal['max3sat']

Identifier for this data type.
clauses list[Max3SatClause]

A list containing all clauses of the formula in CNF. Each clause is a tuple of three literals. Each literal is a tuple of (variable_index, is_positive). Example: ((0, True), (1, False), (2, True)) represents (x0 OR NOT x1 OR x2).
n_vars int

The number of variables in the problem.

plot(*, ax: Axes | None = None) -> Axes

Plot a bipartite graph of variables and clauses.

Variable nodes are placed on the left and clause nodes on the right. Solid edges indicate a positive literal; dashed edges indicate a negated literal.

Parameters:

Name Type Description Default
ax Axes | None

Matplotlib axes to draw on. Creates a new figure if None.

 None

Returns:

Type Description
Axes

The axes with the plot.

to_string() -> str

Print the data.

Returns:

Type Description
str

String representation of the data.

from_clause_list(clauses: list[Max3SatClause], n_vars: int | None = None) -> Max3satData staticmethod

Create Max3satData from a list of clauses.

Parameters:

Name Type Description Default
clauses list[Max3SatClause]

A list of clauses. Each clause is a tuple of three literals, where each literal is a tuple of (variable_index, is_positive). Example: [((0, True), (1, False), (2, True))].

 required
n_vars int | None

The number of variables. If None, inferred as one more than the highest variable index appearing in the clauses.

 None

Returns:

Type Description
Max3satData

A Max3sat data instance.

Raises:

Type Description
ValueError

If clauses is empty and n_vars is not provided, or if n_vars is less than the number of variables in the clauses.

Examples:

>>> clauses = [((0, True), (1, False), (2, True))]
>>> data = Max3satData.from_clause_list(clauses)

generate_random(size: int = 10, n_clauses: int | None = None, seed: int | None = None) -> Max3satData staticmethod

Generate a random instance.

Parameters:

Name Type Description Default
size int

Number of variables, by default 10.

 10
n_clauses int | None

Number of clauses. If None, defaults to 2 * size.

 None
seed int | None

Random seed for reproducibility, by default None.

 None

Returns:

Type Description
Max3satData

A randomly generated data instance.

Examples:

>>> data = Max3satData.generate_random(size=20, n_clauses=40, seed=42)

Formulation

Formulation for Max 3-SAT use case.

Max3satFormulation

Bases: UcFormulation[Max3satData, Max3satSolution]

Constraint-based formulation for Max 3-SAT.

Mathematical Formulation

Decision Variables: v[i] in {0, 1} -- truth value of variable i. s[c] in {0, 1} -- whether clause c is satisfied.

Objective: maximize sum_c s[c]

Constraints: For each clause c with literals (l1, l2, l3): s[c] <= expr(l1) + expr(l2) + expr(l3) where expr(i, True) = v[i], expr(i, False) = 1 - v[i].

to_string(data: Max3satData) -> str staticmethod

Format the formulation as a string.

Parameters:

Name Type Description Default
data Max3satData

The problem data.

 required

Returns:

Type Description
str

Formatted description.

formulate(data: Max3satData) -> Model staticmethod

Formulate the Max 3-SAT problem.

Parameters:

Name Type Description Default
data Max3satData

The problem data.

 required

Returns:

Type Description
Model

A Luna Model ready to be solved.

interpret(solution: Solution, data: Max3satData) -> Max3satSolution staticmethod

Extract a Max 3-SAT solution from the solver result.

Parameters:

Name Type Description Default
solution Solution

The solver solution.

 required
data Max3satData

The original problem data.

 required

Returns:

Type Description
Max3satSolution

Structured solution.

Raises:

Type Description
NoSolutionFoundError

If the solver did not find any solution.

Solution

Solution model for Max3sat use case.

Max3satSolution

Bases: UcSolution

Solution for the Max3sat use case.

Attributes:

Name Type Description
name Literal['max3sat']

Identifier for this solution type.
assignment dict[int, bool]

A dictionary mapping variable indices to their boolean assignment. Example: {0: True, 1: False} means x_0 is True, x_1 is False.
num_satisfied int

The number of clauses satisfied by this assignment.
satisfied_clause_indices list[int]

Indices of the clauses that are satisfied by the assignment.
is_valid bool

Whether the solution is valid (all variables assigned).

plot(data: Max3satData | None = None, *, ax: Axes | None = None) -> Axes

Plot the MAX-3SAT solution.

When data is provided, draws a bipartite variable-clause graph with clause nodes colored green (satisfied) or red (unsatisfied). Without data, displays a single horizontal bar showing the number of satisfied clauses.

Parameters:

Name Type Description Default
data Max3satData | None

Problem data. When provided, the full bipartite graph is drawn with satisfaction coloring.

 None
ax Axes | None

Matplotlib axes to draw on. Creates a new figure if None.

 None

Returns:

Type Description
Axes

The axes with the plot.

to_string() -> str

Print the solution.

Returns:

Type Description
str

String representation of the solution.

Instance

Instance model for Max3sat use case.

Max3satInstance

Bases: UcInstance[Max3satData, Max3satFormulation, Max3satSolution]

Instance combining data and formulation for Max3sat.

Collection

Collection of Max3sat instances.

Max3satCollection

Bases: UcInstanceCollection[Max3satInstance]

Collection of Max3sat instances.

This collection provides methods to generate benchmark instances with various characteristics for testing and evaluation.

from_random(min_size: int, max_size: int, num_instances: int = 1, seed: int | None = None) -> Max3satCollection classmethod

Generate random instances.

Parameters:

Name Type Description Default
min_size int

Minimum problem size.

 required
max_size int

Maximum problem size.

 required
num_instances int

Number of instances per size, by default 1.

 1
seed int | None

Random seed for reproducibility, by default None.

 None

Returns:

Type Description
Max3satCollection

Collection containing generated instances.

Examples:

>>> collection = Max3satCollection.from_random(
...     min_size=5,
...     max_size=10,
...     num_instances=3,
...     seed=42,
... )