Paracooba

พาราคูบา

นี่เป็นเครื่องมือแบบแยกส่วนสำหรับการแก้ปัญหา SAT และ QBF แบบขนานแบบกระจาย โดยจะจัดการกระบวนการแก้ไขสูตรโดยอัตโนมัติด้วยคิวบ์ที่ให้มาผ่านเครือข่ายของโหนดประมวลผล นอกจากนี้ยังมีอัลกอริธึมลูกบาศก์แบบรวมอีกด้วย สามารถจัดเตรียมลูกบาศก์ให้กับเครื่องมือนี้ได้ในรูปแบบ "iCNF" (DIMACS ปกติพร้อมลูกบาศก์ต่อท้ายในรูปแบบ a 1 2 3 0 ) ตัวอย่างเช่น คิวบ์เหล่านี้สามารถสร้างขึ้นได้ภายในเดือนมีนาคม

การใช้งาน [SAT]

สถานการณ์การใช้งานทั้งสองมีอธิบายไว้ด้านล่าง อาร์กิวเมนต์บรรทัดคำสั่งเพิ่มเติมมีให้ ใช้ --help สำหรับข้อมูลเพิ่มเติม ตัวเลือกบางตัวยังไม่มีผลกระทบใดๆ เนื่องจากมีการปรับปรุงใหม่ ไบนารี parac และ paracs มีฟังก์ชันเหมือนกัน แต่ paracs มีการเชื่อมโยงแบบคงที่กับโมดูลทั้งหมด ในขณะที่ parac โหลดโมดูลในขณะรันไทม์ หากคุณมีปัญหาในการค้นหาโมดูลที่จำเป็น ให้ใช้ paracs

ช่วงการประกาศจะควบคุมความถี่ของการออกอากาศ IPv4 UDP ไปยังซับเน็ตภายในเครื่องเพื่อค้นหาอินสแตนซ์อื่นๆ ของโมดูลตัวสื่อสารเริ่มต้น หรือสามารถระบุรีโมทอื่นๆ ได้โดยตรง

เมื่อจัดหาตัวเลือกเพิ่มเติมให้กับโมดูลตัวแก้ปัญหาให้กับโหนดหลัก โมดูลจะซิงค์ตัวเลือกที่มีให้กับโหนดอื่นที่เชื่อมต่อทั้งหมดโดยอัตโนมัติ เมื่อแก้ไขสูตรโดยไม่มีคิวบ์ที่กำหนดไว้ล่วงหน้า ตัวเลือก --resplit จะมีประโยชน์มาก เนื่องจากจะยกเลิก CaDiCaL โดยอัตโนมัติเมื่อการแก้ไขใช้เวลานานเกินไป และใช้ตัวแก้ปัญหา lookahead เพื่อสร้างคิวบ์ใหม่

ตัวอย่างหนึ่งวิธีการเริ่มต้นโหนดหลักใหม่แสดงไว้ด้านล่าง

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

การใช้งาน [QBF]

นอกเหนือจากโมดูลการแก้ปัญหา SAT แล้ว ตัวแก้ปัญหา QBF ยังรวมอยู่ในรูปแบบของโมดูล cpp_qbf_prefixexpander แยกวิเคราะห์สูตร QBF และให้คิวบ์ตัวแก้ปัญหา QBF ตามคำนำหน้า

การเรียกใช้เริ่มต้นใช้ตัวแก้ปัญหา QBF DepQBF เป็นแบ็กเอนด์และทำงานดังต่อไปนี้ (โดยใช้เวอร์ชันคงที่โดยไม่ต้องโหลดโมดูลแบบไดนามิก):

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

เครือข่าย

Master-Node ("แก้สูตรนี้ให้ฉัน")

 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