PolyHorn Engine¶

The PolyHorn engine is a specialized verification component within EFMC that handles polynomial constraint systems using advanced mathematical theorems. It provides a powerful framework for solving satisfiability problems involving polynomial inequalities and universally quantified formulas.

Overview¶

PolyHorn implements three fundamental mathematical theorems for polynomial constraint solving:

Farkas’ Lemma: For linear polynomial constraints
Handelman’s Theorem: For polynomial constraints with linear left-hand sides
Putinar’s Theorem: For general polynomial constraints using sum-of-squares decomposition

The engine automatically selects the most appropriate theorem based on the structure of the input constraints, or allows manual selection through configuration.

Theoretical Background¶

Farkas’ Lemma¶

Farkas’ Lemma provides a fundamental result in linear programming theory. For a system of linear inequalities \(Ax \geq 0\), the lemma states that either the system has a solution, or there exists a vector \(y \geq 0\) such that \(A^T y = 0\) and \(y \neq 0\).

In the context of PolyHorn, Farkas’ Lemma is used to handle constraint systems of the form:

\[\forall x. (f_1(x) \geq 0 \land \ldots \land f_n(x) \geq 0) \Rightarrow g(x) \geq 0\]

where all \(f_i\) and \(g\) are linear polynomials.

Handelman’s Theorem¶

Handelman’s Theorem extends Farkas’ Lemma to handle polynomial constraints where the left-hand side consists of linear constraints but the right-hand side can be polynomial. It states that if a polynomial is positive on a basic closed semialgebraic set defined by linear inequalities, then it can be represented as a positive combination of products of the defining linear forms.

Putinar’s Theorem¶

Putinar’s Theorem provides the most general framework using sum-of-squares (SOS) decomposition. It handles arbitrary polynomial constraint systems by representing positive polynomials as sums of squares plus combinations of constraint polynomials multiplied by sums of squares.

For a constraint system defined by polynomial inequalities \(g_1(x) \geq 0, \ldots, g_m(x) \geq 0\), if a polynomial \(f(x)\) is positive on the feasible region, then:

\[f(x) = \sigma_0(x) + \sum_{i=1}^m \sigma_i(x) \cdot g_i(x)\]

where each \(\sigma_i(x)\) is a sum of squares.

Usage¶

Basic API Usage¶

The PolyHorn engine can be used through its main API function:

from efmc.engines.polyhorn.main import execute
from pysmt.shortcuts import *
from pysmt.typing import REAL

# Create symbols
x = Symbol("x", REAL)
y = Symbol("y", REAL)

# Create a solver and add constraints
solver = Solver(name="z3")
solver.add_assertion(x >= Real(0))
solver.add_assertion(y >= Real(0))
solver.add_assertion(ForAll([x, y],
                           Implies(And(x >= Real(1), y >= Real(1)),
                                  x + y >= Real(2))))

# Configure the engine
config = {
    "theorem_name": "auto",  # or "farkas", "handelman", "putinar"
    "solver_name": "z3",
    "degree_of_sat": 2,
    "degree_of_nonstrict_unsat": 2
}

# Execute
result, model = execute(solver, config)
print(f"Result: {result}")
print(f"Model: {model}")

Configuration Options¶

The PolyHorn engine supports various configuration parameters:

Core Settings:

theorem_name: Choice of theorem (“farkas”, “handelman”, “putinar”, or “auto”)
solver_name: Backend SMT solver (“z3”, “cvc4”, etc.)
integer_arithmetic: Whether to use integer arithmetic (default: False)

Degree Control:

degree_of_sat: Maximum degree for satisfiability constraints
degree_of_nonstrict_unsat: Maximum degree for non-strict unsatisfiability constraints
degree_of_strict_unsat: Maximum degree for strict unsatisfiability constraints
max_d_of_strict: Degree of variables generated for strict cases in Putinar’s theorem

Heuristics:

SAT_heuristic: Enable satisfiability-based heuristics
unsat_core_heuristic: Enable unsatisfiable core-based optimization

Input Formats¶

PolyHorn accepts input in two main formats:

SMT2 Format:

(declare-const x Real)
(declare-const y Real)
(assert (forall ((l Real))
        (=> (and (= x l) (>= x 1) (<= x 3))
            (and (<= x 10) (= l 2) (> x 0)))))
(check-sat)
(get-model)

PySMT Solver Objects:

The engine can directly work with PySMT solver objects, automatically converting them to the internal representation.

Implementation Details¶

Core Components¶

Parser (Parser.py)

Handles parsing of both SMT2 format and a custom readable format. Supports complex polynomial expressions and constraint systems.

PositiveModel (PositiveModel.py)

The main orchestrator class that manages constraint generation, theorem selection, and solver interaction.

Theorem Implementations:

Farkas.py: Implements Farkas’ Lemma for linear constraints
Handelman.py: Implements Handelman’s Theorem with monomial generation
Putinar.py: Implements Putinar’s Theorem with sum-of-squares decomposition

Polynomial Representation:

Polynomial.py: Core polynomial data structure
Coefficient.py: Handles polynomial coefficients with unknown variables
Constraint.py: Represents polynomial constraints and inequalities

Solver Integration (Solver.py)

Provides utilities for constraint generation, SMT format conversion, and variable management.

Automatic Theorem Selection¶

When theorem_name is set to “auto”, PolyHorn automatically selects the most appropriate theorem:

Farkas’ Lemma: If both left-hand side and right-hand side constraints are linear
Handelman’s Theorem: If left-hand side is linear but right-hand side is polynomial
Putinar’s Theorem: For general polynomial constraint systems

This selection optimizes both performance and completeness based on the constraint structure.

Advanced Features¶

Sum-of-Squares Optimization¶

For Putinar’s theorem, PolyHorn generates sum-of-squares templates using semidefinite programming techniques. The implementation creates lower triangular matrices and computes their products to ensure positive semidefiniteness.

Degree Management¶

The engine provides fine-grained control over polynomial degrees in different contexts:

Satisfiability constraints can use different degree bounds than unsatisfiability constraints
Strict and non-strict inequalities are handled with separate degree parameters
Automatic degree escalation for improved completeness

Core Iteration Heuristic¶

PolyHorn implements an unsatisfiable core-based optimization that iteratively removes unnecessary constraints to simplify the solving process while maintaining correctness.

Examples¶

Linear Constraint System¶

# System: x >= 0, y >= 0 ⊢ x + y >= 0
solver = Solver(name="z3")
solver.add_assertion(ForAll([x, y],
                           Implies(And(x >= Real(0), y >= Real(0)),
                                  x + y >= Real(0))))

config = {"theorem_name": "farkas", "solver_name": "z3"}
result, model = execute(solver, config)

Polynomial Constraint System¶

# System with quadratic constraints
solver = Solver(name="z3")
solver.add_assertion(ForAll([x, y],
                           Implies(And(x*x + y*y <= Real(1)),
                                  x*x <= Real(1))))

config = {
    "theorem_name": "putinar",
    "solver_name": "z3",
    "degree_of_sat": 4
}
result, model = execute(solver, config)

Performance Considerations¶

Degree Selection: Higher degrees provide more completeness but significantly increase computational cost. Start with low degrees (0-2) and increase as needed.

Theorem Choice: Farkas’ Lemma is fastest for linear systems, while Putinar’s theorem is most general but computationally expensive.

Solver Backend: Z3 generally provides the best performance for the generated constraint systems.

Memory Usage: Sum-of-squares decomposition can generate large constraint systems. Monitor memory usage for high-degree problems.

Limitations¶

Decidability: While theoretically complete for real arithmetic, practical decidability depends on degree bounds
Integer Arithmetic: Limited support for integer constraints compared to real arithmetic
Scalability: Performance degrades significantly with increasing polynomial degrees and variable counts
Numerical Stability: High-degree polynomials may suffer from numerical precision issues

Integration with EFMC¶

PolyHorn integrates seamlessly with the broader EFMC verification framework:

CHC Support: Handles Constrained Horn Clauses with polynomial constraints
Template Integration: Works with EFMC’s template-based verification engines
Multi-Engine Workflows: Can be combined with other EFMC engines for hybrid verification approaches

The engine is particularly effective for verification problems involving:

Polynomial loop invariants
Nonlinear arithmetic properties
Optimization and control system verification
Hybrid system analysis

References¶

Farkas, J. (1902). Theorie der einfachen Ungleichungen
Handelman, D. (1988). Representing polynomials by positive linear functions on compact convex polyhedra
Putinar, M. (1993). Positive polynomials on compact semi-algebraic sets
Parrilo, P. A. (2003). Semidefinite programming relaxations for semialgebraic problems
Lasserre, J. B. (2001). Global optimization with polynomials and the problem of moments