import clingo

def kha_thi(h):
    ctl = clingo.Control()
    ctl.add("base", [], f"""
        lop(a;b;c). ca(1..{h}).
        1 {{ xep(L,C) : ca(C) }} 1 :- lop(L).
        :- xep(L,C), xep(M,C), L<M.
    """)
    ctl.ground([("base", [])])
    return bool(ctl.solve().satisfiable)

def can_dau(ngan, dai):
    if not kha_thi(dai):
        raise ValueError("Cận trên chưa có lịch khả thi")
    while ngan < dai:
        giua = (ngan + dai) // 2
        if kha_thi(giua):
            dai = giua
        else:
            ngan = giua + 1
    return ngan

assert [kha_thi(h) for h in range(1, 5)] == [False, False, True, True]
assert can_dau(1, 4) == 3
print("Horizon nhỏ nhất bằng 3.")