Paracooba

باراكوبا

هذه أداة معيارية لحل SAT وQBF المتوازي الموزع. يقوم تلقائيًا بإدارة عملية حل الصيغ باستخدام المكعبات المتوفرة عبر شبكة من العقد الحسابية. كما أن لديها خوارزمية تكعيب متكاملة. يمكن توفير المكعبات لهذه الأداة بتنسيق "iCNF" (DIMACS العادي مع المكعبات الملحقة بالنموذج a 1 2 3 0 ). يمكن على سبيل المثال إنشاء هذه المكعبات بحلول شهر مارس.

الاستخدام [SAT]

يتم وصف سيناريوهي الاستخدام أدناه. يتم توفير وسائط سطر أوامر إضافية، استخدم --help لمزيد من المعلومات. بعض الخيارات ليس لها أي تأثيرات حتى الآن، حيث يتم إعادة صياغتها. الثنائيات parac و paracs متطابقتان وظيفيًا، لكن paracs مرتبطة بشكل ثابت بجميع الوحدات، بينما يقوم parac بتحميل الوحدات في وقت التشغيل. إذا كانت لديك مشاكل في العثور على الوحدات المطلوبة، استخدم paracs .

يتحكم الفاصل الزمني للإعلان في تردد عمليات بث IPv4 UDP في الشبكة الفرعية المحلية للعثور على مثيلات أخرى لوحدة الاتصال الافتراضية. وبدلاً من ذلك، يمكن تحديد أجهزة التحكم عن بعد الأخرى مباشرة.

عند توفير خيارات إضافية لوحدة الحل للعقدة الرئيسية، فإنها تقوم تلقائيًا بمزامنة الخيارات المتوفرة مع جميع العقد المتصلة الأخرى. عند حل الصيغ بدون مكعبات محددة مسبقًا، يكون خيار --resplit مفيدًا جدًا، لأنه يلغي CaDiCaL تلقائيًا عندما يستغرق الحل وقتًا طويلاً ويطبق حلاً أماميًا لإنشاء مكعب جديد.

أحد الأمثلة على كيفية بدء عقدة رئيسية جديدة موضح أدناه.

 parac <file.[i]cnf> [--cadical-cubes] [--resplit]

الاستخدام [QBF]

بالإضافة إلى وحدة حل SAT، تم أيضًا دمج محلل QBF في شكل الوحدة cpp_qbf_prefixexpander . يقوم بتوزيع صيغة QBF ويعطي مكعبات حل QBF بناءً على البادئة.

يستخدم الاستدعاء الافتراضي حل QBF DepQBF كواجهة خلفية ويعمل على النحو التالي (باستخدام الإصدار الثابت بدون تحميل الوحدة الديناميكية):

 paraqs <file.qdimacs> [--use-depqbf]

الشبكات

العقدة الرئيسية ("حل هذه الصيغة بالنسبة لي")

 parac <file.[i]cnf> [--udp-announcement-interval 1000]

Daemon-Node ("توفير عقدة حسابية للأساسيات الأخرى في الشبكة")

 parac [--known-remote hostname]

التبعيات الخارجية

تتطلب هذه الأداة التبعيات الخارجية التالية. يرجى التأكد من تثبيت رؤوس التطوير الخاصة بهم حتى تتمكن من تجميع البرنامج.

• تعزيز الرؤوس
• سجل التعزيز
• تعزيز خيارات البرنامج

الحد الأدنى لإصدار التعزيز الذي تم اختباره: 1.65.1

يتم تضمين كافة التبعيات الأخرى في هذه الشجرة المصدر (والوحدات الفرعية) ولا يلزم التعامل معها على وجه التحديد. يمكن أيضًا استبعاد Distrac من البناء، إما ببساطة عن طريق عدم استنساخ الوحدة الفرعية أو عن طريق ضبط -DENABLE_DISTRAC=OFF على CMake.

مبنى

 # Clone the repository
git clone https://github.com/maximaximal/Paracooba.git
git submodule update --init --recursive

# Build directory
mkdir build
cd build

# Building
cmake ..
make -j