omnibias.sos.solve

0.1.0a2AlphaPython >=3.10AGPL / commercial

Sum-of-squares constructions, polynomial positivity checks, and rigorous validation of proposed Gram matrices.

import omnibias.sos.solve

Module contract & mathematical conventions

A compact float SDP *proposer* for Sum-of-Squares Gram matrices.

**This module never proves anything.** It proposes a floating-point, strictly-positive-definite Gram matrix Q with z(x)^T Q z(x) approx p(x). The proof happens later in omnibias.sos.certify, which rationally rounds Q and runs a rigorous interval LDL^T positive-definiteness check. This mirrors the repo's neumann_inverse_norm_bound pattern: a float solver proposes, a verified routine certifies -- so the SDP can be floating-point and even swapped for an external backend without touching soundness.

The core is a primal log-det interior-point method in the symmetric-vectorisation (svec) space, parametrised over the affine "coefficient-matching" subspace so that every iterate satisfies z^T Q z = p exactly (up to float round-off). For pure SOS feasibility it computes the analytic centre (the maximum-determinant Gram, which rounds well); a general free-variable + linear-objective form (used by the auxiliary-functional method) follows a short barrier path.

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 →

CONSTANT

GramProposer

omnibias.sos.solve.GramProposerSource ↗

GramProposer = Callable[[np.ndarray, np.ndarray, int], 'np.ndarray | None']

This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.

Read the implementation

GramProposer = Callable[[np.ndarray, np.ndarray, int], "np.ndarray | None"]

CLASS

SDPResult

omnibias.sos.solve.SDPResultSource ↗

class SDPResult

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 the float SDP proposer (advisory only, never a proof).

Parameters

Name	Type & default	Contract
`status`dataclass field	`str`Required	See the operation contract and implementation below.
`gram`dataclass field	`np.ndarray \| None`Required	See the operation contract and implementation below.
`free_vars`dataclass field	`np.ndarray \| None`Required	See the operation contract and implementation below.
`min_eig`dataclass field	`float`Required	See the operation contract and implementation below.
`detail`dataclass field	`str`Required	See the operation contract and implementation below.

Fields & methods

statusfield

status: str

"solved" (a PD proposal found), "infeasible", or "failed".

View source ↗

gramfield

gram: np.ndarray | None

The proposed symmetric Gram matrix Q (float), or None.

View source ↗

free_varsfield

free_vars: np.ndarray | None

Optimised free variables y (auxiliary form), or None.

View source ↗

min_eigfield

min_eig: float

Smallest eigenvalue of the proposed Q (a float health check).

View source ↗

detailfield

detail: str

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

View source ↗

Read the implementation

class SDPResult:
    """Outcome of the float SDP proposer (advisory only, never a proof)."""

    status: str
    """``"solved"`` (a PD proposal found), ``"infeasible"``, or ``"failed"``."""
    gram: np.ndarray | None
    """The proposed symmetric Gram matrix ``Q`` (float), or ``None``."""
    free_vars: np.ndarray | None
    """Optimised free variables ``y`` (auxiliary form), or ``None``."""
    min_eig: float
    """Smallest eigenvalue of the proposed ``Q`` (a float health check)."""
    detail: str

FUNCTION

solve_gram_program

omnibias.sos.solve.solve_gram_programSource ↗

solve_gram_program(m: int, lhs: np.ndarray, rhs: np.ndarray, objective: np.ndarray, *, max_newton: int=40, barrier_steps: int=6, feas_tol: float=1e-08, pd_target: float=0.0001, reg: np.ndarray | None=None) -> SDPResult

General SOS program: minimise objective . (svec(Q), y) with Q >= 0.

Used by the auxiliary-functional method, where the free variables y are an auxiliary functional's coefficients and a bound C. The optional per-coordinate ridge reg keeps chosen free variables well-scaled (a numeric tie-breaker only; soundness rests entirely on the downstream verified certificate). Advisory float proposal only; the certified bound comes from certifying the resulting SOS polynomial.

Parameters

Name	Type & default	Contract
`m`positional-or-keyword	`int`Required	See the operation contract and implementation below.
`lhs`positional-or-keyword	`np.ndarray`Required	See the operation contract and implementation below.
`rhs`positional-or-keyword	`np.ndarray`Required	See the operation contract and implementation below.
`objective`positional-or-keyword	`np.ndarray`Required	See the operation contract and implementation below.
`max_newton`keyword-only	`int`Default: 40	See the operation contract and implementation below.
`barrier_steps`keyword-only	`int`Default: 6	See the operation contract and implementation below.
`feas_tol`keyword-only	`float`Default: 1e-08	See the operation contract and implementation below.
`pd_target`keyword-only	`float`Default: 0.0001	See the operation contract and implementation below.
`reg`keyword-only	`np.ndarray \| None`Default: None	See the operation contract and implementation below.

ReturnsSDPResult

Executed regression · false statement is inconclusive

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_false_statement_is_inconclusive() -> None:
    # x - 5 <= -4 on [-1, 1]; must never be "proved".
    cert = certify_nonneg_on_set(X1 - 5.0 * ONE1, [ONE1 - X1 * X1])
    assert cert.status == "inconclusive"
    assert not cert.certified

python -m pytest "packages/omnibias-sos/tests/test_positivstellensatz.py::test_false_statement_is_inconclusive" -q

Read the implementation

def solve_gram_program(
    m: int,
    lhs: np.ndarray,
    rhs: np.ndarray,
    objective: np.ndarray,
    *,
    max_newton: int = 40,
    barrier_steps: int = 6,
    feas_tol: float = 1e-8,
    pd_target: float = 1e-4,
    reg: np.ndarray | None = None,
) -> SDPResult:
    r"""General SOS program: minimise ``objective . (svec(Q), y)`` with ``Q >= 0``.

    Used by the auxiliary-functional method, where the free variables ``y`` are an
    auxiliary functional's coefficients and a bound ``C``.  The optional per-coordinate
    ridge ``reg`` keeps chosen free variables well-scaled (a numeric tie-breaker only;
    soundness rests entirely on the downstream verified certificate).  Advisory float
    proposal only; the certified bound comes from certifying the resulting SOS
    polynomial.
    """
    result = _interior_point(
        lhs, rhs, objective, m,
        max_newton=max_newton, barrier_steps=barrier_steps, feas_tol=feas_tol,
        pd_target=pd_target, reg=reg,
    )
    if result is None:
        return SDPResult("infeasible", None, None, float("nan"), "no PD feasible point found")
    matrix, y = result
    eig = float(np.linalg.eigvalsh(matrix).min())
    return SDPResult("solved", matrix, y, eig, f"barrier-path solution (min eig {eig:.3e})")

FUNCTION

solve_sos_gram

omnibias.sos.solve.solve_sos_gramSource ↗

solve_sos_gram(polynomial: Polynomial, basis: Sequence[Exponent], *, max_newton: int=60, feas_tol: float=1e-08, pd_target: float=0.0001, external: GramProposer | None=None) -> SDPResult

Propose a PD Gram matrix Q with z(x)^T Q z(x) approx polynomial.

Parameters

polynomial, basis: The polynomial and the monomial basis z(x) (exponent tuples). external: Optional external backend (A, t, m) -> Q (e.g. a wrapper around a dedicated SDP solver). Advisory only -- the proposal is still rationally rounded and rigorously certified downstream.

Returns

SDPResult status == "solved" carries a floating-point PD proposal. This is **not** a proof of nonnegativity; certification happens in omnibias.sos.certify.certify_sos.

Parameters

Name	Type & default	Contract
`polynomial`positional-or-keyword	`Polynomial`Required	The polynomial and the monomial basis `z(x)` (exponent tuples).
`basis`positional-or-keyword	`Sequence[Exponent]`Required	See the operation contract and implementation below.
`max_newton`keyword-only	`int`Default: 60	See the operation contract and implementation below.
`feas_tol`keyword-only	`float`Default: 1e-08	See the operation contract and implementation below.
`pd_target`keyword-only	`float`Default: 0.0001	See the operation contract and implementation below.
`external`keyword-only	`GramProposer \| None`Default: None	Optional external backend `(A, t, m) -> Q` (e.g. a wrapper around a dedicated SDP solver). Advisory only -- the proposal is still rationally rounded and rigorously certified downstream.

ReturnsSDPResult

Executed regression · is sos helper agrees

Full file, imports & fixtures ↗

def test_is_sos_helper_agrees() -> None:
    assert is_sos(X * X - X * Y + Y * Y + ONE)
    assert not is_sos(Polynomial(2, {(4, 2): 1.0, (2, 4): 1.0, (2, 2): -3.0, (0, 0): 1.0}))

python -m pytest "packages/omnibias-sos/tests/test_certify.py::test_is_sos_helper_agrees" -q

Read the implementation

def solve_sos_gram(
    polynomial: Polynomial,
    basis: Sequence[Exponent],
    *,
    max_newton: int = 60,
    feas_tol: float = 1e-8,
    pd_target: float = 1e-4,
    external: GramProposer | None = None,
) -> SDPResult:
    r"""Propose a PD Gram matrix ``Q`` with ``z(x)^T Q z(x) approx polynomial``.

    Parameters
    ----------
    polynomial, basis:
        The polynomial and the monomial basis ``z(x)`` (exponent tuples).
    external:
        Optional external backend ``(A, t, m) -> Q`` (e.g. a wrapper around a
        dedicated SDP solver).  Advisory only -- the proposal is still rationally
        rounded and rigorously certified downstream.

    Returns
    -------
    SDPResult
        ``status == "solved"`` carries a floating-point PD proposal.  This is
        **not** a proof of nonnegativity; certification happens in
        :func:`omnibias.sos.certify.certify_sos`.
    """
    system = sos_constraint_system(polynomial, basis)
    if system is None:
        return SDPResult(
            "infeasible", None, None, float("nan"),
            "polynomial has a monomial no basis product can build",
        )
    rows, targets = system
    m = len(basis)

    if external is not None:
        proposal = external(rows, targets, m)
        if proposal is None:
            return SDPResult("failed", None, None, float("nan"), "external solver returned no Gram")
        matrix = np.asarray(proposal, dtype=float)
        eig = float(np.linalg.eigvalsh(matrix).min())
        status = "solved" if eig > 0.0 else "failed"
        return SDPResult(status, matrix, None, eig, f"external solver (min eig {eig:.3e})")

    result = _interior_point(
        rows, targets, np.zeros(rows.shape[1]), m,
        max_newton=max_newton, barrier_steps=1, feas_tol=feas_tol, pd_target=pd_target,
    )
    if result is None:
        return SDPResult(
            "infeasible", None, None, float("nan"),
            "no positive-definite Gram matrix matches the coefficients (not SOS in this basis)",
        )
    matrix, _y = result
    eig = float(np.linalg.eigvalsh(matrix).min())
    return SDPResult("solved", matrix, None, eig, f"analytic-centre Gram (min eig {eig:.3e})")

FUNCTION

sos_constraint_system

omnibias.sos.solve.sos_constraint_systemSource ↗

sos_constraint_system(polynomial: Polynomial, basis: Sequence[Exponent]) -> tuple[np.ndarray, np.ndarray] | None

Build the coefficient-matching rows A and targets t.

Returns (A, t) with A[k] . svec(Q) == t[k] encoding "the coefficient of product monomial alpha_k in z^T Q z equals p_{alpha_k}", or None if the polynomial has a monomial no basis product can build (so it cannot be SOS in this basis).

Parameters

Name	Type & default	Contract
`polynomial`positional-or-keyword	`Polynomial`Required	See the operation contract and implementation below.
`basis`positional-or-keyword	`Sequence[Exponent]`Required	See the operation contract and implementation below.

Returnstuple[np.ndarray, np.ndarray] | None

Executed regression · is sos helper agrees

Full file, imports & fixtures ↗

def test_is_sos_helper_agrees() -> None:
    assert is_sos(X * X - X * Y + Y * Y + ONE)
    assert not is_sos(Polynomial(2, {(4, 2): 1.0, (2, 4): 1.0, (2, 2): -3.0, (0, 0): 1.0}))

python -m pytest "packages/omnibias-sos/tests/test_certify.py::test_is_sos_helper_agrees" -q

Read the implementation

def sos_constraint_system(
    polynomial: Polynomial, basis: Sequence[Exponent]
) -> tuple[np.ndarray, np.ndarray] | None:
    r"""Build the coefficient-matching rows ``A`` and targets ``t``.

    Returns ``(A, t)`` with ``A[k] . svec(Q) == t[k]`` encoding "the coefficient of
    product monomial ``alpha_k`` in ``z^T Q z`` equals ``p_{alpha_k}``", or ``None``
    if the polynomial has a monomial no basis product can build (so it cannot be
    SOS in this basis).
    """
    m = len(basis)
    idx = _svec_indices(m)
    products = gram_products(basis)
    if not polynomial.support <= set(products):
        return None
    alphas = sorted(products)
    rows = np.zeros((len(alphas), _svec_dim(m)))
    targets = np.zeros(len(alphas))
    for row, alpha in enumerate(alphas):
        for i, j, _mult in products[alpha]:
            rows[row, idx[(i, j)]] = 1.0 if i == j else _SQRT2
        targets[row] = polynomial.coefficient(alpha)
    return rows, targets

← Package overview Runnable learning examples →

omnibias.sos.solve

GramProposer​

SDPResult​

Parameters

Fields & methods

solve_gram_program​

Parameters

solve_sos_gram​

Parameters

sos_constraint_system​

Parameters

GramProposer

SDPResult

solve_gram_program

solve_sos_gram

sos_constraint_system