Алгоритм Чаффа
 | Эта статья включает список литературы , связанную литературу или внешние ссылки , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . ( Июль 2017 г. ) |
Chaff — это алгоритм решения задач булевой выполнимости в программировании. Его разработали исследователи из Принстонского университета . Алгоритм представляет собой экземпляр алгоритма DPLL с рядом улучшений для эффективной реализации.
Реализации
[ редактировать ]Некоторые доступные реализации алгоритма в программном обеспечении: mChaff и zChaff, причем последний является наиболее широко известным и используемым. zChaff изначально был написан доктором Линтао Чжаном, сейчас [ объяснить ] в Microsoft Research , отсюда и буква «z». В настоящее время он поддерживается исследователями из Принстонского университета и доступен для загрузки как в виде исходного кода, так и в виде двоичных файлов для Linux . zChaff бесплатен для некоммерческого использования.
Ссылки
[ редактировать ]- М. Москевич, К. Мэдиган, Ю. Чжао, Л. Чжан, С. Малик. Чафф: Разработка эффективного решателя SAT , 39-я конференция по автоматизации проектирования (DAC 2001), Лас-Вегас, ACM 2001.
- Визель, Ю.; Вайсенбахер, Г.; Малик, С. (2015). «Решатели логической выполнимости и их применение при проверке моделей». Труды IEEE . 103 (11): 2021–2035. дои : 10.1109/JPROC.2015.2455034 . S2CID 10190144 .
Внешние ссылки
[ редактировать ] | Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |