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

  • ax (Axes | None, default: None ) –

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

Returns:

  • Axes –

    The axes with the plot.

to_string() -> str

Print the data.

Returns:

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

  • 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))].

  • n_vars (int | None, default: None ) –

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

Returns:

Raises:

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

  • size (int, default: 10 ) –

    Number of variables, by default 10.

  • n_clauses (int | None, default: None ) –

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

  • seed (int | None, default: None ) –

    Random seed for reproducibility, by default None.

Returns:

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:

Returns:

  • str –

    Formatted description.

formulate(data: Max3satData) -> Model staticmethod

Formulate the Max 3-SAT problem.

Parameters:

Returns:

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

  • solution (Solution) –

    The solver solution.

  • data (Max3satData) –

    The original problem data.

Returns:

Raises:

Solution

Solution model for Max3sat use case.

Max3satSolution

Bases: UcSolution

Solution for the Max3sat use case.

Attributes:

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

  • data (Max3satData | None, default: None ) –

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

  • ax (Axes | None, default: None ) –

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

Returns:

  • Axes –

    The axes with the plot.

to_string() -> str

Print the solution.

Returns:

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

  • min_size (int) –

    Minimum problem size.

  • max_size (int) –

    Maximum problem size.

  • num_instances (int, default: 1 ) –

    Number of instances per size, by default 1.

  • seed (int | None, default: None ) –

    Random seed for reproducibility, by default None.

Returns:

Examples:

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