OR-Tools CP-SAT में आसन्नता निषेध के लिए मजबूत फॉर्म्युलेशन

चार पिंजरों में कुत्तों की बैठाई: OR-Tools CP-SAT में constraint का साफ फॉर्म्युलेशन. add_exactly_one और add_at_least_one से adjacency निषेध सही तरह मॉडल करें.

जोड़े-दर-जोड़े टकराव वाली इकाइयों को पास-पास स्लॉट में रखने-न-रखने का सवाल constraint programming का एक परिचित अभ्यास है। OR-Tools CP-SAT में इसे मॉडल करने का संक्षिप्त तरीका है बूलियन असाइनमेंट वैरिएबल्स और आसन्नता के नियम। फिर भी, add_implication के साथ दिखने में स्वाभाविक एन्कोडिंग व्यवहार में कभी-कभी संभव व्यवस्थाओं को उजागर नहीं करती। नीचे एक संपूर्ण वॉकथ्रू है जो पहले समस्या को पुन: उत्पन्न करता है और फिर एक मज़बूत फॉर्म्युलेशन दिखाता है जो सभी संभव प्लेसमेंट्स को साफ तौर पर सामने लाता है।

समस्या दिखाने वाला न्यूनतम मॉडल

परिदृश्य: चार कुत्ते, सीध में लगे चार पिंजरे, और कुछ ऐसी असंगत जोड़ियां जिन्हें आस-पास नहीं बैठना चाहिए। शुरुआती संस्करण add_implication के जरिए इन आसन्नता-वर्जनाओं को एन्कोड करता है।

from ortools.sat.python import cp_model
# डेटा
pets = ["Lulu", "Abby", "Boone", "Kensey"]
slots = ["cage_A", "cage_B", "cage_C", "cage_D"]
# असंगत जोड़ियां (पास-पास नहीं हो सकतीं)
clashes = [("Boone", "Lulu"), ("Boone", "Abby")]
# रैखिक निकटता क्रमबद्ध जोड़ियों के रूप में
neighbors = [("cage_A", "cage_B"), ("cage_B", "cage_C"), ("cage_C", "cage_D")]
# मॉडल
cp = cp_model.CpModel()
# बूलियन असाइनमेंट: पालतू p स्लॉट s में
assign = {}
for p in pets:
    for s in slots:
        assign[(p, s)] = cp.new_bool_var(f"y_{p}_{s}")
# हर पालतू ठीक एक स्लॉट में
for p in pets:
    cp.add(sum(assign[(p, s)] for s in slots) == 1)
# हर स्लॉट में अधिकतम एक पालतू
for s in slots:
    cp.add(sum(assign[(p, s)] for p in pets) <= 1)
# आसन्नता प्रतिबंध (इम्प्लिकेशन)
for a, b in clashes:
    for s1, s2 in neighbors:
        cp.add_implication(assign[(a, s1)], assign[(b, s2)].Not())
        cp.add_implication(assign[(b, s2)], assign[(a, s1)].Not())
# एक समाधान खोजें
engine = cp_model.CpSolver()
status = engine.Solve(cp)
# रिपोर्ट
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print("Solution:")
    for p in pets:
        for s in slots:
            if engine.value(assign[(p, s)]):
                print(f"  {p} -> {s}")
else:
    print("No solution found.")

असल में समस्या क्या है

उद्देश्य यह है कि चुनी गई जोड़ियों को पास-पास बैठने से रोका जाए, और साथ ही कुत्तों और पिंजरों के बीच एक परिपूर्ण मिलान सुनिश्चित हो। ऊपर वाले वैरिएंट में ये आसन्नता-निषेध इम्प्लिकेशन के रूप में लिखे गए हैं। देखा गया व्यवहार यह है कि सॉल्वर, संभव असाइनमेंट मौजूद होने पर भी, उनमें से कोई एक लौटाने में चूक सकता है। नीचे दिया गया फॉर्म्युलेशन इन्हें सीधे क्लॉज़ के रूप में पोस्ट करता है और दोनों अक्षों पर exact cover लागू करता है, जिससे यह समस्या नहीं आती।

कारगर फॉर्म्युलेशन और समाधान

नियमों को और सीधे कहा जा सकता है। पहला, द्विभाजित असाइनमेंट को add_exactly_one के साथ मॉडल करें—हर पालतू के लिए भी और हर स्लॉट के लिए भी। दूसरा, हर आसन्नता-निषेध को नकारे हुए लिटेरल्स के विस्युंजन (disjunction) के रूप में एन्कोड करें, यानी दो आसन्न प्लेसमेंट में से कम से कम एक झूठा होना चाहिए। इसके लिए नकारे हुए BoolVars पर add_at_least_one का उपयोग करें। इस तरह, सॉल्यूशनों को गिनना साफ-सुथरा हो जाता है; इस डेटा सेट पर चार समाधान मिलते हैं।

from ortools.sat.python import cp_model
# डेटा
pets = ["Lulu", "Abby", "Boone", "Kensey"]
slots = ["cage_A", "cage_B", "cage_C", "cage_D"]
clashes = [("Boone", "Lulu"), ("Boone", "Abby")]
neighbors = [("cage_A", "cage_B"), ("cage_B", "cage_C"), ("cage_C", "cage_D")]
# मॉडल
cp = cp_model.CpModel()
assign = {(p, s): cp.new_bool_var(f"y_{p}_{s}") for p in pets for s in slots}
# परिपूर्ण मिलान: प्रति पालतू ठीक एक
for p in pets:
    cp.add_exactly_one(assign[(p, s)] for s in slots)
# परिपूर्ण मिलान: प्रति स्लॉट ठीक एक
for s in slots:
    cp.add_exactly_one(assign[(p, s)] for p in pets)
# आसन्नता निषेध क्लॉज़ के रूप में: दोनों साथ में सत्य नहीं
for a, b in clashes:
    for s1, s2 in neighbors:
        cp.add_at_least_one(~assign[(a, s1)], ~assign[(b, s2)])
        cp.add_at_least_one(~assign[(b, s1)], ~assign[(a, s2)])
# एक समाधान खोजें
engine = cp_model.CpSolver()
status = engine.Solve(cp)
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print("Solution:")
    for p in pets:
        for s in slots:
            if engine.value(assign[(p, s)]):
                print(f"  {p} -> {s}")
else:
    print("No solution found.")

इस तरह लिखा मॉडल सभी संभव असाइनमेंट्स की गणना को सीधा बना देता है। एक रन में चार अलग-अलग समाधान रिपोर्ट हुए—जैसे Boone को cage_A में रखा गया और उसके बगल में Kensey, या Boone को cage_D में और दूसरी ओर पास में Kensey। बाकी विकल्प भी दिए गए डेटा के अनुरूप इसी ढांचे का पालन करते हैं।

यह जानना क्यों उपयोगी है

CP-SAT में, प्रतिबंधों का रूप जितना स्पष्ट होता है, उतना ही बेहतर। permutation जैसी संरचनाओं के लिए add_exactly_one सॉल्वर को बिना अस्पष्टता के बताता है कि यह एक परिमेय व्यवस्था है। आसन्नता निषेधों के लिए, नकारे हुए लिटेरल्स पर add_at_least_one से सीधे क्लॉज़ लिखना “दोनों साथ में नहीं” को उसी रूप में व्यक्त करता है जिसे SAT कोर सहज रूप से संभालता है। इससे संभव क्षेत्र साफ दिखता है और समाधान-गणना अपेक्षा के मुताबिक होती है।

निष्कर्ष

स्थानीय टकराव वाले असाइनमेंट समस्याओं में, दोनों आयामों पर matching को add_exactly_one से व्यक्त करें और जोड़ीवार “पास-पास नहीं” को नकारे हुए लिटेरल्स पर add_at_least_one वाली क्लॉज़ के रूप में लिखें। यह फॉर्म्युलेशन संक्षिप्त, डिबग करने में आसान है और इस डेटा सेट के लिए संभव असाइनमेंट बिना किसी आश्चर्य के देता है।