1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53

def visualize_boolean_monotonicity(lo: int, hi: int, is_feasible) -> None:
    """
    Visualize the boolean partition created by a monotonic feasibility function.
    
    For minimization: should see [False, False, ..., False, True, True, ..., True]
    For maximization: should see [True, True, ..., True, False, False, ..., False]
    """
    print(f"Feasibility across [{lo}, {hi}]:")
    print()
    
    results = []
    first_true = None
    last_true = None
    
    for x in range(lo, hi + 1):
        result = is_feasible(x)
        results.append(("T" if result else "F", x))
        if result and first_true is None:
            first_true = x
        if result:
            last_true = x
    
    # Print first 20 and last 5 for large ranges
    to_print = results[:20] + ["..."] + results[-5:] if len(results) > 30 else results
    print(" ".join(str(r[0]) + f"({r[1]})" if isinstance(r, tuple) else r for r in to_print))
    print()
    print(f"First True (min answer): {first_true}")
    print(f"Last True (max answer): {last_true}")
 
 
# Example: Ship packages problem
def can_ship(capacity: int) -> bool:
    weights = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
    D = 5
    days_needed = 1
    current_load = 0
    for w in weights:
        if current_load + w <= capacity:
            current_load += w
        else:
            days_needed += 1
            current_load = w
    return days_needed <= D
 
 
# Visualization
visualize_boolean_monotonicity(10, 25, can_ship)
 
# Output:
# Feasibility across [10, 25]:
# F(10) F(11) F(12) F(13) F(14) T(15) T(16) T(17) T(18) T(19) T(20) T(21) T(22) T(23) T(24) T(25)
# First True (min answer): 15
# Last True (max answer): 25

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67

"""
Monotonicity Proof: Shipping Problem
 
Feasibility: can_ship(weights, D, capacity) -> bool
 
Claim: If can_ship(weights, D, C) == True, then can_ship(weights, D, C+1) == True
 
Intuitive argument (simulation-based):
- With capacity C, suppose we ship packages using a greedy assignment
- Each day, we load packages until adding one more would exceed C
- This produces some schedule S with days_needed(S) <= D
 
- Now consider capacity C+1:
- We use the SAME schedule S
- Every package fits (since each day's load <= C < C+1)
- Therefore days_needed(S) <= D still holds
 
- Hence if C works, C+1 works
 
Mathematical formalization:
Let schedule(C) = optimal # of days for capacity C
Then: schedule(C+1) <= schedule(C) for all C
 
This is a non-increasing function, which gives:
- For minimization (find smallest working C):
  can_ship(C) = True  → can_ship(C+1) = True  (non-decreasing boolean)
  
The sequence looks like: [False, False, ..., False, True, True, ..., True]
"""
 
def verify_monotonicity(weights, D, lo, hi):
    """
    Empirically verify monotonicity of the shipping feasibility function.
    Returns True if monotonicity holds across the range.
    """
    def can_ship(capacity):
        days = 1
        load = 0
        for w in weights:
            if load + w <= capacity:
                load += w
            else:
                days += 1
                load = w
        return days <= D
    
    prev_result = can_ship(lo)
    transition_count = 0
    
    for c in range(lo + 1, hi + 1):
        curr_result = can_ship(c)
        if prev_result != curr_result:
            transition_count += 1
            if prev_result == True:  # True -> False is wrong direction
                print(f"ERROR: Transition True->False at capacity {c}")
                return False
        prev_result = curr_result
    
    print(f"Monotonicity verified! Transitions: {transition_count}")
    return transition_count <= 1  # Should transition at most once
 
 
# Verify for shipping problem
weights = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
D = 5
verify_monotonicity(weights, D, 10, 55)
# Output: Monotonicity verified! Transitions: 1

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

def binary_search_continuous(lo: float, hi: float, is_feasible, epsilon: float = 1e-9) -> float:
    """
    Binary search on continuous (real-valued) answer space.
    
    Finds the minimum x in [lo, hi] such that is_feasible(x) == True.
    Assumes monotonic feasibility: [False, False, ..., True, True, ...]
    
    Args:
        lo: Lower bound (must be infeasible or boundary)
        hi: Upper bound (must be feasible)
        is_feasible: Monotonic predicate function
        epsilon: Precision threshold
        
    Returns:
        Minimum feasible value within epsilon precision
    """
    # Method 1: Epsilon-based termination
    while hi - lo > epsilon:
        mid = (lo + hi) / 2
        if is_feasible(mid):
            hi = mid  # Answer is at mid or to the left
        else:
            lo = mid  # Answer is to the right
    
    return (lo + hi) / 2
 
 
def binary_search_continuous_iterations(lo: float, hi: float, is_feasible, iterations: int = 100) -> float:
    """
    Alternative: Fixed number of iterations (more predictable runtime).
    
    100 iterations gives precision of (hi - lo) / 2^100 ≈ 10^-30 * original range
    More than enough for double precision floats.
    """
    for _ in range(iterations):
        mid = (lo + hi) / 2
        if is_feasible(mid):
            hi = mid
        else:
            lo = mid
    
    return (lo + hi) / 2
 
 
# Example: Find minimum radius to cover all points with circles of equal radius
def min_radius_to_cover_points(points: list[tuple[float, float]], centers: list[tuple[float, float]]) -> float:
    """
    Find minimum radius r such that every point is within distance r
    of at least one center.
    """
    import math
    
    def is_feasible(radius: float) -> bool:
        # Check if all points are covered by some circle
        for px, py in points:
            covered = False
            for cx, cy in centers:
                dist = math.sqrt((px - cx)**2 + (py - cy)**2)
                if dist <= radius + 1e-12:  # Small epsilon for float comparison
                    covered = True
                    break
            if not covered:
                return False
        return True
    
    # Bounds: lo = 0, hi = max possible distance
    lo = 0.0
    hi = 0.0
    for px, py in points:
        for cx, cy in centers:
            dist = math.sqrt((px - cx)**2 + (py - cy)**2)
            hi = max(hi, dist)
    
    return binary_search_continuous(lo, hi, is_feasible)
 
 
# Example usage
points = [(0, 0), (3, 4), (6, 0)]
centers = [(1, 1), (5, 1)]
print(f"Minimum radius: {min_radius_to_cover_points(points, centers):.6f}")

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

def binary_search_minimization_with_invariants(lo: int, hi: int, is_feasible) -> int:
    """
    Binary search with explicit loop invariant annotations.
    Finds minimum x such that is_feasible(x) == True.
    
    Precondition: is_feasible is monotonically non-decreasing on [lo, hi]
    Precondition: is_feasible(hi) == True (at least one feasible value exists)
    
    Postcondition: Returns x* = min{x : is_feasible(x) == True}
    """
    # INVARIANT: answer ∈ [lo, hi]
    # INVARIANT: ∀ x < lo: is_feasible(x) == False
    # INVARIANT: ∀ x > hi: is_feasible(x) == True (but suboptimal)
    
    original_lo, original_hi = lo, hi
    answer = hi  # Default to upper bound (known feasible)
    
    while lo <= hi:
        # ASSERTION: answer ∈ [lo, original_hi]
        # ASSERTION: is_feasible(answer) == True
        
        mid = lo + (hi - lo) // 2  # Avoid overflow
        
        if is_feasible(mid):
            # mid is feasible; it might be the answer or something smaller is
            # ASSERTION: answer ∈ [lo, mid]
            answer = mid  # Update best known feasible
            hi = mid - 1  # Search for smaller feasible
            # MAINTAINS: ∀ x > hi (now = mid-1): is_feasible(x) == True
        else:
            # mid is infeasible; answer must be larger
            # ASSERTION: answer ∈ [mid+1, hi]
            lo = mid + 1  # Search for feasible in right half
            # MAINTAINS: ∀ x < lo (now = mid+1): is_feasible(x) == False
    
    # POSTCONDITION: lo > hi, so range is empty
    # POSTCONDITION: answer == min{x : is_feasible(x) == True}
    return answer

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

def check_monotonicity(lo: int, hi: int, is_feasible, expected_direction: str = "non-decreasing") -> bool:
    """
    Empirically verify monotonicity of a feasibility function.
    
    Args:
        lo, hi: Range to check
        is_feasible: The predicate function
        expected_direction: "non-decreasing" (for minimization) or "non-increasing" (for maximization)
        
    Returns:
        True if monotonicity holds, False otherwise
        
    Also prints diagnostic information if monotonicity fails.
    """
    results = [(x, is_feasible(x)) for x in range(lo, hi + 1)]
    
    # Find transitions
    transitions = []
    for i in range(1, len(results)):
        prev_x, prev_f = results[i-1]
        curr_x, curr_f = results[i]
        if prev_f != curr_f:
            transitions.append((prev_x, prev_f, curr_x, curr_f))
    
    # Check expected pattern
    if expected_direction == "non-decreasing":
        # Should only have False->True transitions
        for prev_x, prev_f, curr_x, curr_f in transitions:
            if prev_f == True and curr_f == False:
                print(f"❌ VIOLATION: True->False at {prev_x}->{curr_x}")
                print(f"   Expected: non-decreasing (F, F, ..., T, T, ...)")
                return False
    else:  # non-increasing
        # Should only have True->False transitions
        for prev_x, prev_f, curr_x, curr_f in transitions:
            if prev_f == False and curr_f == True:
                print(f"❌ VIOLATION: False->True at {prev_x}->{curr_x}")
                print(f"   Expected: non-increasing (T, T, ..., F, F, ...)")
                return False
    
    if len(transitions) > 1:
        print(f"⚠ WARNING: {len(transitions)} transitions found (expected at most 1)")
        print(f"   Transitions: {transitions}")
    
    print(f"✓ Monotonicity ({expected_direction}) verified with {len(transitions)} transition(s)")
    return True
 
 
# Example usage
def can_ship(weights, D, capacity):
    days = 1
    load = 0
    for w in weights:
        if load + w <= capacity:
            load += w
        else:
            days += 1
            load = w
    return days <= D
 
weights = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
D = 5
is_feasible = lambda c: can_ship(weights, D, c)
 
check_monotonicity(10, 30, is_feasible, "non-decreasing")