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 LunaModel 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 | None = None, max_size: int | None = None, num_instances: int = 1, seed: int | None = None, *, sizes: Sequence[int] | None = None) -> Max3satCollection classmethod

Generate random instances.

Parameters:

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

    Minimum problem size.

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

    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.

  • sizes (Sequence[int] | None, default: None ) –

    Explicit sizes to generate, e.g. [10, 50, 100], instead of a range. Mutually exclusive with min_size/max_size, by default None.

Returns:

Examples:

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

filter_infeasible(max_runtime: float = 3600, *, quiet: bool = True) -> list[bool]

Drop the instances of this collection that have no feasible solution.

Every instance is formulated and handed to SCIP, which stops as soon as it finds the first feasible solution. An instance is removed from the collection when SCIP proves the model infeasible, when no solution turns up within max_runtime, or when formulating it fails altogether. This keeps randomly generated instances from breaking a downstream pipeline.

Parameters:

  • max_runtime (float, default: 3600 ) –

    SCIP time limit per instance in seconds. Must be positive. Defaults to 3600 seconds.

  • quiet (bool, default: True ) –

    Suppress the SCIP solver output.

Returns:

  • list[bool] –

    Feasibility mask over the instances as they were before filtering, in that order: True where the instance was kept, False where it was removed.

Raises: