채프 알고리즘

Chaff algorithm

Chaff는 프로그래밍에서 부울 만족도 문제를 해결하기 위한 알고리즘이다. 그것은 미국 프린스턴 대학의 연구자들에 의해 디자인되었다. 알고리즘은 DPLL 알고리즘의 한 예로서 효율적인 구현을 위해 여러 가지 개선사항이 있다.

구현

소프트웨어에서 이용 가능한 알고리즘의 구현으로는 mChaff와 zChaff가 있는데, 후자는 가장 널리 알려지고 사용되는 것이다. zChaff는 원래 현재 마이크로소프트[clarify] Research에서 일하고 있는 린타오 장 박사에 의해 쓰여졌고, 따라서 "z"가 되었다. 현재 프린스턴 대학교의 연구자들에 의해 유지되고 있으며 Linux에서 소스 코드와 바이너리 다로 다운로드 받을 수 있다. zChaff는 비상업적으로 무료로 사용할 수 있다.

참조

  • M. 모스케위츠, C. 마디건, Y. 자오, L. 장, S. 말릭. Chaff: Engineering a Efficient SAT Solver, 제39회 DAC(Design Automation Conference, DAC 2001), ACM, 라스베이거스 2001.
  • Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11). doi:10.1109/JPROC.2015.2455034.

외부 링크