خوارزمية القشر

الموسوعة الحرة

Chaff هي خوارزمية لحل مسائل إرضاء المنطق البولياني في البرمجة. صممها باحثون في جامعة برينستون . تُعدّ هذه الخوارزمية نسخةً من خوارزمية DPLL مع عدد من التحسينات لضمان كفاءة التنفيذ.

التطبيقات

من بين التطبيقات البرمجية المتاحة للخوارزمية، نجد zChaff mChaffو zChaff zChaff، حيث يُعدّ الأخير الأكثر شهرةً واستخدامًا. كتب zChaff في الأصل الدكتور لينتاو تشانغ، ومن هنا جاء حرف "z". يتولى باحثون في جامعة برينستون صيانته حاليًا ، وهو متاح للتنزيل كشفرة مصدرية وملفات تنفيذية على نظام لينكس . zChaff مجاني للاستخدام غير التجاري.

مراجع

  • م. موسكيويتش، سي. مادجان، واي. تشاو، إل. تشانغ، إس. مالك. تشاف: هندسة حل فعال لمسألة إرضاء النظام ، المؤتمر التاسع والثلاثون لأتمتة التصميم (DAC 2001)، لاس فيغاس، ACM 2001.
  • فيزل، ي.؛ فايسنباخر، ج.؛ مالك، س. (2015). "حلول قابلية الإرضاء المنطقية وتطبيقاتها في التحقق من النماذج". وقائع معهد مهندسي الكهرباء والإلكترونيات . 103 (11): 2021-2035 . doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 .