Weighted MaxSAT Backend

The ocean.maxsat module exposes the weighted MaxSAT formulation backed by PySAT. The main public entry point is ocean.maxsat.Explainer; the remaining classes document the underlying Boolean model, variable bundles, and manager helpers used to build that formulation. For random forests, the public explainer also supports hard_voting=True to encode majority voting at the tree level instead of comparing averaged class proportions.

Weighted MaxSAT backend for optimal counterfactual search.

class BaseModel

Bases: ABC, WCNF

Base weighted CNF model used by the MaxSAT backend.

add_exactly_one(lits)

Add constraint that exactly one path is selected.

add_hard(lits, return_id=False)

Add a hard clause (must be satisfied).

Returns:

The clause ID if return_id is True, otherwise -1.

add_soft(lits, weight=1.0)

Add a soft clause with a given weight.

add_var(name)

build_vars(*variables)

get_var(name)

invalidate_solver_state()

Mark the formula as having changed non-monotonically.

property solver_epoch

vpool

class Explainer(ensemble, *, mapper, weights=None, hard_voting=False, epsilon=1, model_type=Type.MAXSAT)

Bases: Model, BaseExplainer

MaxSAT-based explainer for tree ensemble classifiers.

Initialize an empty weighted MaxSAT model for a parsed ensemble.

Parameters:

• trees – Parsed trees whose leaf activations define the ensemble class scores.

• mapper – Feature mapper aligning processed query coordinates with the Boolean feature encoding.

• weights – Optional tree weights.

• hard_voting – Whether to build the hard-voting MaxSAT encoding.

• max_samples – Reserved parameter used by compatible higher-level explainers.

• epsilon – Integer tie-breaking margin used in the score constraints.

• model_type – Backend builder variant.

Status = 'UNKNOWN'

explain(x, *, y, norm, return_callback=False, verbose=False, max_time=60, num_workers=None, random_seed=42, clean_up=True)

Solve one counterfactual query with the weighted MaxSAT backend.

Parameters:

• x – Query instance in the processed feature space.

• y – Target class enforced by the counterfactual.

• norm – Distance norm. The MaxSAT backend currently supports only 1.

• return_callback – Accepted for API compatibility but ignored by this backend.

• verbose – Whether to enable RC2 logging.

• max_time – Time limit in seconds.

• num_workers – Optional thread count forwarded to the MaxSAT solver.

• random_seed – Accepted for API compatibility but currently ignored.

• clean_up – Whether to remove query-specific clauses after the solve.

Returns:

The decoded counterfactual, or None when no feasible counterfactual is found within the given limits.

Return type:

Explanation | None

Raises:

RuntimeError – If the MaxSAT solver raises an error that is not UNSAT or timeout.

get_anytime_solutions()

Return the intermediate solution trace for the last MaxSAT solve.

Returns:

The MaxSAT backend currently exposes only the final solution.

Return type:

None

get_distance()

Return the post-processed distance of the last CF.

Returns:

Post-processed \(L_p\) distance for the last successful solve.

Return type:

float

Raises:

RuntimeError – If no explanation has been computed yet.

get_objective_value()

Return the weighted MaxSAT objective value of the last solve.

Returns:

Objective value rescaled back to the user-facing distance units.

Return type:

float

get_solving_status()

Return the status of the latest MaxSAT solve.

Returns:

Status string such as "OPTIMAL" or "INFEASIBLE".

Return type:

str

class Explanation(mapping=None, *, columns=None, validate=True)

Bases: Mapper[FeatureVar], BaseExplanation

Concrete explanation container returned by the MaxSAT backend.

Initialize a mapper from feature metadata and transformed columns.

Parameters:

• mapping – Mapping from original feature names to metadata objects.

• columns – Processed pandas index describing the transformed coordinates.

• validate – Whether to verify that mapping and columns are consistent.

format_continuous_value(f, idx, levels)

format_discrete_value(f, val, thresholds)

format_threshold_continuous_value(f, name)

format_threshold_discrete_value(f, name)

property query

to_numpy()

to_series()

property value

vget(i)

property x

class FeatureManager(mapper)

Bases: object

Manage MaxSAT feature variables for the counterfactual point \(x\).

This manager owns the Boolean or interval-selector variables representing the processed coordinates of the counterfactual explanation. The query \(\hat{x}\) only appears later in the soft objective clauses.

Wrap parsed features in MaxSAT-specific backend variables.

FEATURE_VAR_FMT = 'feature[{key}]'

build_features(model)

Create MaxSAT variables for the coordinates of \(x\).

property explanation

property mapper

property n_columns

property n_features

vget(i)

Return the literal representing processed coordinate i of x.

Returns:

Literal representing the requested coordinate.

Return type:

int

class FeatureVar(feature, name)

Bases: Var, FeatureKeeper

MaxSAT variable bundle associated with a single parsed feature.

TH_VAR_NAME_FMT = '{name}[{idx}]'

X_VAR_NAME_FMT = 'x[{name}]'

build(model)

property has_threshold_encoding

property split_threshold_values

threshold_index(value)

xget(code=None, mu=None)

class MaxSATSolver(solver_name='cadical195', TimeLimit=60, n_threads=1)

Bases: object

Thin RC2 wrapper to keep a stable interface.

property cost

delete()

Release any persistent RC2 state held by this wrapper.

model(v)

Return 1.0 if variable v is true in the model, 0.0 otherwise.

Args:

v: Variable to check in the model.

Returns:

1.0 if variable v is true in the model, 0.0 otherwise.

Raises:

ValueError: If no model has been found solve() must be called first.

solve(w)

property state_token

Opaque token identifying the currently cached RC2 instance.

property state_version

Monotonic version incremented whenever RC2 is rebuilt.

property synced_counts

Number of hard and soft clauses synchronized into RC2.

class Model(trees, mapper, *, weights=None, hard_voting=False, max_samples=0, epsilon=1, model_type=Type.MAXSAT)

Bases: BaseModel, FeatureManager, GarbageManager, TreeManager

Weighted MaxSAT formulation for tree ensemble explanations.

The Boolean feature variables encode the counterfactual point x and the Boolean tree variables encode the active leaf decisions p_(t,l).

Initialize an empty weighted MaxSAT model for a parsed ensemble.

Parameters:

• trees – Parsed trees whose leaf activations define the ensemble class scores.

• mapper – Feature mapper aligning processed query coordinates with the Boolean feature encoding.

• weights – Optional tree weights.

• hard_voting – Whether to build the hard-voting MaxSAT encoding.

• max_samples – Reserved parameter used by compatible higher-level explainers.

• epsilon – Integer tie-breaking margin used in the score constraints.

• model_type – Backend builder variant.

DEFAULT_EPSILON = 1

class Type(*values)

Bases: Enum

MAXSAT = 'MAXSAT'

add_objective(x, *, norm=1)

Encode the \(L_1\) distance \(d_1(x, \hat{x})\) as soft clauses.

Parameters:

• x – Query point \(\hat{x}\) in the processed feature space. The code parameter is named x, but mathematically it represents the query.

• norm – Distance norm. The MaxSAT backend currently supports only \(L_1\).

Raises:

ValueError – If x does not have the expected size or norm is unsupported.

build()

Create the Boolean encoding of features, leaves, and path consistency.

After build(), the model contains the Boolean variables encoding the counterfactual point \(x\), the active leaves \(p_{t,\ell}\), and the hard clauses linking both.

cleanup()

Remove query-specific soft and hard clauses from the MaxSAT model.

The structural Boolean encoding of \(x\) and \(p_{t,\ell}\) stays in place, while the objective clauses and target-class clauses for the previous query \(\hat{x}\) are removed.

set_majority_class(y, *, op=0)

Enforce the target class through hard score constraints.

For every competing class, the backend encodes the pairwise dominance condition

\[f_y(x) \ge f_c(x) + \varepsilon_c\]

Raises:

ValueError – If y is not a valid class index.

class TreeManager(trees, *, weights=None)

Bases: object

Manage MaxSAT tree variables and the support encoding of \(f\).

Each TreeVar encodes the active leaf decisions \(p_{t,\ell}\) of one tree. The stored function representation is a Boolean support view of \(f(x)\) used by the MaxSAT encoding.

Initialize the tree manager and validate the estimator weights.

TREE_VAR_FMT = 'tree[{t}]'

build_trees(model)

Create the MaxSAT tree variables and cache \(f(x)\) support.

property estimators

property function

property n_classes

property n_estimators

property n_trees

property shape

property trees

weighted_function()

Return the Boolean support representation used for \(f(x)\).

Each entry (op, c) stores the leaf literals whose active leaf supports class \(c\) for output op.

Returns:

Boolean support literals grouped by output and class.

Return type:

dict[tuple[NonNegativeInt, NonNegativeInt], list[int]]

property weights

class TreeVar(tree, name)

Bases: Var, TreeKeeper, Mapping[NonNegativeInt, object]

MaxSAT literals encoding the active leaf of one parsed tree.

CLASS_VAR_NAME_FMT = '{name}_class'

PATH_VAR_NAME_FMT = '{name}_path'

build(model)

cget(class_id)