본문 바로가기
HOME> 논문 > 논문 검색상세

논문 상세정보

이진 변수 기수 조건을 위한 CNF 변환 방법의 분석
Comparative Analysis on CNF Encodings for Boolean Cardinality Constraints

이민   (경기대학교 컴퓨터과학과UU0000066  ); 권기현   (경기대학교 컴퓨터과학과UU0000066  );
  • 초록

    이진 변수의 기수 조건이란 여러 이진 변수 중에서 하나를 선택하는 것이다. 이러한 조건을 줄여서 BCC(Boolean Cardinality Constraint)라고 부른다. BCC는 소프트웨어 공학을 비롯해서 전산학의 다양한 분야에서 널리 사용되고 있다. 그래서 BCC를 CNF로 변환하는 효율적인 방법이 많이 연구되었다. 본 논문에서는 지금까지 제시된 변환 방법을 효율성과 유연성 측면에서 분석한다. 뿐만 아니라 이해하기 어려운 것으로 잘 알려진 CNF 절을 시각화하여 숨겨진 구조를 드러냄으로서 기존 분석과 차별화를 하였다. 분석 결과를 확인하기 위해서 다양한 비둘기-집 문제에 적용하였다. 그 결과 BCC를 다루는데 있어서 커멘더 변환 방법이 다른 방법보다 우수하였다.


    BCC(Boolean Cardinality Constraint) is to select one boolean variable from n different variables. It is widely used in many areas including software engineering. Thus, many efficient encoding techniques of BCC into CNF have been studied extensively In this paper we analyze some representative encodings with respect to flexibility as well as efficiency. In addition we use a visualization tool to draw the CNF clauses generated from each encodings. Visualizing the clauses exposes a hidden structure in encodings and makes to compare each encodings on the structure level, which is one of the prominent achievement in our work compared to other works. And we apply our analysis on the pigeon-hole problems to have confidence. In our experimental settings, the commander encoding shows the best performance.


  • 주제어

    만족성 문제 .   CNF 변환 .   시각화 .   변환 기준.  

  • 참고문헌 (20)

    1. M. Huth and M. Ryan, Logic in Computer Science, Cambridge university Press, 2004 
    2. 권기현, 'SAT 처리기를 위한 수도쿠 퍼즐의 최적화된 인코딩', 정보과학회논문지: 소프트웨어 및 응용, 정보과학회, 제34권 제7호, pp. 616-624, 2007     
    3. I. Lynce and J. Ouaknine, 'Sudoku as a SAT problem,' in The Proceedings of AIMATH, 2006 
    4. Will Klieber and G. Kwon, 'Efficient CNF Encoding for Selecting 1 from N Objects,' in Proceedings of CFV'07, 2007 
    5. Alloy tool (웹 사이트 http://alloy.mit.edu/) 
    6. From http://www.satlib.org/Benchmarks/SAT/satformat.ps 
    7. C. Sinz, 'Towards an Optimal CNF Encoding of Boolean Cardinality Constraints,' in Proceedings of CP 2005, pp. 827-831, 2005 
    8. C. Sinz and E.M. Dieringer, 'DPvis - a Tool to Visualize Structured SAT Instances,' in Proceedings of SAT 2005, pp. 257-268, 2005 
    9. T. Latvala, A. Biere, K.Heljanko, and T. Junttila, 'Simple Bounded LTL Model Checking,' in Proceedings of FMCAD'2004, pp. 186-200, 2004 
    10. M. Davis, G. Logemann and D. Loveland, 'A Machine Program for Theorem Proving,' Communications of the ACM 5 (7): 394-397, 1962 
    11. F.A. Aloul, K.A. Sakallah, and I.L. Markov, 'Efficient Symmetry Breaking for Boolean Satisfiability,' IEEE Transactions on Computer, Vol.55, No.5, pp. 549-558, 2006 
    12. M.N. Velev, 'Tuning SAT for Formal Verification and Testing,' Journal of Universal Computer Science Vol.10, Issue 12, pp. 1559-1561, 2006 
    13. J.P. Silva and K.A. Sakallah, 'GRAPS: A Search Algorithm for Propositional Satisfiability,' IEEE Trans. Computers, Vol.48, No.5, pp. 506-521, 1999 
    14. F. Ivancic, et.al., 'F-Soft: Software Verification Platform,' in Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005 
    15. J.P. Warners, 'A Linear-time Transformation of Linear Inequalities into Conjunctive Normal Form,' Information Processing Letter, Vol.68, pp. 63-69, 1998 
    16. M. Sheeran and G. Stalmarck, 'A Tutorial on Stalmarck's Proof Procedure for Propositional Logic,' in Proceedings of FMCAD'98, pp. 82-99, 1998 
    17. M.W. Moskewicz, et.al., 'Chaff: Engineering an Efficient SAT Solver,' in Proceedings of DAC'01. 2001 
    18. N. Een and N. Sorensson, 'An Extensible SAT Solver,' in Proceedings of SAT'03, 2003 
    19. O. Baileux and Y. Boufkhad, 'Efficient CNF Encoding of Boolean Cardinality Constraints,' in Proceedings of CP 2003, pp. 108-122, 2003 
    20. I. Lynce and J.P. Silva, 'Efficient data structures for backtrack search SAT solvers,' Journal of Annual Mathematics Artificial Intelligence, Vol.43, No.1, pp. 137-152, 2005 

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

무료다운로드
  • NDSL :
유료다운로드

유료 다운로드의 경우 해당 사이트의 정책에 따라 신규 회원가입, 로그인, 유료 구매 등이 필요할 수 있습니다. 해당 사이트에서 발생하는 귀하의 모든 정보활동은 NDSL의 서비스 정책과 무관합니다.

원문복사신청을 하시면, 일부 해외 인쇄학술지의 경우 외국학술지지원센터(FRIC)에서
무료 원문복사 서비스를 제공합니다.

NDSL에서는 해당 원문을 복사서비스하고 있습니다. 위의 원문복사신청 또는 장바구니 담기를 통하여 원문복사서비스 이용이 가능합니다.

이 논문과 함께 출판된 논문 + 더보기