Encoding Layer API#

The hermax.encoder package provides a unified way for compiling Pseudo-Boolean and Cardinality constraints efficiently.

PBCompiler#

class hermax.encoder.PBCompiler#

Bases: object

The central entry point for compiling batches of Pseudo-Boolean (PB) constraints.

PBCompiler ensures that the SAT encoding is as compact and efficient as possible.

classmethod compile_batch(items, amo_groups, eo_groups, top_id)#

Compiles a batch of PB constraints into SAT.

This method performs a multi-stage compilation process:

  1. Clustering: Analysis of variable connectivity to find related constraint sets.

  2. K-Merge Extraction: Solving for optimal shared bases within clusters.

  3. Priority Encoding: Sorting remaining constraints to maximize structural learning.

  4. In-Batch Learning: Updating the structural knowledge base in real-time.

Parameters:

  • items (List[PBItem]) – A list of PBItem objects to be compiled.

  • amo_groups (List[List[int]]) – Known At-Most-One literal groups.

  • eo_groups (List[List[int]]) – Known Exactly-One literal groups.

  • top_id (int) – The current maximum variable ID in the solver.

Returns:

A list of CNFPlus objects containing the generated SAT clauses and auxiliary variables.

classmethod compile_batch_with_options(items, amo_groups, eo_groups, top_id, *, merge_pb_optimization, kmerge_config=None)#
Parameters:

  • items (List[PBItem])

  • amo_groups (List[List[int]])

  • eo_groups (List[List[int]])

  • top_id (int)

  • merge_pb_optimization (bool)

  • kmerge_config (KMergeConfig | None)

PBItem#

class hermax.encoder.PBItem#

Bases: object

Represents a single Pseudo-Boolean or Cardinality constraint for compilation.

Parameters:

  • lits – DIMACS-style literals.

  • bound – The Right-Hand Side (RHS) value.

  • weights – Non-negative integer weights. If None, all weights are assumed to be 1.

  • cmp_op – Comparison operator ('<=' or '==').

lits: List[int]#
bound: int#
weights: List[int] | None = None#
cmp_op: str = '<='#
property is_cardinality: bool#

Returns True if all weights are 1 (or implicit).

get_weights()#

Returns the actual weights list, materializing unit weights if necessary.

Return type:

List[int]

__init__(lits, bound, weights=None, cmp_op='<=')#
Parameters:

  • lits (List[int])

  • bound (int)

  • weights (List[int] | None)

  • cmp_op (str)

Return type:

None

References#

The encoders used in Hermax are state-of-the-art research in SAT encoding techniques. References:

  • PySAT (Cardinality): Hermax uses pycard from the PySAT toolkit.

    • Reference: Ignatiev, A., Morgado, A., & Marques-Silva, J. (2018). PySAT: A Python Toolkit for Prototyping with SAT Oracles.

  • PBLib (Pseudo-Boolean): We use the PBLib library for our PB encoding strategies.

    • Reference: Manthey, N., Philipp, T., & Steinke, P. (2015). PBLib - A Library for Encoding Pseudo-Boolean Constraints into CNF.

  • PB(AMO) (PB + AMO): We provide bindings to PB(AMO) encodings, which we exploit in our modelling layer.

    • Reference: Bofill, M., Garcia, J., Suy, J., & Villaret, M. (2021). SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints.