omnibias.boolean.torch.ops.solver

0.1.0a2AlphaPython >=3.10Apache-2.0

Boolean truth tables, multilinear extensions, algebraic spectra, and finite-temperature gate systems.

import omnibias.boolean.torch.ops.solver

Module contract & mathematical conventions

Differentiable Boolean equation/system solver (torch): propose-and-verify.

A BooleanSystem bundles a set of Boolean equations phi_k(x) = 0. Two solve paths:

an **exact GF(2) fast-path** (omnibias.boolean._core.gf2_solve) used automatically when every equation is XOR-linear -- Gaussian elimination is polynomial-time and genuinely collapses that search space;
a **beta-annealed soft search** otherwise: the unknown bits are sigmoid latents x = sigmoid(beta * theta) (the free parameters c), the residual is the sum of squared multilinear-extension violations of the gates, and beta is annealed beta -> inf with omnibias.binary.BetaAnnealScheduler.

The soft search is a **heuristic**: it proposes a relaxed assignment, hardens it, and then *verifies it against the exact Boolean system*. verified=False means the heuristic did not find a solution -- not that none exists.

Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.

Module source ↗Source revision 9a2d73df0573Running reference examples →

Imports & aliases

These names share a definition with another public module. Follow a name for its full contract, parameters, and examples.

Import from this module	Canonical reference
`BetaAnnealScheduler`	`omnibias.binary.BetaAnnealScheduler`

CLASS

BooleanSystem

omnibias.boolean.torch.ops.BooleanSystemSource ↗

class BooleanSystem

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

A system of Boolean equations phi_k(x) = 0 (each phi_k a truth table).

Parameters

Name	Type & default	Contract
`n`dataclass field	`int`Required	See the operation contract and implementation below.
`constraints`dataclass field	`tuple[TruthTable, ...]`Required	See the operation contract and implementation below.

Executed regression · inconsistent linear system

Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_inconsistent_linear_system() -> None:
    sys = BooleanSystem.from_predicates(
        [lambda a: a == 0, lambda a: a == 1], n=1
    )
    res = solve(sys)
    assert res.method == "gf2"
    assert not res.verified
    assert res.assignment is None

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_inconsistent_linear_system" -q

Regression example · gf2 fast path linear unique

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_gf2_fast_path_linear_unique() -> None:
    # x0 ^ x1 = 1 and x1 = 1  ->  x1 = 1, x0 = 0 (unique).
    sys = BooleanSystem.from_predicates(
        [lambda a, b: (a ^ b) == 1, lambda a, b: b == 1], n=2
    )
    assert sys.is_linear()
    res = solve(sys)
    assert res.method == "gf2"
    assert res.verified
    assert res.assignment == (0, 1)

python -m pytest packages/omnibias-boolean/tests/test_solver.py -k test_gf2_fast_path_linear_unique -q

Fields & methods

nfield

n: int

Declared int field on BooleanSystem. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

constraintsfield

constraints: tuple[TruthTable, ...]

Declared tuple[TruthTable, ...] field on BooleanSystem. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

from_constraintsmethod

from_constraints(cls, constraints: Sequence[TruthTable]) -> BooleanSystem

Build from constraint truth tables (1 = violated).

Parameters

Name	Type & default	Contract
`constraints`positional-or-keyword	`Sequence[TruthTable]`Required	See the operation contract and implementation below.

Returns: BooleanSystem

Validation & failure cases

When not constraints, raises ValueError('need at least one constraint').
When num_vars(c) != n, raises ValueError('all constraints must share the same arity').

Executed regression · inconsistent linear system

Full file, imports & fixtures ↗

def test_inconsistent_linear_system() -> None:
    sys = BooleanSystem.from_predicates(
        [lambda a: a == 0, lambda a: a == 1], n=1
    )
    res = solve(sys)
    assert res.method == "gf2"
    assert not res.verified
    assert res.assignment is None

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_inconsistent_linear_system" -q

Method implementation

    def from_constraints(cls, constraints: Sequence[TruthTable]) -> BooleanSystem:
        """Build from constraint truth tables (``1`` = violated)."""
        if not constraints:
            raise ValueError("need at least one constraint")
        n = num_vars(constraints[0])
        for c in constraints:
            if num_vars(c) != n:
                raise ValueError("all constraints must share the same arity")
        return cls(n=n, constraints=tuple(tuple(c) for c in constraints))

View source ↗

from_predicatesmethod

from_predicates(cls, predicates: Sequence[Callable[..., bool]], n: int) -> BooleanSystem

Build from predicates; phi_k is 0 exactly where pred_k holds.

Parameters

Name	Type & default	Contract
`predicates`positional-or-keyword	`Sequence[Callable[..., bool]]`Required	See the operation contract and implementation below.
`n`positional-or-keyword	`int`Required	See the operation contract and implementation below.

Returns: BooleanSystem

Executed regression · inconsistent linear system

Full file, imports & fixtures ↗

def test_inconsistent_linear_system() -> None:
    sys = BooleanSystem.from_predicates(
        [lambda a: a == 0, lambda a: a == 1], n=1
    )
    res = solve(sys)
    assert res.method == "gf2"
    assert not res.verified
    assert res.assignment is None

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_inconsistent_linear_system" -q

Method implementation

    def from_predicates(
        cls, predicates: Sequence[Callable[..., bool]], n: int
    ) -> BooleanSystem:
        """Build from predicates; ``phi_k`` is ``0`` exactly where ``pred_k`` holds."""
        constraints = [
            tuple(0 if pred(*bits) else 1 for bits in all_assignments(n))
            for pred in predicates
        ]
        return cls.from_constraints(constraints)

View source ↗

residual_softmethod

residual_soft(self, x: Tensor) -> Tensor

Sum of squared multilinear-extension violations at a soft point x.

Parameters

Name	Type & default	Contract
`x`positional-or-keyword	`Tensor`Required	See the operation contract and implementation below.

Returns: Tensor

Validation & failure cases

When x.shape[-1] != self.n, raises ValueError(f'x must have last dim {self.n}, got {x.shape}').

Executed regression · anneal solves nonlinear system

Full file, imports & fixtures ↗

def test_anneal_solves_nonlinear_system() -> None:
    # x0 & x1 = 1  and  x1 | x2 = 1  ->  x0 = 1, x1 = 1, x2 free. Nonlinear (AND).
    sys = BooleanSystem.from_predicates(
        [lambda a, b, c: (a & b) == 1, lambda a, b, c: (b | c) == 1], n=3
    )
    assert not sys.is_linear()
    res = solve(sys, steps=200, restarts=12, seed=0)
    assert res.method == "anneal"
    assert res.verified
    assert res.assignment is not None and sys.verify(res.assignment)

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_anneal_solves_nonlinear_system" -q

Method implementation

    def residual_soft(self, x: Tensor) -> Tensor:
        """Sum of squared multilinear-extension violations at a soft point ``x``."""
        if x.shape[-1] != self.n:
            raise ValueError(f"x must have last dim {self.n}, got {x.shape}")
        total = x.new_zeros(())
        for c in self._constraint_tensors(x.dtype, x.device):
            phi = _multilinear_eval_point(c, x)
            total = total + phi * phi
        return total

View source ↗

verifymethod

verify(self, bits: Sequence[int]) -> bool

Exact check: every equation holds at the (hard) assignment bits.

Parameters

Name	Type & default	Contract
`bits`positional-or-keyword	`Sequence[int]`Required	See the operation contract and implementation below.

Returns: bool

Executed regression · gf2 fast path linear unique

Full file, imports & fixtures ↗

def test_gf2_fast_path_linear_unique() -> None:
    # x0 ^ x1 = 1 and x1 = 1  ->  x1 = 1, x0 = 0 (unique).
    sys = BooleanSystem.from_predicates(
        [lambda a, b: (a ^ b) == 1, lambda a, b: b == 1], n=2
    )
    assert sys.is_linear()
    res = solve(sys)
    assert res.method == "gf2"
    assert res.verified
    assert res.assignment == (0, 1)

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_gf2_fast_path_linear_unique" -q

Method implementation

    def verify(self, bits: Sequence[int]) -> bool:
        """Exact check: every equation holds at the (hard) assignment ``bits``."""
        return verify_assignment(self.constraints, bits)

View source ↗

is_linearmethod

is_linear(self) -> bool

True iff every equation is XOR-linear (GF(2) fast-path applies).

Returns: bool

Executed regression · inconsistent linear system

Full file, imports & fixtures ↗

def test_inconsistent_linear_system() -> None:
    sys = BooleanSystem.from_predicates(
        [lambda a: a == 0, lambda a: a == 1], n=1
    )
    res = solve(sys)
    assert res.method == "gf2"
    assert not res.verified
    assert res.assignment is None

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_inconsistent_linear_system" -q

Method implementation

    def is_linear(self) -> bool:
        """``True`` iff every equation is XOR-linear (GF(2) fast-path applies)."""
        return constraints_are_linear(self.constraints)

View source ↗

combinedmethod

combined(self) -> TruthTable

The single OR-combined constraint (1 where any equation is violated).

Returns: TruthTable

Method implementation

    def combined(self) -> TruthTable:
        """The single OR-combined constraint (``1`` where any equation is violated)."""
        return system_constraint(self.constraints)

View source ↗

Read the implementation

class BooleanSystem:
    """A system of Boolean equations ``phi_k(x) = 0`` (each ``phi_k`` a truth table)."""

    n: int
    constraints: tuple[TruthTable, ...]

    @classmethod
    def from_constraints(cls, constraints: Sequence[TruthTable]) -> BooleanSystem:
        """Build from constraint truth tables (``1`` = violated)."""
        if not constraints:
            raise ValueError("need at least one constraint")
        n = num_vars(constraints[0])
        for c in constraints:
            if num_vars(c) != n:
                raise ValueError("all constraints must share the same arity")
        return cls(n=n, constraints=tuple(tuple(c) for c in constraints))

    @classmethod
    def from_predicates(
        cls, predicates: Sequence[Callable[..., bool]], n: int
    ) -> BooleanSystem:
        """Build from predicates; ``phi_k`` is ``0`` exactly where ``pred_k`` holds."""
        constraints = [
            tuple(0 if pred(*bits) else 1 for bits in all_assignments(n))
            for pred in predicates
        ]
        return cls.from_constraints(constraints)

    def _constraint_tensors(self, dtype: torch.dtype, device: torch.device) -> list[Tensor]:
        return [
            torch.tensor(c, dtype=dtype, device=device) for c in self.constraints
        ]

    def residual_soft(self, x: Tensor) -> Tensor:
        """Sum of squared multilinear-extension violations at a soft point ``x``."""
        if x.shape[-1] != self.n:
            raise ValueError(f"x must have last dim {self.n}, got {x.shape}")
        total = x.new_zeros(())
        for c in self._constraint_tensors(x.dtype, x.device):
            phi = _multilinear_eval_point(c, x)
            total = total + phi * phi
        return total

    def verify(self, bits: Sequence[int]) -> bool:
        """Exact check: every equation holds at the (hard) assignment ``bits``."""
        return verify_assignment(self.constraints, bits)

    def is_linear(self) -> bool:
        """``True`` iff every equation is XOR-linear (GF(2) fast-path applies)."""
        return constraints_are_linear(self.constraints)

    def combined(self) -> TruthTable:
        """The single OR-combined constraint (``1`` where any equation is violated)."""
        return system_constraint(self.constraints)

Other public import paths

omnibias.boolean.torch.ops.BooleanSystem
omnibias.boolean.torch.ops.solver.BooleanSystem

CLASS

SolveResult

omnibias.boolean.torch.ops.SolveResultSource ↗

class SolveResult

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

Outcome of solve: a hardened assignment plus its exact verification.

Parameters

Name	Type & default	Contract
`assignment`dataclass field	`tuple[int, ...] \| None`Required	See the operation contract and implementation below.
`verified`dataclass field	`bool`Required	See the operation contract and implementation below.
`residual`dataclass field	`float`Required	See the operation contract and implementation below.
`method`dataclass field	`str`Required	See the operation contract and implementation below.
`relaxed`dataclass field	`tuple[float, ...] \| None`Default: None	See the operation contract and implementation below.

Fields & methods

assignmentfield

assignment: tuple[int, ...] | None

Declared tuple[int, ...] | None field on SolveResult. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

verifiedfield

verified: bool

Declared bool field on SolveResult. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

residualfield

residual: float

Declared float field on SolveResult. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

methodfield

method: str

Declared str field on SolveResult. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

relaxedfield

relaxed: tuple[float, ...] | None = None

Declared tuple[float, ...] | None field on SolveResult. Default expression: None.

View source ↗

Read the implementation

class SolveResult:
    """Outcome of :func:`solve`: a hardened assignment plus its exact verification."""

    assignment: tuple[int, ...] | None
    verified: bool
    residual: float
    method: str
    relaxed: tuple[float, ...] | None = None

Other public import paths

omnibias.boolean.torch.ops.SolveResult
omnibias.boolean.torch.ops.solver.SolveResult

FUNCTION

brute_force_solutions

omnibias.boolean.torch.ops.brute_force_solutionsSource ↗

brute_force_solutions(system: BooleanSystem) -> list[tuple[int, ...]]

All exact solutions (for tests / verification on small systems).

Parameters

Name	Type & default	Contract
`system`positional-or-keyword	`BooleanSystem`Required	See the operation contract and implementation below.

Returnslist[tuple[int, ...]]

Executed regression · gf2 enumerates full solution space

Full file, imports & fixtures ↗

def test_gf2_enumerates_full_solution_space() -> None:
    # Parity x0 ^ x1 ^ x2 = 0 has a 2-dimensional null space (4 even-parity points).
    sys = BooleanSystem.from_predicates([lambda a, b, c: (a ^ b ^ c) == 0], n=3)
    gsol = gf2_solve(sys.constraints)
    assert gsol is not None and gsol.consistent
    from omnibias.boolean._core.truth_table import index_of

    bf = sorted(index_of(b) for b in brute_force_solutions(sys))
    assert gsol.enumerate_solutions() == bf
    assert len(bf) == 4

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_gf2_enumerates_full_solution_space" -q

Read the implementation

def brute_force_solutions(system: BooleanSystem) -> list[tuple[int, ...]]:
    """All exact solutions (for tests / verification on small systems)."""
    out = []
    for idx in range(1 << system.n):
        bits = assignment(idx, system.n)
        if system.verify(bits):
            out.append(bits)
    return out

Other public import paths

omnibias.boolean.torch.ops.brute_force_solutions
omnibias.boolean.torch.ops.solver.brute_force_solutions

FUNCTION

solve

omnibias.boolean.torch.ops.solveSource ↗

solve(system: BooleanSystem, *, schedule: BetaAnnealScheduler | None=None, steps: int=300, lr: float=0.2, restarts: int=16, seed: int=0, use_gf2: bool=True, dtype: torch.dtype=torch.float64) -> SolveResult

Solve system (GF(2) fast-path when linear, else annealed soft search).

Parameters

Name	Type & default	Contract
`system`positional-or-keyword	`BooleanSystem`Required	See the operation contract and implementation below.
`schedule`keyword-only	`BetaAnnealScheduler \| None`Default: None	See the operation contract and implementation below.
`steps`keyword-only	`int`Default: 300	See the operation contract and implementation below.
`lr`keyword-only	`float`Default: 0.2	See the operation contract and implementation below.
`restarts`keyword-only	`int`Default: 16	See the operation contract and implementation below.
`seed`keyword-only	`int`Default: 0	See the operation contract and implementation below.
`use_gf2`keyword-only	`bool`Default: True	See the operation contract and implementation below.
`dtype`keyword-only	`torch.dtype`Default: torch.float64	See the operation contract and implementation below.

ReturnsSolveResult

Executed regression · inconsistent linear system

Full file, imports & fixtures ↗

def test_inconsistent_linear_system() -> None:
    sys = BooleanSystem.from_predicates(
        [lambda a: a == 0, lambda a: a == 1], n=1
    )
    res = solve(sys)
    assert res.method == "gf2"
    assert not res.verified
    assert res.assignment is None

python -m pytest "packages/omnibias-boolean/tests/test_solver.py::test_inconsistent_linear_system" -q

Regression example · gf2 fast path linear unique

This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.

Full file, imports & fixtures ↗

def test_gf2_fast_path_linear_unique() -> None:
    # x0 ^ x1 = 1 and x1 = 1  ->  x1 = 1, x0 = 0 (unique).
    sys = BooleanSystem.from_predicates(
        [lambda a, b: (a ^ b) == 1, lambda a, b: b == 1], n=2
    )
    assert sys.is_linear()
    res = solve(sys)
    assert res.method == "gf2"
    assert res.verified
    assert res.assignment == (0, 1)

python -m pytest packages/omnibias-boolean/tests/test_solver.py -k test_gf2_fast_path_linear_unique -q

Read the implementation

def solve(
    system: BooleanSystem,
    *,
    schedule: BetaAnnealScheduler | None = None,
    steps: int = 300,
    lr: float = 0.2,
    restarts: int = 16,
    seed: int = 0,
    use_gf2: bool = True,
    dtype: torch.dtype = torch.float64,
) -> SolveResult:
    """Solve ``system`` (GF(2) fast-path when linear, else annealed soft search)."""
    if use_gf2 and system.is_linear():
        gsol = gf2_solve(system.constraints)
        if gsol is not None:
            if not gsol.consistent:
                return SolveResult(None, False, float("inf"), "gf2")
            bits = gsol.particular
            return SolveResult(bits, system.verify(bits), 0.0, "gf2")

    if schedule is None:
        schedule = BetaAnnealScheduler(1.0, 20.0, steps, "exp")
    device = torch.device("cpu")
    gen = torch.Generator(device=device).manual_seed(seed)
    best: SolveResult | None = None
    for _ in range(restarts):
        theta = torch.randn(
            system.n, generator=gen, dtype=dtype, device=device, requires_grad=True
        )
        opt = torch.optim.Adam([theta], lr=lr)
        for t in range(steps):
            beta = schedule.value(t)
            x = torch.sigmoid(beta * theta)
            loss = system.residual_soft(x)
            opt.zero_grad()
            loss.backward()
            opt.step()
        with torch.no_grad():
            x = torch.sigmoid(schedule.value(steps) * theta)
            bits = tuple(int(v >= 0.5) for v in x)
            res = float(system.residual_soft(x))
        cand = SolveResult(
            bits, system.verify(bits), res, "anneal", tuple(float(v) for v in x)
        )
        if best is None or (cand.verified and not best.verified) or (
            cand.verified == best.verified and cand.residual < best.residual
        ):
            best = cand
        if best.verified:
            break
    assert best is not None
    return best

Other public import paths

omnibias.boolean.torch.ops.solve
omnibias.boolean.torch.ops.solver.solve

← Package overview Runnable learning examples →

omnibias.boolean.torch.ops.solver

Imports & aliases​

BooleanSystem​

Parameters

Fields & methods

Parameters

Parameters

Parameters

Parameters

SolveResult​

Parameters

Fields & methods

brute_force_solutions​

Parameters

solve​

Parameters

Imports & aliases

BooleanSystem

SolveResult

brute_force_solutions

solve