Utilities#

List of Functions#

hermax.core.utils.normalize_wcnf_formula

Normalize WCNF-like inputs to PySAT WCNF when needed.

Module Description#

Hermax supports PySAT WCNF formulas natively and can optionally accept OptiLog WCNF formulas when OptiLog is installed [1] [2].

The function hermax.core.utils.normalize_wcnf_formula() provides the central conversion path used by solver constructors:

  • PySAT WCNF/WCNFPlus inputs are passed through unchanged

  • OptiLog WCNF inputs are converted into PySAT WCNF

  • None is preserved.

This keeps solver wrappers simple and ensures consistent behavior across all Hermax backends.

Optional OptiLog Compatibility#

Install with OptiLog support using:

pip install "hermax[optilog]"

OptiLog support is optional because OptiLog has its own licensing model. PySAT remains a required dependency of Hermax.

Based on OptiLog’s documented WCNF API (hard_clauses and soft_clauses), Hermax converts:

  • each item in hard_clauses into a hard clause in PySAT WCNF

  • each pair (weight, clause) in soft_clauses into a PySAT soft clause with that weight.

API Details#

class hermax.core.utils.WCNFData#

Stable view of a WCNF-like input used by solver adapters.

Third-party formula implementations do not all expose PySAT’s exact hard/soft/wght layout. Keep that compatibility at this boundary; solver implementations should consume this representation rather than probe arbitrary formula objects themselves.

hard: list[list[Any]]#
soft: list[tuple[list[Any], Any]]#
num_vars: int#
__init__(hard, soft, num_vars)#
Parameters:

  • hard (list[list[Any]])

  • soft (list[tuple[list[Any], Any]])

  • num_vars (int)

Return type:

None

hermax.core.utils.normalize_wcnf_formula(formula)#

Normalize WCNF-like inputs to PySAT WCNF when needed.

Returns None unchanged. Returns PySAT WCNF/WCNFPlus unchanged. Converts OptiLog WCNF into PySAT WCNF. Returns any other object unchanged, so existing wrapper-specific best-effort loaders can still handle custom WCNF-like objects.

Parameters:

formula (Any)

Return type:

Any

hermax.core.utils.extract_wcnf_data(formula)#

Extract clauses from a PySAT or compatible WCNF object.

Compatibility attribute access is deliberately contained here. The returned lists are copies, so adapters can normalize them without mutating a caller-owned formula.

Parameters:

formula (Any)

Return type:

WCNFData

References#