Алгоритм Chaff - Chaff algorithm

Chaff - это алгоритм для решения примеров проблемы логической выполнимости в программировании. Он был разработан исследователями из Принстонского университета , США. Алгоритм является экземпляром алгоритма DPLL с рядом улучшений для эффективной реализации.

Реализации

Некоторыми доступными реализациями алгоритма в программном обеспечении являются mChaff и zChaff , последний из которых является наиболее широко известным и используемым. zChaff был первоначально написан доктором Линтао Чжаном, ныне работающим в Microsoft Research , отсюда и буква «z». Сейчас он поддерживается исследователями из Принстонского университета и доступен для загрузки как исходный код, так и двоичные файлы в Linux . zChaff бесплатен для некоммерческого использования.

использованная литература

  • М. Москевич, К. Мадиган, Ю. Чжао, Л. Чжан, С. Малик. Чафф: Разработка эффективного SAT-решателя , 39-я конференция по автоматизации проектирования (DAC 2001), Лас-Вегас, ACM 2001.
  • Визель, Ю .; Weissenbacher, G .; Малик, С. (2015). "Решатели логической выполнимости и их приложения в проверке моделей". Труды IEEE . 103 (11). DOI : 10.1109 / JPROC.2015.2455034 .

внешние ссылки


Значок заглушки

Эта статья, посвященная формальным методам, является незавершенной . Вы можете помочь Википедии, расширив ее .