Certification
We provide support for certifying non-singular solutions to polynomial systems. The details of the implementation described in the article
Breiding, P., Rose, K. and Timme, S. "Certifying zeros of polynomial systems using interval arithmetic." arXiv:2011.05000
Certify
HomotopyContinuation.certify — Functioncertify(F, solutions, [p, certify_cache]; options...)
certify(F, result, [p, certify_cache]; options...)Attempt to certify that the given approximate solutions correspond to true solutions of the polynomial system $F(x;p)$. The system $F$ has to be an (affine) square polynomial system. Also attemps to certify for each solutions whether it approximates a real solution. The certification is done using interval arithmetic and the Krawczyk method[Moo77]. Returns a CertificationResult which additionall returns the number of distinct solutions. For more details of the implementation see [BRT20].
Options
show_progress = true: Iftrueshows a progress bar of the certification process.max_precision = 256: The maximal accuracy (in bits) that is used in the certification process.compile = false: See thesolvedocumentation.
Example
We take the first example from our introduction guide.
@var x y
# define the polynomials
f₁ = (x^4 + y^4 - 1) * (x^2 + y^2 - 2) + x^5 * y
f₂ = x^2+2x*y^2 - 2y^2 - 1/2
F = System([f₁, f₂], variables = [x,y])
result = solve(F)Result with 18 solutions
========================
• 18 paths tracked
• 18 non-singular solutions (4 real)
• random seed: 0xcaa483cd
• start_system: :polyhedralWe see that we obtain 18 solutions and it seems that 4 solutions are real. However, this is based on heuristics. To be absolute certain we can certify the result
certify(F, result)CertificationResult
===================
• 18 solution candidates given
• 18 certified solution intervals (4 real, 14 complex)
• 18 distinct certified solution intervals (4 real, 14 complex)and see that there are indeed 18 solutions and that they are all distinct.
CertificationResult
The result of certify is a CertificationResult:
HomotopyContinuation.CertificationResult — TypeCertificationResultThe result of certify for multiple solutions. Contains a vector of SolutionCertificate as well as a list of certificates which correspond to the same true solution.
IteratorCertificationResult
Certifying a ResultIterator produces a IteratorCertificationResult:
HomotopyContinuation.IteratorCertificationResult — TypeIteratorCertificationResultFinal summary returned by the BSP-based certify method forResultIterator.
HomotopyContinuation.bsp — Functionbsp(R::IteratorCertificationResult)Return the BSP partition used during iterator certification.
SolutionCertificate
A CertificationResult contains in particular all SolutionCertificates:
HomotopyContinuation.SolutionCertificate — TypeSolutionCertificateResult of certify for a single solution. Contains the initial solutions and if the certification was successful a vector of complex intervals where the true solution is contained in. The complex intervals are given as an Arblib.AcbMatrix. The Arblib.AcbMatrix is printed in the default format of Arblib. This means that, if the midpoint of an interval can't be represented with sufficiently many correct digits, Arblib will not print the midpoint. Instead, it will print an interval of the form [+/- r], where r will be an upper bound for the absolute value of the ball. An enclosure of the correct interval can be printed as follows.
Base.show(certificate::SolutionCertificate; digits = 16, more = true)This uses the ARB_STR_MORE functionality in Flint with 16 digits.
HomotopyContinuation.certificates — Functioncertificates(R::CertificationResult)Obtain the stored SolutionCertificates.
certificates(d::DistinctCertifiedSolutions)Return a vector of solution certificates in the DistinctSolutionCertificates object.
HomotopyContinuation.distinct_certificates — Functiondistinct_certificates(R::CertificationResult)Obtain the certificates corresponding to the determined distinct solution intervals.
HomotopyContinuation.is_certified — Functionis_certified(certificate::AbstractSolutionCertificate)Returns true if certificate is a certificate that certified_solution_interval(certificate) contains a unique zero.
HomotopyContinuation.is_real — Methodis_real(certificate::AbstractSolutionCertificate)Returns true if certificate certifies that the certified solution interval contains a true real zero of the system. If false is returned then this does not necessarily mean that the true solution is not real.
HomotopyContinuation.is_complex — Methodis_complex(certificate::AbstractSolutionCertificate)Returns true if certificate certifies that the certified solution interval contains a non-real complex zero of the system.
HomotopyContinuation.is_positive — Methodis_positive(certificate::AbstractSolutionCertificate)Returns true if is_certified(certificate) is true and the unique zero contained in certified_solution_interval(certificate) is real and positive.
HomotopyContinuation.solution_candidate — Functionsolution_candidate(certificate::AbstractSolutionCertificate)Returns the given provided solution candidate.
HomotopyContinuation.certified_solution_interval — Functioncertified_solution_interval(certificate::AbstractSolutionCertificate)Returns an Arblib.AcbMatrix representing a vector of complex intervals where a unique zero of the system is contained in. Returns nothing if is_certified(certificate) is false.
HomotopyContinuation.certified_solution_interval_after_krawczyk — Functioncertified_solution_interval_after_krawczyk(certificate::ExtendedSolutionCertificate)Returns an Arblib.AcbMatrix representing a vector of complex intervals where a unique zero of the system is contained in. This is the result of applying the Krawczyk operator to certified_solution_interval(certificate). Returns nothing if is_certified(certificate) is false.
HomotopyContinuation.certificate_index — Functioncertificate_index(certificate::AbstractSolutionCertificate)Return the index of the solution certificate. Here the index refers to the index of the provided solution candidates.
HomotopyContinuation.solution_approximation — Functionsolution_approximation(certificate::AbstractSolutionCertificate)If is_certified(certificate) is true this returns the midpoint of the certified_solution_interval of the given certificate as a Vector{ComplexF64}. Returns nothing if is_certified(certificate) is false.
Incremental Certified Sets
For iteratively building a certified set of distinct solutions, use DistinctCertifiedSolutions and add_solution!. This API can be updated batch-by-batch and merged in memory with merge!.
HomotopyContinuation.DistinctCertifiedSolutions — TypeDistinctCertifiedSolutions(F::System, params; thread_safe::Bool = false)Create a DistinctCertifiedSolutions object from a system and certification parameters. If thread_safe is true, the object will be thread-safe.
DistinctCertifiedSolutions(F::AbstractSystem, params; thread_safe::Bool = false)Create a DistinctCertifiedSolutions object from an abstract system and certification parameters.
HomotopyContinuation.add_solution! — Functionadd_solution!(d::DistinctCertifiedSolutions, sol::Vector{ComplexF64}, i::Integer = 0; certify_solution_kwargs...)Add a solution to the DistinctSolutionCertificates object if it is not a duplicate. Returns (added, status, representative_index, certified_solution) where status is one of :certified_distinct, :duplicate, or :not_certified. When added is true, certified_solution is the midpoint of the certified interval; otherwise nothing.
HomotopyContinuation.distinct_certified_solutions — Functiondistinct_certified_solutions(F, S, p = nothing; threading::Bool = Threads.nthreads() > 1, show_progress::Bool = true, certify_solution_kwargs...)Return a DistinctCertifiedSolutions struct containing distinct certified solutions obtained from a vector of solutions S of a system F. Compared to certify this only keeps the distinct certified solutions and not all certificates. This in in particular useful if you want to merge multiple large solution sets into one set of distinct certified solutions.
HomotopyContinuation.distinct_certified_solutions! — Functiondistinct_certified_solutions!(d::DistinctCertifiedSolutions, S; threading::Bool = Threads.nthreads() > 1, show_progress::Bool = true, certify_solution_kwargs...)Add a vector of solutions S to a DistinctCertifiedSolutions struct d.
HomotopyContinuation.stats — Functionstats(d::DistinctCertifiedSolutions)Return a named tuple with counters for processed candidates, certified-distinct solutions, duplicates, and non-certified candidates.
Helper functions
HomotopyContinuation.ncertified — Functionncertified(R::CertificationResult)Returns the number of certified solutions.
ncertified(R::IteratorCertificationResult)Return the number of path results that were certified.
HomotopyContinuation.nreal_certified — Functionnreal_certified(R::CertificationResult)Returns the number of certified real solutions.
nreal_certified(R::IteratorCertificationResult)Return the number of certified path results that were certified real.
HomotopyContinuation.ncomplex_certified — Functionncomplex_certified(R::CertificationResult)Returns the number of certified complex solutions.
ncomplex_certified(R::IteratorCertificationResult)Return the number of certified path results that were certified non-real complex.
HomotopyContinuation.ndistinct_certified — Functionndistinct_certified(R::CertificationResult)Returns the number of distinct certified solutions.
ndistinct_certified(R::IteratorCertificationResult)Return the number of distinct certified solutions obtained after leafwise certification.
HomotopyContinuation.ndistinct_real_certified — Functionndistinct_real_certified(R::CertificationResult)Returns the number of distinct certified real solutions.
ndistinct_real_certified(R::IteratorCertificationResult)Return the number of distinct certified solutions that were certified real.
HomotopyContinuation.ndistinct_complex_certified — Functionndistinct_complex_certified(R::CertificationResult)Returns the number of distinct certified complex solutions.
ndistinct_complex_certified(R::IteratorCertificationResult)Return the number of distinct certified solutions that were certified non-real complex.
Missing docstring for nprocessed. Check Documenter's build log for details.
Missing docstring for nduplicates. Check Documenter's build log for details.
HomotopyContinuation.nnotcertified — Functionnnotcertified(R::IteratorCertificationResult)Return the number of path results that could not be certified.
HomotopyContinuation.npaths — Functionnpaths(R::IteratorCertificationResult)Return the total number of path results produced by the iterator.
HomotopyContinuation.start_iterator_length — Functionstart_iterator_length(R::IteratorCertificationResult)Return the length of the iterator for the start system.
HomotopyContinuation.target_iterator_length — Functiontarget_iterator_length(R::IteratorCertificationResult)Return the length of the iterator for the target system.
HomotopyContinuation.nleaves — Functionnleaves(R::IteratorCertificationResult)Return the number of BSP leaves in the final partition.
HomotopyContinuation.max_leaf_size — Functionmax_leaf_size(R::IteratorCertificationResult)Return the size of the largest BSP leaf.
HomotopyContinuation.oversized_leaves — Functionoversized_leaves(R::IteratorCertificationResult)Return the number of terminal BSP leaves whose size exceeds the requested leaf_size_bound.
HomotopyContinuation.unsplittable_leaves — Functionunsplittable_leaves(R::IteratorCertificationResult)Return the number of BSP leaves that could not be refined further in the chosen projection.
HomotopyContinuation.nleaf_splits — Functionnleaf_splits(R::IteratorCertificationResult)Return the number of local BSP refinement steps performed during certification.
HomotopyContinuation.save — Methodsave(filename, C::CertificationResult)Store a text representation of the certification result C on disk.
HomotopyContinuation.show_straight_line_program — Functionshow_straight_line_program(R::CertificationResult)
show_straight_line_program(io::IO, R::CertificationResult)Print a representation of the used straight line program.