Check for Disjointness of Sets

The function isdisjoint checks whether the intersection of two sets is empty. It can optionally produce a witness if the intersection is nonempty.

Examples

We use the following four sets for illustration.

using LazySets, LazySets.Approximations, Plots
B1 = Ball1(-ones(2), 1.)
B2 = Ball2(ones(2), 1.)
BI = BallInf(zeros(2), 1.)
H = Hyperrectangle(ones(2), ones(2))
sets = [B1, B2, BI, H]

function plot_sets(sets)
    for S in sets
        println(S)
        plot!(S, 1e-2, fillalpha=0.1)
    end
end

function plot_points(points, prefix)
    for i in eachindex(points)
        p = points[i]
        num_occur = length(findfirst(x -> x == p, points[1:i]))
        x = p[1]
        y = p[2]
        if num_occur == 1
            x += 0.15
        elseif num_occur == 2
            y += 0.15
        elseif num_occur == 3
            x -= 0.15
        else
            y -= 0.15
        end
        plot!(Singleton(p))
        plot!(annotations=(x, y, text("$(prefix)$(i)")))
    end
end

plot1 = plot()
plot_sets(sets)
plot1

println(isdisjoint(BI, H))
w1 = isdisjoint(BI, H, true)[2]
println(isdisjoint(B1, BI))
w2 = isdisjoint(B1, BI, true)[2]
println(isdisjoint(B1, H))

false
false
true

witnesses = [w1, w2]

plot1 = plot()
plot_sets(sets)
plot_points(witnesses, "w")
plot1

Methods

Base.isdisjoint — Method

isdisjoint(X::LazySet, Y::LazySet, [witness]::Bool=false)

Check whether two sets are disjoint (i.e., do not intersect), and optionally compute a witness.

Input

X – set
Y – set
witness – (optional, default: false) compute a witness if activated

Output

If the witness option is deactivated: true iff $X ∩ Y = ∅$
If the witness option is activated:
- (true, []) iff $X ∩ Y = ∅$
- (false, v) iff $X ∩ Y ≠ ∅$ for some $v ∈ X ∩ Y$

Notes

The convenience alias is_intersection_empty is also available.

source

Base.isdisjoint — Function

Extended help

isdisjoint(X::LazySet, S::AbstractSingleton, [witness]::Bool=false)

Algorithm

Let $S = \{s\}$. Then $S ∩ X = ∅$ iff $s ∉ X$.

source

Base.isdisjoint — Function

Extended help

isdisjoint(Z::AbstractZonotope, H::Hyperplane, [witness]::Bool=false)

Algorithm

$Z ∩ H = ∅$ iff $(b - a⋅c) ∉ \left[ ± ∑_{i=1}^p |a⋅g_i| \right]$, where $a$, $b$ are the hyperplane coefficients, $c$ is the zonotope's center, and $g_i$ are the zonotope's generators.

For witness production we fall back to a less efficient implementation for general sets as the first argument.

source

Base.isdisjoint — Function

Extended help

isdisjoint(X::LazySet, hp::Hyperplane, [witness]::Bool=false)

Notes

This implementation assumes that the set X is convex.

Algorithm

A convex set intersects with a hyperplane iff the support function in the negative resp. positive direction of the hyperplane's normal vector $a$ is to the left resp. right of the hyperplane's constraint $b$:

\[-ρ(-a, X) ≤ b ≤ ρ(a, X)\]

For witness generation, we compute a line connecting the support vectors to the left and right, and then take the intersection of the line with the hyperplane. We follow this algorithm for the line-hyperplane intersection.

source

Base.isdisjoint — Function

Extended help

isdisjoint(X::LazySet, hs::HalfSpace, [witness]::Bool=false)

Algorithm

A set intersects with a half-space iff the support function in the negative direction of the half-space's normal vector $a$ is less than the constraint $b$ of the half-space: $-ρ(-a, X) ≤ b$.

For compact set X, we equivalently have that the support vector in the negative direction $-a$ is contained in the half-space: $σ(-a) ∈ hs$. The support vector is thus also a witness if the sets are not disjoint.

source

Base.isdisjoint — Function

Extended help

isdisjoint(P::AbstractPolyhedron, X::LazySet, [witness]::Bool=false;
           [solver]=nothing, [algorithm]="exact")

Input

solver – (optional, default: nothing) the backend used to solve the linear program
algorithm – (optional, default: "exact") algorithm keyword, one of: * "exact" (exact, uses a feasibility LP) *"sufficient" (sufficient, uses half-space checks)

Notes

For algorithm == "exact", we assume that constraints_list(X) is defined. For algorithm == "sufficient", witness production is not supported.

For solver == nothing, we fall back to default_lp_solver(N).

Algorithm

For algorithm == "exact", see isempty(P::HPoly, ::Bool).

For algorithm == "sufficient", we rely on the intersection check between the set X and each constraint in P. This requires one support-function evaluation of X for each constraint of P. With this algorithm, the method may return false even in the case where the intersection is empty. On the other hand, if the algorithm returns true, then it is guaranteed that the intersection is empty.

source

Base.isdisjoint — Function

Extended help

isdisjoint(C::Complement, X::LazySet, [witness]::Bool=false)

Algorithm

We fall back to X ⊆ C.X, which can be justified as follows:

\[ X ∩ Y^C = ∅ ⟺ X ⊆ Y\]

source

Base.isdisjoint — Function

Extended help

isdisjoint(cpa::CartesianProductArray, P::AbstractPolyhedron,
           [witness]::Bool=false)

Notes

This implementation assumes that the sets in the Cartesian product cpa are polyhedral.

cpa – Cartesian products of a finite number of polytopes

Algorithm

We first identify the blocks of cpa in which P is constrained. Then we project cpa to those blocks and convert the result to an HPolytope (or HPolyhedron if the set type is not known to be bounded) Q. Finally we determine whether Q and the projected P intersect.

source

Base.isdisjoint — Function

Extended help

isdisjoint(X::CartesianProductArray, Y::CartesianProductArray,
           [witness]::Bool=false)

Notes

The implementation requires (and checks) that the Cartesian products have the same block structure.

Witness production is currently not supported.

source

Base.isdisjoint — Function

Extended help

isdisjoint(cpa::CartesianProductArray, H::AbstractHyperrectangle,
           [witness]::Bool=false)

Algorithm

The sets cpa and H are disjoint if and only if at least one block of cpa and the corresponding projection of H are disjoint. We perform these checks sequentially.

source