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 — Function

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

Check whether two sets do not intersect, and otherwise optionally compute a witness.

Input

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

Output

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

Algorithm

This is a fallback implementation that computes the concrete intersection, intersection, of the given sets.

A witness is constructed using the an_element implementation of the result.

source

Base.isdisjoint — Function

isdisjoint(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
           [witness]::Bool=false)

Check whether two hyperrectangular sets do not intersect, and otherwise optionally compute a witness.

Input

H1 – hyperrectangular set
H2 – hyperrectangular set
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $H1 ∩ H2 = ∅$
If witness option is activated:
- (true, []) iff $H1 ∩ H2 = ∅$
- (false, v) iff $H1 ∩ H2 ≠ ∅$ and $v ∈ H1 ∩ H2$

Algorithm

$H1 ∩ H2 ≠ ∅$ iff $|c_2 - c_1| ≤ r_1 + r_2$, where $≤$ is taken component-wise.

A witness is computed by starting in one center and moving toward the other center for as long as the minimum of the radius and the center distance. In other words, the witness is the point in H1 that is closest to the center of H2.

source

Base.isdisjoint — Function

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

Check whether a set and a set with a single value do not intersect, and otherwise optionally compute a witness.

Input

X – set
S – set with a single value
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $S ∩ X = ∅$
If witness option is activated:
- (true, []) iff $S ∩ X = ∅$
- (false, v) iff $S ∩ X ≠ ∅$ and v = element(S) $∈ S ∩ X$

Algorithm

$S ∩ X = ∅$ iff element(S) $∉ X$.

source

Base.isdisjoint — Function

isdisjoint(S1::AbstractSingleton, S2::AbstractSingleton,
           [witness]::Bool=false)

Check whether two sets with a single value do not intersect, and otherwise optionally compute a witness.

Input

S1 – set with a single value
S2 – set with a single value
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $S1 ∩ S2 = ∅$
If witness option is activated:
- (true, []) iff $S1 ∩ S2 = ∅$
- (false, v) iff $S1 ∩ S2 ≠ ∅$ and v = element(S1) $∈ S1 ∩ S2$

Algorithm

$S1 ∩ S2 = ∅$ iff $S1 ≠ S2$.

source

Base.isdisjoint — Function

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

Check whether a zonotopic set and a hyperplane do not intersect, and otherwise optionally compute a witness.

Input

Z – zonotopic set
H – hyperplane
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $Z ∩ H = ∅$
If witness option is activated:
- (true, []) iff $Z ∩ H = ∅$
- (false, v) iff $Z ∩ H ≠ ∅$ and $v ∈ Z ∩ H$

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

isdisjoint(L1::LineSegment, L2::LineSegment, [witness]::Bool=false)

Check whether two line segments do not intersect, and otherwise optionally compute a witness.

Input

L1 – line segment
L2 – line segment
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $L1 ∩ L2 = ∅$
If witness option is activated:
- (true, []) iff $L1 ∩ L2 = ∅$
- (false, v) iff $L1 ∩ L2 ≠ ∅$ and $v ∈ L1 ∩ L2$

Algorithm

The algorithm is inspired from here, which again is the special 2D case of a 3D algorithm from [1].

We first check if the two line segments are parallel, and if so, if they are collinear. In the latter case, we check membership of any of the end points in the other line segment. Otherwise the lines are not parallel, so we can solve an equation of the intersection point, if it exists.

[1] Ronald Goldman. Intersection of two lines in three-space. Graphics Gems

source

Base.isdisjoint — Function

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

Check whether a convex set an a hyperplane do not intersect, and otherwise optionally compute a witness.

Input

X – convex set
hp – hyperplane
witness – (optional, default: false) compute a witness if activated

Output

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

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

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

Check whether a set an a half-space do not intersect, and otherwise optionally compute a witness.

Input

X – set
hs – half-space
witness – (optional, default: false) compute a witness if activated

Output

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

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(H1::HalfSpace, H2::HalfSpace, [witness]::Bool=false)

Algorithm

Two half-spaces do not intersect if and only if their normal vectors point in the opposite direction and there is a gap between the two defining hyperplanes.

The latter can be checked as follows: Let $H1 : a_1⋅x = b_1$ and $H2 : a_2⋅x = b_2$. Then we already know that $a_2 = -k⋅a_1$ for some positive scaling factor $k$. Let $x_1$ be a point on the defining hyperplane of $H1$. We construct a line segment from $x_1$ to the point $x_2$ on the defining hyperplane of $hs_2$ by shooting a ray from $x_1$ with direction $a_1$. Thus we look for a factor $s$ such that $(x_1 + s⋅a_1)⋅a_2 = b_2$. This gives us $s = (b_2 - x_1⋅a_2) / (-k a_1⋅a_1)$. The gap exists if and only if $s$ is positive.

If the normal vectors do not point in opposite directions, then the defining hyperplanes intersect and we can produce a witness as follows. All points $x$ in this intersection satisfy $a_1⋅x = b_1$ and $a_2⋅x = b_2$. Thus we have $(a_1 + a_2)⋅x = b_1+b_2$. We now find a dimension where $a_1 + a_2$ is non-zero, say, $i$. Then the result is a vector with one non-zero entry in dimension $i$, defined as $[0, …, 0, (b_1 + b_2)/(a_1[i] + a_2[i]), 0, …, 0]$. Such a dimension $i$ always exists.

source

Base.isdisjoint — Function

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

Check whether a polyhedral set and another set do not intersect, and otherwise optionally compute a witness.

Input

P – polyhedral set
X – set (see the Notes section below)
witness – (optional, default: false) compute a witness if activated
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)

Output

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

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

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

Check whether a union of two sets and another set do not intersect, and otherwise optionally compute a witness.

Input

U – union of two sets
X – set
witness – (optional, default: false) compute a witness if activated

Output

true iff $\text{U} ∩ X = ∅$.

source

Base.isdisjoint — Function

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

Check whether a union of a finite number of sets and another set do not intersect, and otherwise optionally compute a witness.

Input

U – union of a finite number of sets
X – set
witness – (optional, default: false) compute a witness if activated

Output

true iff $\text{U} ∩ X = ∅$.

source

Base.isdisjoint — Function

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

Check whether a universe and another set do not intersect, and otherwise optionally compute a witness.

Input

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

Output

true iff $X ≠ ∅$.

source

Base.isdisjoint — Function

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

Check whether the complement of a set and another set do not intersect, and otherwise optionally compute a witness.

Input

C – complement of a set
X – set
witness – (optional, default: false) compute a witness if activated

Output

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

Algorithm

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

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

source

Base.isdisjoint — Function

isdisjoint(Z1::AbstractZonotope, Z2::AbstractZonotope,
           [witness]::Bool=false; [solver]=nothing)

Check whether two zonotopic sets do not intersect, and otherwise optionally compute a witness.

Input

Z1 – zonotopic set
Z2 – zonotopic set
witness – (optional, default: false) compute a witness if activated
solver – (optional, default: nothing) the backend used to solve the linear program

Output

If witness option is deactivated: true iff $Z1 ∩ Z2 = ∅$
If witness option is activated:
- (true, []) iff $Z1 ∩ Z2 = ∅$
- (false, v) iff $Z1 ∩ Z2 ≠ ∅$ and $v ∈ Z1 ∩ Z2$

Algorithm

The algorithm is taken from [1].

$Z1 ∩ Z2 = ∅$ iff $c_1 - c_2 ∉ Z(0, (g_1, g_2))$ where $c_i$ and $g_i$ are the center and generators of zonotope Zi and $Z(c, g)$ represents the zonotope with center $c$ and generators $g$.

[1] L. J. Guibas, A. T. Nguyen, L. Zhang: Zonotopes as bounding volumes. SODA

source

Base.isdisjoint — Function

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

Check whether a polytopic Cartesian product array and a polyhedral set do not intersect, and otherwise optionally compute a witness.

Input

cpa – Cartesian products of a finite number of polytopes
P – polyhedral set
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $\text{cpa} ∩ P = ∅$
If witness option is activated:
- (true, []) iff $\text{cpa} ∩ P = ∅$
- (false, v) iff $\text{cpa} ∩ P ≠ ∅$ and $v ∈ \text{cpa} ∩ P$

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

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

Check whether two Cartesian products of a finite number of sets with the same block structure do not intersect, and otherwise optionally compute a witness.

Input

X – Cartesian products of a finite number of sets
Y – Cartesian products of a finite number of sets
witness – (optional, default: false) compute a witness if activated

Output

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

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

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

Check whether a Cartesian product of a finite number of sets and a hyperrectangular set do not intersect, and otherwise optionally compute a witness.

Input

cpa – Cartesian product of a finite number of sets
H – hyperrectangular set
witness – (optional, default: false) compute a witness if activated

Output

If witness option is deactivated: true iff $cpa ∩ H = ∅$
If witness option is activated:
- (true, []) iff $cpa ∩ H = ∅$
- (false, v) iff $cpa ∩ H ≠ ∅$ and $v ∈ cpa ∩ H$

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

Base.isdisjoint — Function

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

Check whether two sets do not intersect, and otherwise optionally compute a witness.

Input

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

Output

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

Algorithm

This is a fallback implementation that computes the concrete intersection, intersection, of the given sets.

A witness is constructed using the an_element implementation of the result.

source

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

Check whether a polyhedral set and another set do not intersect, and otherwise optionally compute a witness.

Input

P – polyhedral set
X – set (see the Notes section below)
witness – (optional, default: false) compute a witness if activated
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)

Output

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

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).

source