만족가능성 처리기를 이용한 이진 변수 서브시퀀스 추출
Extracting Subsequence of Boolean Variables using SAT-solver
0
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
최근 정형 검증 분야에서 상태 폭발 문제를 극복하기 위해 만족가능성(Satisfiability) 처리기를 사용하는 방법이 많이 연구되고 있다. 만족가능성 처리기를 사용하려면 대상을 CNF 식으로 변환해야 하는데, 이진 기수 제약 조건은 시스템을 CNF 식으로 변환하기 위해 많이 사용되는 기법이다. 그러나 이진 기수 제약 조건은 이진 변수들의 집합을 다루기 때문에 이진 변수들의 순서 정보는 변환할 수 없었다. 본 논문에서는 이진 변수의 시퀀스에서 길이가 인 서브시퀀스 추출 문제에 대한 CNF 변환 방법을 제안한다. 또한 실험을 통해 제안된 방법이 순서정보를 고려치 않고 적용한 변환 방법보다 훨씬 더 좋은 결과를 얻을 수 있었다.
Abstract
Recently in the field of model checking, to overcome the state explosion problem, the method of using a SAT-solver is mainly researched. To use a SAT-solver, the system to be verified is translated into CNF and the Boolean cardinality constraint is widely used in translating the system into CNF. In BCC it is dealt with set of boolean variables, but there is no translating method of the sequence among Boolean variables. In this paper, we propose methods for translating the problem, which is extracting a subsequence with length from a sequence of Boolean variables, into CNF formulas. Through experimental results, we show that our method is more efficient than using only BCC.
참고문헌 (14)
- E. M. Clarke, "Model Checking" (1999), MIT Press
- M. Davis, "A Machine Program for Theorem Proving", Communications of the ACM, 2(4), pp.394~397 (1962)
- Marques-Silva, J. P., "GRASP: A Search Algorithm for Propositional Satisfiability", IEEE Transactions on Computers, 48, pp.506~521 (1999)
- M.W. Moskewicz, "Chaff: Engineering an Efficient SAT Solver", In Proceedings of Design Automation Conference (2001)
- [URL]
- H. Kautz, "Planning as satisfiability", In Proceedings of the ECAI’92,, pp.359~363 (1992), John Wiley & Sons, Inc.
- A. Biere, "Bounded Model Checking" (2003), Advances in Computers
- T. Latvala, "Simple Is Better: Efficient Bounded Model Checking for Past LTL", in the Proceedings of VMCAI 2005, 통권 : 3385 (2005)
- G. Kwon, "Optimized CNF Encoding for Sudoku Puzzles", in The Proceedings of LPAR06 (2006)
- O.Bailleux, "Efficient CNF encoding of Boolean cardinality constraints", in Proceedings of the CP 2003,, 통권 : 2833 (2003)
- C. Sinz, "Towards an optimal CNF encoding of Boolean cardinality constraints", In Proceedings of the CP 2005, 통권 : 3709 (2005)
- K. J. Batenburg, "An evolutionary algorithm for discrete tomography" (2004), Discrete Applied Mathematics
- B. J. Batenburg, "A discrete tomography approach to Japanese puzzles", in Proceedings of the Belgian-Dutch Conf. Artificial Intelligence (2004)
- [URL]