Solver สำหรับค้นหาจุดแก้ไขของระบบบูลีน
Intro: ปัญหา
ปัญหาของฉันเกี่ยวข้องกับการแก้ระบบสมการที่ค้นหาจุดตรึงของระบบบูลีนที่ศึกษา ($F(X)=X$).
ตัวอย่างง่ายๆ
ปล่อย $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$เป็นตัวแปรบูลีนที่น่าสนใจ ปล่อย$F=\{f_1,f_2,f_3\}$เป็นฟังก์ชันการปรับปรุงสำหรับตัวแปรเหล่านี้ (เช่น$x_i(t+1) = f_i(x(t))$) กำหนดให้เป็นฟังก์ชันเงื่อนไขต่อไปนี้ (ขึ้นอยู่กับอินพุตของแต่ละตัวแปร - โหนดในแนวคิดกราฟที่เกี่ยวข้อง):
$f_1 = \begin{cases} 1, -x_2 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_2 = \begin{cases} 1, x_1-x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_3 = \begin{cases} 1, x_1+x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$
ฟังก์ชันเหล่านี้ได้รับแรงบันดาลใจจากคำถามนี้
เป้าหมายคือการค้นหาชุดคำตอบ $\bar{x}$ (อาจเป็นศูนย์หนึ่งหรือหลายตัวต่อ se) ซึ่ง $F(\bar{x})=\bar{x}$.
ตัวอย่างข้างต้นเป็นกรณีที่ง่ายมาก ในท้ายที่สุดฉันต้องการแก้ระบบสมการที่มีตัวแปรหลายร้อยตัว โปรดทราบว่าการทำงานในสภาพที่จะเป็นเชิงเส้นรวมกันของปัจจัยการผลิตแต่ละตัวแปรและตัวแปรเสมอบูล
คำถาม
ฉันต้องการตัวแก้ปัญหาที่มีประสิทธิภาพสำหรับปัญหาประเภทนี้ (ซึ่งเรียกว่าNP-hard btw!) เช่นปัญหานี้สามารถกำหนดเป็นโปรแกรมข้อ จำกัด และแก้ไขโดยใช้เทคนิค Answer Set Programming (ASP) ได้หรือไม่
คำตอบ
ปรากฎว่า ASP สามารถใช้แก้ปัญหานี้ได้! ที่นี่ฉันให้การเข้ารหัสที่เป็นไปได้ของปัญหาในไฟล์ชื่อfp.lp:
% variables
var(1..3).
% functions
% f(Function,Coefficient,Variable)
f(1,-1,2).
f(2,1,1).
f(2,-1,3).
f(3,1,1).
f(3,1,3).
% guess assignment to variables
{ init(V) : var(V) }.
% compute functions
next(F) :- var(F), #sum { C,V : f(F,C,V), init(V) } >= 0.
% check if fixed point
:- init(V), not next(V).
:- next(V), not init(V).
#show next/1.
#show init/1.
การใช้clingo(เวอร์ชัน5.4.0) จากบรรทัดคำสั่ง: clingo fp.lpเราได้รับUNSATISFIABLEสำหรับอินสแตนซ์เฉพาะนี้
แสดงความคิดเห็น%f(2,1,1).และเรียกใช้ตัวclingoแก้ปัญหาที่เราได้รับอีกครั้ง:
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
ตัวแปรที่ส่งคืนทั้งในเพรดิเคตinit/1และnext/1ตัวแปรจะถูกแปลเป็นตัวแปรบูลีนที่ใช้งานอยู่ (1) และตัวแปรที่ขาดไปเป็นค่าที่ไม่ใช้งาน (0) ผลลัพธ์ที่ได้จึงเป็นเวกเตอร์บูลีน$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
เครดิตสำหรับคำตอบนี้ส่งไปที่ Roland Kaminski สมาชิกคนอื่น ๆ ของชุมชน ASP potassco ได้แสดงความคิดเห็นและแนวทางแก้ไขที่เป็นประโยชน์ สำหรับข้อมูลเพิ่มเติมเกี่ยวกับ ASP โปรดตรวจสอบ:https://potassco.org/