canuc80k7708·9/39

Cờ Trên Trục Số

Nộp bài trên LQDOJ

Bài 77 · 2-SAT

Có lá cờ trên một trục số. Cờ được đặt tại đúng một trong hai tọa độ hoặc . Sau khi đặt, khoảng cách giữa mọi cặp cờ khác nhau phải ít nhất là . Hãy xác định tính khả thi và, nếu có, đưa ra một cách đặt.

Input

  • Dòng đầu chứa hai số nguyên và .
  • Mỗi trong dòng tiếp theo chứa hai số nguyên và .

Output

  • Nếu không thể đặt đủ cờ, in No.
  • Nếu có thể, in Yes, sau đó in dòng. Dòng thứ chứa tọa độ đã chọn cho cờ .

Constraints

Scoring

  • Subtask ( số điểm): .
  • Subtask ( số điểm): Không có giới hạn bổ sung.

Example

Test 1

Input

2 8
3 13
5 7

Output

Yes
13
5

Giải thích: Ba cặp lựa chọn còn lại đều có khoảng cách nhỏ hơn ; chỉ cặp tọa độ và có khoảng cách đúng bằng , nên đây là phương án duy nhất.

Test 2

Input

2 10
0 5
3 8

Output

No

Giải thích: Mọi tọa độ của cờ thứ nhất đều cách mọi tọa độ của cờ thứ hai ít hơn , nên không thể đặt cả hai.

Lời giải tóm tắt
  • Phân tích: Mỗi đối tượng có đúng hai lựa chọn, nên ta biểu diễn bằng một biến Boolean. Gọi biến của cờ i cho biết chọn X_i hay Y_i. Hai lựa chọn thuộc hai cờ khác nhau bị cấm đi cùng nhau khi khoảng cách của chúng nhỏ hơn D.
  • Phân tích: Mỗi cấm đoán “không được đồng thời chọn A và B” tương đương clause (NOT A OR NOT B). Các quan hệ bằng nhau hoặc khác nhau cũng viết được bằng hai clause. Với clause (P OR Q), thêm hai cung kéo theo NOT P -> Q và NOT Q -> P.
  • Thuật toán: 1. Tạo hai đỉnh literal cho mỗi biến. 2. Chuyển từng quan hệ của đề thành các clause hai literal và thêm cung kéo theo. 3. Tìm các thành phần liên thông mạnh bằng hai lượt DFS lặp. 4. Nếu một biến và phủ định của nó nằm cùng SCC, hệ vô nghiệm. Ngược lại, thứ tự SCC cho một phép gán hợp lệ. 5. Từ phép gán, in tọa độ X_i hoặc Y_i tương ứng; nếu mâu thuẫn SCC thì in No.
  • Chứng minh đúng: Mỗi clause được thêm là tương đương chính xác với một quan hệ hoặc một cặp lựa chọn bị cấm trong đề. Vì vậy, một phép gán thỏa công thức 2-CNF khi và chỉ khi các lựa chọn tương ứng thỏa toàn bộ yêu cầu gốc. Tiêu chuẩn SCC của 2-SAT phát hiện vô nghiệm đúng khi một literal và phủ định của nó kéo theo lẫn nhau. Khi không có cặp như vậy, phép gán theo thứ tự SCC thỏa mọi cung kéo theo, do đó thỏa mọi clause. Bởi vậy thuật toán báo đúng tính khả thi và mọi chứng nhận được in đều hợp lệ.
  • Độ phức tạp: O(N^2) thời gian và O(N^2) bộ nhớ trong trường hợp xấu nhất.