Previous  Up  Next

Module Sos.Q

module Q: S  with module Poly = Polynomial.Q

Polynomial expressions.

module Poly: Polynomial.S 
type var

Parametric variables.

type polynomial_expr =
| Const of Poly.t
| Var of var
| Mult_scalar of Poly.Coeff.t * polynomial_expr
| Add of polynomial_expr * polynomial_expr
| Sub of polynomial_expr * polynomial_expr
| Mult of polynomial_expr * polynomial_expr
| Power of polynomial_expr * int
| Compose of polynomial_expr * polynomial_expr list
| Derive of polynomial_expr * int

Constructors. See the module Polynomial.S for details.

val make : ?n:int -> ?d:int -> ?homogen:bool -> string -> polynomial_expr

make s creates a new parametric variable named s. For instance, make "lambda" creates a new scalar parametric variable and make ~n:1 ~d:2 "p" creates a new polynomial parametric variable (p_0 + p_1 x0 + p_2 x0^2 with p_0, p_1 and p_2 scalar parametric variables).

n : number of variables (default: 1), must be positive
d : degree (default: 1), must be positive
homogen : creates an homogeneous polynomial (default: false), i.e., all monomials of same degree (for instance x_0 x_1^3 + x_0^4 is homogeneous, x_0 x_1^3 + x_0^3 is not)

Functions for above constructors.

val const : Poly.t -> polynomial_expr
val scalar : Poly.Coeff.t -> polynomial_expr
val monomial : Monomial.t -> polynomial_expr
val mult_scalar : Poly.Coeff.t -> polynomial_expr -> polynomial_expr
val add : polynomial_expr -> polynomial_expr -> polynomial_expr
val sub : polynomial_expr -> polynomial_expr -> polynomial_expr
val mult : polynomial_expr -> polynomial_expr -> polynomial_expr
val power : polynomial_expr -> int -> polynomial_expr
val compose : polynomial_expr -> polynomial_expr list -> polynomial_expr
val derive : polynomial_expr -> int -> polynomial_expr

Conversion functions.

val of_list : (Monomial.t * polynomial_expr) list -> polynomial_expr
exception Dimension_error
val to_list : polynomial_expr -> (Monomial.t * polynomial_expr) list

Returns a list sorted in increasing order of Monomial.compare without duplicates. All polynomial_expr in the returned list are scalars (i.e., functions nb_vars and degree below both return 0).

Various functions.

See the module Polynomial.S for details. Beware that the returned values correspond to the polynomial_expression and can be larger than the result after solving. For instance, considering the expression v x_1^3 + x_0^2 with v a variable, nb_vars and degree will respectively return 2 and 3. Although, when asking the expression to be SOS, v will be 0 and then nb_vars and degree will become respectively 1 and 2 in the result.

val nb_vars : polynomial_expr -> int
val degree : polynomial_expr -> int
val is_homogeneous : polynomial_expr -> bool
val param_vars : polynomial_expr -> var list

param_vars e returns the list of all parametric variables appearing in e.

Prefix and infix operators.

To use this operators, it's convenient to use local opens. For instance to write the polynomial 2.3 x0^3 x2^2 + x1 + 0.5:

let module Sos = Osdp.Sos.Float in
Sos.(2.3 *. ??0**3 * ??2**2 + ??1 + !0.5)

See the module Polynomial.S for details.

val (!!) : Poly.t -> polynomial_expr

Const

val ?? : int -> polynomial_expr
val (!) : Poly.Coeff.t -> polynomial_expr

scalar

val ( *. ) : Poly.Coeff.t -> polynomial_expr -> polynomial_expr
val (~-) : polynomial_expr -> polynomial_expr
val (+) : polynomial_expr -> polynomial_expr -> polynomial_expr
val (-) : polynomial_expr -> polynomial_expr -> polynomial_expr
val ( * ) : polynomial_expr -> polynomial_expr -> polynomial_expr
val (/) : polynomial_expr -> Poly.Coeff.t -> polynomial_expr
val (/.) : Poly.Coeff.t -> Poly.Coeff.t -> polynomial_expr
val ( ** ) : polynomial_expr -> int -> polynomial_expr
val (>=) : polynomial_expr -> polynomial_expr -> polynomial_expr

e1 >= e2 is just syntactic sugar for e1 - e2.

val (<=) : polynomial_expr -> polynomial_expr -> polynomial_expr

e1 <= e2 is just syntactic sugar for e2 - e1.

Printing.

val pp : Stdlib.Format.formatter -> polynomial_expr -> unit

Printer for polynomial expressions.

val pp_names : string list -> Stdlib.Format.formatter -> polynomial_expr -> unit

See Monomial.pp_names for details about names.

SOS.

type options = {
   sdp : Sdp.options; (*

default: Sdp.default

*)
   verbose : int; (*

verbosity level, non negative integer, 0 (default) means no output (but see sdp.verbose just above)

*)
   scale : bool; (*

scale (default: true)

*)
   trace_obj : bool; (*

When no objective is set (Purefeas below), minimize the trace of the SOS constraints instead of no objective (default: false).

*)
   dualize : bool; (*

solve using the dual representation, can be slower but more robust (default: false)

*)
   monoms : Monomial.t list list; (*

monomials (default: []) for each constraint (automatically determined when list shorter than constraints list)

*)
   pad : float; (*

padding factor (default: 2.), 0. means no padding

*)
   pad_list : float list; (*

padding factors (dafault: []) for each constraint (pad used when list shorter than constraints list)

*)
} 
val default : options

Default values above.

type obj =
| Minimize of polynomial_expr
| Maximize of polynomial_expr
| Purefeas

Minimize e or Maximize e or Purefeas (just checking feasibility). e must be an affine combination of scalar variables (obtained from var).

type values 
type 'a witness = Monomial.t array * 'a array array 
exception Not_linear
val solve : ?options:options ->
       ?solver:Sdp.solver ->
       obj ->
       polynomial_expr list ->
       SdpRet.t * (float * float) * values * float witness list

solve obj l tries to optimise the objective obj under the constraint that each polynomial expressions in l is SOS. If solver is provided, it will supersed the solver given in options. Returns a tuple ret, (pobj, dobj), values, witnesses. If SdpRet.is_success ret, then the following holds. pobj (resp. dobj) is the achieved primal (resp. dual) objective value. values contains values for each variable appearing in l (to be retrieved through following functions value and value_poly). witnesses is a list with the same length than l containing pairs v, Q such that Q is a square matrix and v a vector of monomials of the same size and the polynomial v^T Q v should be close from the corresponding polynomial in l.

If ret is SdpRet.Success, then all SOS constraints in l are indeed satisfied by the values returned in values (this is checked through the function check below with witnesses).

val value : polynomial_expr -> values -> Poly.Coeff.t

value e values returns the evaluation of polynomial expression e, replacing all Var by the correspoding value in values.

val value_poly : polynomial_expr -> values -> Poly.t

value_poly e values returns the evaluation of polynomial expression e, replacing all Var by the correspoding value in values.

val check : ?options:options ->
       ?values:values -> polynomial_expr -> float witness -> bool

If check ?options e ?values (v, Q) returns true, then e is SOS. Otherwise, either e is not SOS or the difference between e and v^T Q v is too large or Q is not positive definite enough for the proof to succeed. The witness (v, Q) is typically obtained from the above function solve. If e contains variables, they are replaced by the corresponding value in values (values is empty by default).

Here is how it works. e is expected to be the polynomial v^T Q v modulo numerical errors. To prove that e is SOS despite these numerical errors, we first check that the polynomial e can be expressed as v^T Q' v for some Q' (i.e. that the monomial base v contains enough monomials). Then e can be expressed as v^T (Q + R) v where R is a matrix with all coefficients bounded by the maximum difference between the coefficients of the polynomials e and v^T Q v. If all such matrices Q + R are positive definite, then e is SOS.

val check_round : ?options:options ->
       ?values:values ->
       polynomial_expr list ->
       float witness list ->
       (values * Scalar.Q.t witness list) option

TODO: doc (