• 검색어에 아래의 연산자를 사용하시면 더 정확한 검색결과를 얻을 수 있습니다.
  • 검색연산자
검색연산자 기능 검색시 예
() 우선순위가 가장 높은 연산자 예1) (나노 (기계 | machine))
공백 두 개의 검색어(식)을 모두 포함하고 있는 문서 검색 예1) (나노 기계)
예2) 나노 장영실
| 두 개의 검색어(식) 중 하나 이상 포함하고 있는 문서 검색 예1) (줄기세포 | 면역)
예2) 줄기세포 | 장영실
! NOT 이후에 있는 검색어가 포함된 문서는 제외 예1) (황금 !백금)
예2) !image
* 검색어의 *란에 0개 이상의 임의의 문자가 포함된 문서 검색 예) semi*
"" 따옴표 내의 구문과 완전히 일치하는 문서만 검색 예) "Transform and Quantization"
쳇봇 이모티콘
ScienceON 챗봇입니다.
궁금한 것은 저에게 물어봐주세요.

논문 상세정보

이진 변수 기수 조건을 위한 CNF 변환 방법의 분석

Comparative Analysis on CNF Encodings for Boolean Cardinality Constraints


이진 변수의 기수 조건이란 여러 이진 변수 중에서 하나를 선택하는 것이다. 이러한 조건을 줄여서 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.

참고문헌 (20)

  1. 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 
  2. 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 
  3. N. Een and N. Sorensson, 'An Extensible SAT Solver,' in Proceedings of SAT'03, 2003 
  4. M.W. Moskewicz, et.al., 'Chaff: Engineering an Efficient SAT Solver,' in Proceedings of DAC'01. 2001 
  5. M.N. Velev, 'Tuning SAT for Formal Verification and Testing,' Journal of Universal Computer Science Vol.10, Issue 12, pp. 1559-1561, 2006 
  6. Alloy tool (웹 사이트 http://alloy.mit.edu/) 
  7. F. Ivancic, et.al., 'F-Soft: Software Verification Platform,' in Proceedings of the International Conference on Computer Aided Verification (CAV), July 2005 
  8. M. Huth and M. Ryan, Logic in Computer Science, Cambridge university Press, 2004 
  9. C. Sinz, 'Towards an Optimal CNF Encoding of Boolean Cardinality Constraints,' in Proceedings of CP 2005, pp. 827-831, 2005 
  10. 권기현, 'SAT 처리기를 위한 수도쿠 퍼즐의 최적화된 인코딩', 정보과학회논문지: 소프트웨어 및 응용, 정보과학회, 제34권 제7호, pp. 616-624, 2007 
  11. T. Latvala, A. Biere, K.Heljanko, and T. Junttila, 'Simple Bounded LTL Model Checking,' in Proceedings of FMCAD'2004, pp. 186-200, 2004 
  12. O. Baileux and Y. Boufkhad, 'Efficient CNF Encoding of Boolean Cardinality Constraints,' in Proceedings of CP 2003, pp. 108-122, 2003 
  13. Will Klieber and G. Kwon, 'Efficient CNF Encoding for Selecting 1 from N Objects,' in Proceedings of CFV'07, 2007 
  14. M. Davis, G. Logemann and D. Loveland, 'A Machine Program for Theorem Proving,' Communications of the ACM 5 (7): 394-397, 1962 
  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. I. Lynce and J. Ouaknine, 'Sudoku as a SAT problem,' in The Proceedings of AIMATH, 2006 
  17. M. Sheeran and G. Stalmarck, 'A Tutorial on Stalmarck's Proof Procedure for Propositional Logic,' in Proceedings of FMCAD'98, pp. 82-99, 1998 
  18. From http://www.satlib.org/Benchmarks/SAT/satformat.ps 
  19. C. Sinz and E.M. Dieringer, 'DPvis - a Tool to Visualize Structured SAT Instances,' in Proceedings of SAT 2005, pp. 257-268, 2005 
  20. 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 

이 논문을 인용한 문헌 (0)

  1. 이 논문을 인용한 문헌 없음


원문 PDF 다운로드

  • ScienceON :

원문 URL 링크

원문 PDF 파일 및 링크정보가 존재하지 않을 경우 KISTI DDS 시스템에서 제공하는 원문복사서비스를 사용할 수 있습니다. (원문복사서비스 안내 바로 가기)

상세조회 0건 원문조회 0건

DOI 인용 스타일