PB(AMO) API#

Hermax includes an internal structured pseudo-Boolean layer for constraints that can exploit known AMO/EO structure [1].

This is useful for constraints of the form:

sum(w_i * x_i) <= K

when some of the x_i are known to belong to at-most-one (AMO) or exactly-one (EO) groups. Instead of flattening the whole constraint into an ordinary PB, the structured layer can route it to encoders that treat those groups efficiently.

Current Status#

The structured PB API is part of the hermax.encoder package:

from hermax.encoder import PBAMOEnc
from hermax.encoder.pbamo import EncType, OverlapPolicy

Two entry points are available:

  • PBAMOEnc.leq(...) for a disjoint AMO partition you already know

  • PBAMOEnc.auto_leq(...) for overlapping AMO / EO candidates, automatic overlap resolution, and automatic routing between flat CardEnc / PBEnc and structured encoders

Disjoint Partition API#

Use leq(...) when you already have a clean disjoint partition:

examples/model/32_structuredpb_disjoint.py#
from hermax.encoder.pbamo import EncType, PBAMOEnc


def main() -> None:
    lits = [1, 2, 3, 4]
    weights = [2, 3, 4, 7]
    groups = [[1, 2], [3, 4]]
    bound = 8

    cnf = PBAMOEnc.leq(
        lits=lits,
        weights=weights,
        groups=groups,
        bound=bound,
        encoding=EncType.rggt,
    )

    print("encoding=rggt")
    print(f"nv={cnf.nv}")
    print(f"clauses={len(cnf.clauses)}")
    print("first_clauses=")
    for clause in cnf.clauses[:6]:
        print(clause)


if __name__ == "__main__":
    main()

Output#

Structured PB with a disjoint AMO partition#
$ python examples/model/32_structuredpb_disjoint.py
encoding=rggt
nv=6
clauses=6
first_clauses=
[-1, -2]
[-3, -4]
[-1, 5]
[-2, 5]
[-5, -4, 6]
[-6]

Arguments:

  • lits: PB literals

  • weights: integer PB coefficients

  • groups: disjoint AMO partition over lits

  • bound: right-hand side of sum(w_i * x_i) <= bound

  • encoding: one of mdd, gswc, ggpw, gmto, rggt, or best

  • emit_amo: whether to also emit pairwise AMO clauses for the groups

Automatic Overlap API#

Use auto_leq(...) when you have overlapping candidates instead of a clean partition, or when you want the internal router to decide whether a unit-weight cardinality / pseudo-Boolean constraint should stay flat or move to the structured side:

examples/model/33_structuredpb_auto_overlap.py#
from hermax.encoder.pbamo import OverlapPolicy, PBAMOEnc


def main() -> None:
    lits = [1, 2, 3, 4, 5]
    weights = [6, 4, 7, 5, 3]
    bound = 10
    amo_groups = [[1, 2, 3], [2, 3, 4]]
    eo_groups = [[4, 5]]

    cnf = PBAMOEnc.auto_leq(
        lits=lits,
        weights=weights,
        bound=bound,
        amo_groups=amo_groups,
        eo_groups=eo_groups,
        overlap_policy=OverlapPolicy.paper_best_fit_dynamic_future,
    )

    print("overlap_policy=paper_best_fit_dynamic_future")
    print(f"nv={cnf.nv}")
    print(f"clauses={len(cnf.clauses)}")
    print("first_clauses=")
    for clause in cnf.clauses[:8]:
        print(clause)


if __name__ == "__main__":
    main()

Output#

Structured PB with overlapping AMO and EO candidates#
$ python examples/model/33_structuredpb_auto_overlap.py
overlap_policy=paper_best_fit_dynamic_future
nv=13
clauses=22
first_clauses=
[6]
[-2, -7]
[-4, -7]
[7, -8]
[-1, -8]
[-5, -2, -9]
[9, -10]
[-4, -10]

auto_leq(...) does three things:

  1. resolves overlapping AMO / EO candidates into one disjoint partition

  2. decides whether the instance should stay in ordinary flat CardEnc / PBEnc or go to the structured encoders

  3. if routed to the structured side, chooses the structured encoder

The original overlapping AMO / EO constraints are still emitted explicitly as clauses, so the overlap resolution policy only decides which partition is fed to the structured encoder.

Overlap Policy#

Two overlap policies are available:

  • baseline_paper

  • paper_best_fit_dynamic_future

baseline_paper is the direct paper-style greedy baseline [1]:

  • process literals in input order

  • place each literal into the first compatible existing group

  • otherwise start a new group

paper_best_fit_dynamic_future is the current improved policy built on top of that baseline:

  • choose the next literal dynamically, prioritizing the hardest literals first

  • among compatible groups, choose the best fit rather than the first fit

  • prefer placements with:

    • stronger EO support

    • stronger AMO/EO overlap support

    • more future compatibility for remaining literals

    • larger reusable groups

The paper baseline is: “place literals in order and use the first group that works”; our policy is: “place the hardest literal next, and put it where it fits best without harming future placements”

References#