기관회원 [로그인]
소속기관에서 받은 아이디, 비밀번호를 입력해 주세요.
개인회원 [로그인]

비회원 구매시 입력하신 핸드폰번호를 입력해 주세요.
본인 인증 후 구매내역을 확인하실 수 있습니다.

회원가입
서지반출
이진 변수 기수 조건을 위한 CNF 변환 방법의 분석
[STEP1]서지반출 형식 선택
파일형식
@
서지도구
SNS
기타
[STEP2]서지반출 정보 선택
  • 제목
  • URL
돌아가기
확인
취소
  • 이진 변수 기수 조건을 위한 CNF 변환 방법의 분석
저자명
이민,권기현,Lee. Min,Kwon. Gi-Hwon
간행물명
정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용
권/호정보
2008년|35권 2호|pp.81-90 (10 pages)
발행정보
한국정보과학회
파일정보
정기간행물|
PDF텍스트
주제분야
기타
이 논문은 한국과학기술정보연구원과 논문 연계를 통해 무료로 제공되는 원문입니다.
서지반출

기타언어초록

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