การเขียนโปรแกรมชุดคำตอบ

การเขียนโปรแกรมชุดคำตอบ ( ASP ) เป็นรูปแบบหนึ่งของการเขียนโปรแกรมเชิงประกาศที่มุ่งเน้นไปที่ปัญหาการค้นหา ที่ยาก (ส่วนใหญ่เป็นปัญหา NP-hard ) โดยอิงจาก ความหมายของ แบบจำลองเสถียร (ชุดคำตอบ) ของการเขียนโปรแกรมเชิงตรรกะใน ASP ปัญหาการค้นหาจะถูกลดทอนลงเหลือการคำนวณแบบจำลองเสถียร และตัวแก้ปัญหาชุดคำตอบ ซึ่งเป็นโปรแกรมสำหรับสร้างแบบจำลองเสถียร จะถูกใช้เพื่อทำการค้นหา กระบวนการคำนวณที่ใช้ในการออกแบบตัวแก้ปัญหาชุดคำตอบจำนวนมากเป็นการปรับปรุงอัลกอริทึม DPLLและโดยหลักการแล้วจะสิ้นสุดลงเสมอ (แตกต่างจาก การประเมินคำถาม ของ Prologซึ่งอาจนำไปสู่ลูปไม่สิ้นสุด )

ในความหมายทั่วไป ASP ครอบคลุมการประยุกต์ใช้ชุดคำตอบทั้งหมดกับการแสดงความรู้และการให้เหตุผล^{[ 1 ]}^{[ 2 ]}และการใช้การประเมินแบบสอบถามสไตล์ Prolog เพื่อแก้ปัญหาที่เกิดขึ้นในการประยุกต์ใช้เหล่านี้

ประวัติศาสตร์

ตัวอย่างแรกๆ ของการเขียนโปรแกรมชุดคำตอบคือ วิธี การวางแผนที่เสนอโดย Dimopoulos, Nebel และ Köhler ในปี 1997 ^{[ 3 ]}^{[ 4 ]}แนวทางของพวกเขาขึ้นอยู่กับความสัมพันธ์ระหว่างแผนและแบบจำลองที่เสถียร^{[ 5 ]} ในปี 1998 Soininen และ Niemelä ^{[ 6 ]} ได้นำสิ่งที่ปัจจุบันเรียกว่าการเขียนโปรแกรมชุดคำตอบไปใช้กับปัญหาการกำหนดค่าผลิตภัณฑ์^{[ 4 ]}ในปี 1999 คำว่า "การเขียนโปรแกรมชุดคำตอบ" ปรากฏขึ้นเป็นครั้งแรกในหนังสือThe Logic Programming Paradigmในฐานะชื่อของชุดบทความสองฉบับ^{[ 4 ]}บทความฉบับแรกนี้ระบุการใช้ตัวแก้ปัญหาชุดคำตอบสำหรับการค้นหาเป็นกระบวนทัศน์การเขียนโปรแกรมใหม่^{[ 7 ]}ในปีเดียวกันนั้น Niemelä ยังได้เสนอ "โปรแกรมตรรกะที่มีความหมายแบบจำลองที่เสถียร" เป็นกระบวนทัศน์ใหม่ด้วย^{[ 8 ]}

ตอบชุดภาษาโปรแกรม AnsProlog

Lparseเป็นชื่อของโปรแกรมที่สร้างขึ้นมาแต่เดิมเพื่อเป็น เครื่องมือ พื้นฐาน (front-end) สำหรับตัวแก้ชุดคำตอบsmodelsภาษาที่ Lparse ยอมรับนั้นโดยทั่วไปเรียกว่า AnsProlog ^{[ 9 ]}ซึ่งย่อมาจากAnswer Set Programming in Logic [ ^{10 ] ปัจจุบัน}มีการใช้งานในลักษณะเดียวกันในตัวแก้ชุดคำตอบอื่นๆ อีกมากมาย รวมถึงassat , clasp , cmodels , gNt , nomore++และpbmodels ( dlvเป็นข้อยกเว้น ไวยากรณ์ของโปรแกรม ASP ที่เขียนสำหรับ dlv นั้นแตกต่างออกไปบ้าง)

โปรแกรม AnsProlog ประกอบด้วยกฎในรูปแบบต่อไปนี้

< ส่วนหัว> :- < ส่วนเนื้อหา> .

สัญลักษณ์:-("if") จะถูกละทิ้งหาก<body>ว่างเปล่า กฎดังกล่าวเรียกว่าข้อเท็จจริงกฎ Lparse ที่ง่ายที่สุดคือกฎที่มีข้อจำกัด

โครงสร้างที่มีประโยชน์อีกอย่างหนึ่งที่รวมอยู่ในภาษานี้คือทางเลือกตัวอย่างเช่น กฎการเลือก

{ p , q , r }

กล่าวว่า: เลือกอะตอมที่จะรวมไว้ในแบบจำลองเสถียรโดยพลการ โปรแกรม Lparse ที่มีกฎการเลือกนี้และไม่มีกฎอื่นใดจะมีแบบจำลองเสถียร 8 แบบ ซึ่งเป็นเซตย่อยโดยพลการของ นิยามของแบบจำลองเสถียรได้รับการขยายความไปยังโปรแกรมที่มีกฎการเลือก^[¹¹^] กฎการเลือกยังสามารถถือได้ว่าเป็นตัวย่อสำหรับ สูตรเชิงประพจน์ภายใต้ความหมาย ของแบบจำลองเสถียร^[¹²^] ตัวอย่างเช่น กฎการเลือกข้างต้นสามารถมองได้ว่าเป็นตัวย่อสำหรับการเชื่อมโยงของสูตร " ตรงกลางที่ถูกยกเว้น " สามสูตร: $p,q,r$ $\{p,q,r\}$

(p\lor \neg p)\land (q\lor \neg q)\land (r\lor \neg r)

ภาษาของ Lparse ยังช่วยให้เราสามารถเขียนกฎการเลือกแบบ "มีข้อจำกัด" ได้อีกด้วย เช่น

1 { p , q , r } 2.

กฎนี้กล่าวว่า: เลือกอะตอมอย่างน้อย 1 ตัวแต่ไม่เกิน 2 ตัว ความหมายของกฎนี้ภายใต้ความหมายเชิงแบบจำลองเสถียรนั้นแสดงด้วยสูตรเชิงประพจน์ $p,q,r$

(p\lor \neg p)\land (q\lor \neg q)\land (r\lor \neg r)

\land \,(p\lor q\lor r)\land \neg (p\land q\land r)

สามารถใช้ขอบเขตจำนวนสมาชิกในส่วนเนื้อหาของกฎได้เช่นกัน ตัวอย่างเช่น:

:- 2 { p , q , r }.

การเพิ่มข้อจำกัดนี้ลงในโปรแกรม Lparse จะกำจัดแบบจำลองเสถียรที่มีอะตอมอย่างน้อย 2 ตัวความหมายของกฎนี้สามารถแสดงได้ด้วยสูตรเชิงประพจน์ $p,q,r$

\neg ((p\land q)\lor (p\land r)\lor (q\land r))

ตัวแปร (ขึ้นต้นด้วยตัวพิมพ์ใหญ่ เหมือนในProlog ) ใช้ใน Lparse เพื่อย่อกลุ่มของกฎที่ใช้รูปแบบเดียวกัน และยังใช้เพื่อย่อกลุ่มของอะตอมภายในกฎเดียวกันด้วย ตัวอย่างเช่น โปรแกรม Lparse

p ( a ). p ( b ). p ( c ) . q ( X ) :- p ( X ), X ! = a .

มีความหมายเหมือนกับ

p ( a ). p ( b ). p ( c ). q ( b ). q ( c ).

โปรแกรม

p ( a ). p ( b ). p ( c ). { q ( X ):- p ( X )} 2.

เป็นคำย่อของ

p ( a ). p ( b ). p ( c ). { q ( a ), q ( b ), q ( c )} 2.

ช่วงราคาจะมีรูปแบบดังนี้:

( เริ่มต้น.. สิ้นสุด)

โดยที่ start และ end เป็นนิพจน์ทางคณิตศาสตร์ที่มีค่าคงที่ ช่วง (range) เป็นสัญลักษณ์ย่อที่ใช้เพื่อกำหนดขอบเขตเชิงตัวเลขในลักษณะที่เข้ากันได้ ตัวอย่างเช่น ข้อเท็จจริงที่ว่า

ก( 1..3 ).

เป็นทางลัดสำหรับ

a ( 1 ). a ( 2 ). a ( 3 ).

ช่วงค่าต่างๆ สามารถนำไปใช้ในส่วนเนื้อหาของกฎได้เช่นกัน โดยมีความหมายในลักษณะเดียวกัน

เงื่อนไขแบบตัวอักษรจะมีรูปแบบดังนี้:

p ( X ) : q ( X )

ถ้าส่วนขยายของqคือ{q(a1), q(a2), ..., q(aN)}เงื่อนไขข้างต้นจะมีความหมายเทียบเท่ากับการเขียน{p(a1), p(a2), ..., p(aN)}แทนที่เงื่อนไขนั้น ตัวอย่างเช่น

q ( 1..2 ). a :- 1 { p ( X ) : q ( X )}.

เป็นคำย่อสำหรับ

q ( 1 ). q ( 2 ). a :- 1 { p ( 1 ), p ( 2 )}.

การสร้างแบบจำลองที่เสถียร

ในการค้นหาโมเดลที่เสถียรของโปรแกรม Lparse ที่จัดเก็บไว้ในไฟล์${filename}เราใช้คำสั่ง

% lparse ${ filename } | smodels

ตัวเลือกที่ 0 สั่งให้ smodels ค้นหา โมเดลที่เสถียร ทั้งหมดของโปรแกรม ตัวอย่างเช่น หากไฟล์testมีกฎอยู่

1 { p , q , r } 2. s :- ไม่ใช่p .

จากนั้นคำสั่งจะสร้างผลลัพธ์ออกมา

% lparse test | smodels 0 คำตอบ: 1 โมเดลเสถียร: qp คำตอบ: 2 โมเดลเสถียร: p คำตอบ: 3 โมเดลเสถียร: rp คำตอบ: 4 โมเดลเสถียร: qs คำตอบ: 5 โมเดลเสถียร: rs คำตอบ: 6 โมเดลเสถียร: rqs

ตัวอย่างของโปรแกรม ASP

การระบายสีกราฟ

การระบายสีแบบ n - coloring ของกราฟคือฟังก์ชัน n- coloring ที่ทำให้สำหรับทุกคู่ของจุดยอดที่อยู่ติดกัน n-coloring = n-coloring เราต้องการใช้ ASP เพื่อหาการระบายสีแบบ n-coloring ของกราฟที่กำหนด (หรือตรวจสอบว่าไม่มีการระบายสีแบบ n-coloring ดังกล่าว) $n$ $G=\left\langle V,E\right\rangle$ $\mathrm {color} :V\to \{1,\dots ,n\}$ $\mathrm {color} (x)\neq \mathrm {color} (y)$ $(x,y)\in E$ $n$

สามารถดำเนินการนี้ได้โดยใช้โปรแกรม Lparse ดังต่อไปนี้:

c ( 1. . n ).1 { สี( X , I ) : c ( I )} 1 :- v ( X ).:- สี( X , I ), สี( Y , I ), e ( X , Y ), c ( I ).

บรรทัดที่ 1 กำหนดตัวเลขที่จะใช้เป็นสี ตามกฎการเลือกในบรรทัดที่ 2 แต่ละจุดยอดจะต้องกำหนด สีที่ไม่ซ้ำกัน ข้อจำกัดในบรรทัดที่ 3 ห้ามมิให้กำหนดสีเดียวกันให้กับจุดยอดหากมีเส้นเชื่อมระหว่างจุดยอดเหล่านั้น $1,\dots ,n$ $i$ $x$ $x$ $y$

หากเรานำไฟล์นี้ไปรวมกับคำจำกัดความของเช่น $G$

v ( 1..100 ). % 1,..., 100 เป็นจุดยอดe ( 1 , 55 ). % มีเส้นเชื่อมจาก 1 ไปยัง55 ...

จากนั้นเรียกใช้ smodels โดยระบุค่าตัวเลขในบรรทัดคำสั่ง แล้วอะตอมในรูปแบบในผลลัพธ์ของ smodels จะแสดงการระบายสีแบบ. $n$ $\mathrm {color} (\dots ,\dots )$ $n$ $G$

โปรแกรมในตัวอย่างนี้แสดงให้เห็นถึงโครงสร้างแบบ "สร้างและทดสอบ" ซึ่งมักพบได้ในโปรแกรม ASP แบบง่ายๆ กฎการเลือกอธิบายถึงชุดของ "คำตอบที่เป็นไปได้" ซึ่งเป็นซูเปอร์เซตอย่างง่ายของชุดคำตอบสำหรับปัญหาการค้นหาที่กำหนด ตามด้วยข้อจำกัดซึ่งจะกำจัดคำตอบที่เป็นไปได้ทั้งหมดที่ไม่เป็นที่ยอมรับ อย่างไรก็ตาม กระบวนการค้นหาที่ใช้โดย smodels และตัวแก้ปัญหาชุดคำตอบอื่นๆ ไม่ได้อาศัยการลองผิดลองถูก

กลุ่มใหญ่

กลุ่มจุดยอดที่อยู่ติดกันเป็นคู่ๆ ในกราฟเรียกว่า"คลิก" (clique ) โปรแกรม Lparse ต่อไปนี้จะค้นหาคลิกที่มีขนาด ในกราฟทิศทางที่กำหนด หรือตรวจสอบว่าไม่มีคลิกอยู่: $\geq n$

n { ใน( X ) : v ( X )}.:- ใน( X ), ใน( Y ), X ! = Y , ไม่ใช่e ( X , Y ).

นี่เป็นอีกตัวอย่างหนึ่งของการจัดระเบียบแบบสร้างและทดสอบ กฎการเลือกในบรรทัดที่ 1 "สร้าง" เซตทั้งหมดที่ประกอบด้วยจุดยอด ข้อจำกัดในบรรทัดที่ 2 "คัดกรอง" เซตที่ไม่ใช่คลิก $\geq n$

วงจรแฮมิลโทเนียน

วงจรแฮมิลโท เนียน ในกราฟระบุ ทิศทาง คือวงจรที่ผ่านจุดยอดแต่ละจุดของกราฟเพียงครั้งเดียวเท่านั้น โปรแกรม Lparse ต่อไปนี้สามารถใช้เพื่อค้นหาวงจรแฮมิลโทเนียนในกราฟระบุทิศทางที่กำหนด หากมีอยู่ โดยเราสมมติว่า 0 เป็นหนึ่งในจุดยอด

{ ใน( X , Y )} :- e ( X , Y ).:- 2 { ใน( X , Y ) : e ( X , Y )}, v ( X ).:- 2 { ใน( X , Y ) : e ( X , Y )}, v ( Y ).r ( X ) :- ใน( 0 , X ), v ( X ).r ( Y ) :- r ( X ), in ( X , Y ), e ( X , Y ).:- ไม่ใช่r ( X ), v ( X ).

กฎการเลือกในบรรทัดที่ 1 "สร้าง" เซตย่อยทั้งหมดของเซตของขอบ ข้อจำกัดทั้งสามข้อ "คัดกรอง" เซตย่อยที่ไม่ใช่วัฏจักรแฮมิลตัน ข้อจำกัดข้อสุดท้ายใช้述语เสริม(" สามารถเข้าถึงได้จาก 0") เพื่อห้ามจุดยอดที่ไม่ตรงตามเงื่อนไขนี้ 述语นี้ถูกกำหนดแบบเรียกซ้ำในบรรทัดที่ 6 และ 7 $r(x)$ $x$

โปรแกรมนี้เป็นตัวอย่างของโครงสร้าง "สร้าง กำหนด และทดสอบ" ที่ครอบคลุมมากขึ้น โดยประกอบด้วยการกำหนดเงื่อนไขเสริมที่ช่วยให้เรากำจัดวิธีแก้ปัญหาที่เป็นไปได้ "ที่ไม่ดี" ทั้งหมด

การวิเคราะห์ความสัมพันธ์ทางไวยากรณ์

ในการประมวลผลภาษาธรรมชาติ การแยกวิเคราะห์ตามความสัมพันธ์สามารถกำหนดเป็นปัญหา ASP ได้^{[ 13 ]} โค้ดต่อไปนี้แยกวิเคราะห์ประโยคภาษาละติน "Puella pulchra in villa linguam latinam discit" ซึ่งแปลว่า "หญิงสาวสวยกำลังเรียนภาษาละตินในวิลล่า" โครงสร้างต้นไม้ไวยากรณ์แสดงโดยส่วนโค้งของคำกริยาซึ่งแสดงถึงความสัมพันธ์ระหว่างคำในประโยค โครงสร้างที่คำนวณได้เป็นต้นไม้รากที่มีลำดับเชิงเส้น

% ********** ประโยคอินพุต ********** คำ( 1 , puella ) คำ( 2 , ปุชรา). คำ( 3 , ใน) คำ( 4 , วิลล่า) คำ( 5 , ภาษาศาสตร์) คำ( 6 , ละติน) คำ( 7 , แผ่นดิสก์) % ********** พจนานุกรม ******** 1 { โหนด( X , attr ( pulcher , a , fem , nom , sg )); โหนด( X , attr ( pulcher , a , fem , abl , sg )) } 1 :- คำ( X , pulchra ) โหนด( X , attr ( latinus , a , fem , acc , sg )) :- คำ( X , latinam ) 1 { node ( X , attr ( puella , n , fem , nom , sg )); node ( X , attr ( puella , n , fem , abl , sg )) } 1 :- word ( X , puella ). 1 { node ( X , attr ( villa , n , fem , nom , sg )); node ( X , attr ( villa , n , fem , abl , sg )) } 1 :- word ( X, villa ). node ( X , attr ( linguam , n , fem , acc , sg )) :- word ( X , linguam ). node ( X , attr ( discere , v , pres , 3 , sg )) :- word ( X , discit ). node ( X , attr ( in , p )) :- word ( X , in ). % ********** กฎไวยากรณ์ ********** 0 { arc ( X , Y , subj ) } 1 :- node ( X , attr ( _ , v , _ , 3 , sg )), node ( Y , attr ( _ , n , _ , nom , sg )). 0 { arc ( X , Y , dobj ) } 1 :- node ( X , attr ( _ , v , _ , 3 , sg )), node ( Y , attr ( _ , n , _ , acc , sg )). 0 { arc ( X , Y , attr ) } 1 :- node ( X , attr ( _ , n , Gender , Case , Number )), node ( Y , attr ( _ , a , Gender , Case, Number )). 0 { arc ( X , Y , prep ) } 1 :- node ( X , attr ( _ , p )), node ( Y , attr ( _ , n , _ , abl , _ )), X < Y . 0 { arc ( X , Y , adv ) } 1 :- node ( X , attr ( _ , v , _ , _ , _ )), node ( Y , attr ( _ , p )), not leaf ( Y ). % ********** รับประกันความเป็นต้นไม้ของกราฟ ********** 1 { root ( X ) : node ( X , _ ) } 1. :- arc ( X , Z , _ ), arc ( Y , Z , _ ), X ! = Y . :- arc ( X , Y , L1 ), arc ( X , Y , L2 ), L1 ! = L2 . path ( X , Y ) :- arc ( X , Y , _ ). path ( X , Z ) :- arc ( X , Y , _ ), path ( Y , Z ). :- path ( X , X ). :- root ( X ), node ( Y, _ ), X ! = Y , ไม่ใช่path ( X , Y ). leaf ( X ) :- node ( X , _ ), ไม่ใช่arc ( X , _ , _ ).

การกำหนดมาตรฐานภาษาและการแข่งขัน ASP

กลุ่มทำงานมาตรฐาน ASP ได้สร้างข้อกำหนดภาษามาตรฐานที่เรียกว่า ASP-Core-2 ^{[ 14 ]}ซึ่งระบบ ASP รุ่นล่าสุดกำลังมุ่งไปสู่ ASP-Core-2 เป็นภาษาอ้างอิงสำหรับการแข่งขัน Answer Set Programming Competition ซึ่งตัวแก้ปัญหา ASP จะได้รับการทดสอบประสิทธิภาพเป็นระยะๆ กับปัญหาอ้างอิงจำนวนหนึ่ง

การเปรียบเทียบการนำไปใช้งาน

ระบบรุ่นแรกๆ เช่น smodels ใช้การย้อนกลับ (backtracking)เพื่อหาคำตอบ เมื่อทฤษฎีและการใช้งานจริงของตัวแก้ปัญหา Boolean SATพัฒนาขึ้น ตัวแก้ปัญหา ASP จำนวนมากจึงถูกสร้างขึ้นบนพื้นฐานของตัวแก้ปัญหา SAT รวมถึง ASSAT และ Cmodels ระบบเหล่านี้แปลงสูตร ASP เป็นข้อเสนอ SAT ใช้ตัวแก้ปัญหา SAT แล้วแปลงคำตอบกลับไปเป็นรูปแบบ ASP อีกครั้ง ระบบรุ่นใหม่กว่า เช่น Clasp ใช้แนวทางแบบผสมผสาน โดยใช้อัลกอริธึมที่ขับเคลื่อนด้วยความขัดแย้งซึ่งได้รับแรงบันดาลใจจาก SAT โดยไม่ต้องแปลงเป็นรูปแบบตรรกะบูลีนทั้งหมด แนวทางเหล่านี้ช่วยให้ประสิทธิภาพดีขึ้นอย่างมาก บ่อยครั้งที่ดีขึ้นหลายเท่าตัว เมื่อเทียบกับอัลกอริธึมการย้อนกลับแบบเดิม

โครงการPotasscoทำหน้าที่เป็นเหมือนร่มสำหรับระบบต่างๆ มากมายที่กล่าวถึงด้านล่าง รวมถึงclasp , ระบบการต่อสายดิน ( gringo ), ระบบเพิ่มทีละขั้น ( iclingo ), ตัวแก้ข้อจำกัด ( clingcon ), คอมไพเลอร์ ภาษาแอ็กชันไปยัง ASP ( coala ), การใช้งานอินเทอร์ เฟซการส่งข้อความ แบบกระจาย ( claspar ) และอื่นๆ อีกมากมาย

ระบบส่วนใหญ่รองรับตัวแปร แต่โดยอ้อมเท่านั้น โดยการบังคับให้มีการต่อสายดิน โดยใช้ระบบต่อสายดิน เช่นLparseหรือgringoเป็นส่วนหน้า ความจำเป็นในการต่อสายดินอาจทำให้เกิดการระเบิดของเงื่อนไขเชิงการจัดเรียง ดังนั้น ระบบที่ทำการต่อสายดินแบบทันทีทันใดอาจมีข้อได้เปรียบ^{[ 15 ]}

การใช้งานการเขียนโปรแกรมชุดคำตอบที่ขับเคลื่อนด้วยคำถาม เช่น ระบบ Galliwasp ^{[ 16 ]}และ s(CASP) ^{[ 17 ]}หลีกเลี่ยงการกำหนดขอบเขตโดยสิ้นเชิงโดยใช้การรวมกันของการแก้ปัญหาและการเหนี่ยวนำร่วม

แพลตฟอร์ม			คุณสมบัติ					กลศาสตร์
ชื่อ	โอเอส	ใบอนุญาต	ตัวแปร	สัญลักษณ์ฟังก์ชัน	ชุดที่ระบุชัดเจน	รายการที่ชัดเจน	การสนับสนุนแบบแยก (กฎการเลือก)
ASPeRiX ถูกเก็บถาวรเมื่อวันที่ 8 พฤศจิกายน 2016 ที่Wayback Machine	ลินุกซ์	จีพีแอล	ใช่				เลขที่	การต่อลงดินแบบทันทีทันใด
อัสซัต	โซลาริส	ซอฟต์แวร์ฟรี						อิงตาม SAT-solver
ตัวแก้ชุดคำตอบ Clasp	ลินุกซ์ , มอสซาเรลล่า , วินโดวส์	ใบอนุญาต MIT	ใช่ ในภาษาคลิงโก	ใช่	เลขที่	เลขที่	ใช่	ค่อยเป็นค่อยไป ได้แรงบันดาลใจจากโปรแกรมแก้ปัญหา SAT (ไม่ดี ขับเคลื่อนด้วยความขัดแย้ง)
ซีโมเดลส์	ลินุกซ์ , โซลาริส	จีพีแอล	ต้องต่อสายดิน				ใช่	ค่อยเป็นค่อยไป ได้แรงบันดาลใจจากโปรแกรมแก้ปัญหา SAT (ไม่ดี ขับเคลื่อนด้วยความขัดแย้ง)
ดิฟ-เอสเอที	ลินุกซ์ , มอสซาเรลล่า , วินโดวส์ ( เครื่องเสมือนจาวา )	ใบอนุญาต MIT	ต้องต่อสายดิน				ใช่	ได้รับแรงบันดาลใจจากโปรแกรมแก้ปัญหาข้อสอบ SAT (ไม่ดี เน้นความขัดแย้ง) รองรับการแก้ปัญหาเชิงความน่าจะเป็นและการสุ่มตัวอย่างชุดคำตอบ
ดีแอลวี	ลินุกซ์ , มอสซาเรลล่า , วินโดวส์^{[ 18 ]}	ใช้งานได้ฟรีสำหรับการใช้งานทางวิชาการและการศึกษาที่ไม่ใช่เชิงพาณิชย์ และสำหรับองค์กรไม่แสวงหาผลกำไร^{[ 18 ]}	ใช่	ใช่	เลขที่	เลขที่	ใช่	ไม่รองรับ Lparse
DLV-คอมเพล็กซ์	ลินุกซ์ , มอสซาเรลล่า , วินโดวส์	จีพีแอล		ใช่	ใช่	ใช่	ใช่	สร้างขึ้นบนพื้นฐานของDLV — ไม่รองรับ Lparse
จีเอ็นที	ลินุกซ์	จีพีแอล	ต้องต่อสายดิน				ใช่	สร้างขึ้นบนพื้นฐานของโมเดล
nomore++	ลินุกซ์	จีพีแอล						การผสมผสานระหว่างความหมายตรงตัวและตามกฎเกณฑ์
ตุ่นปากเป็ด	ลินุกซ์ , โซลาริส , วินโดวส์	จีพีแอล						กระจาย, มัลติเธรด nomore++, smodels
พีบีโมเดลส์	ลินุกซ์	?						ตัวแก้ปัญหา แบบบูลีนเทียม
โมเดลส์	ลินุกซ์ , มอสซาเรลล่า , วินโดวส์	จีพีแอล	ต้องต่อสายดิน	เลขที่	เลขที่	เลขที่	เลขที่
Smodels-cc ถูกเก็บถาวรเมื่อวันที่ 15 พฤศจิกายน 2015 ที่Wayback Machine	ลินุกซ์	?	ต้องต่อสายดิน					อิงตาม SAT-solver; smodels พร้อมเงื่อนไขความขัดแย้ง
จีบ	ลินุกซ์	?						อิงตาม SAT-solver

ดูเพิ่มเติม

ลิงก์ภายนอก

ข้อกำหนดภาษาอินพุต ASP-Core-2 2.03c
การแข่งขันระบบ ASP ครั้งแรก
การแข่งขัน ASP ครั้งที่สอง
การแข่งขัน ASP ครั้งที่สาม
การแข่งขัน ASP ครั้งที่สี่
ตุ่นปากเป็ด
มีโปรแกรมแก้ชุดคำตอบหลากหลายรูปแบบสำหรับ Debian / Ubuntu
ตัวแก้ชุดคำตอบ Clasp

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

10 ] ปัจจุบัน

[

[

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]