Extracting Subsequence of Boolean Variables using SAT-solver


The KIPS Transactions:PartD, Vol. 15, No. 6, pp. 777-784, Dec. 2008
10.3745/KIPSTD.2008.15.6.777,   PDF Download:

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 k from a sequence of Boolean variables, into CNF formulas. Through experimental results, we show that our method is more efficient than using only BCC.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
S. C. Park and G. H. Kwon, "Extracting Subsequence of Boolean Variables using SAT-solver," The KIPS Transactions:PartD, vol. 15, no. 6, pp. 777-784, 2008. DOI: 10.3745/KIPSTD.2008.15.6.777.

[ACM Style]
Sa Choun Park and Gi Hwon Kwon. 2008. Extracting Subsequence of Boolean Variables using SAT-solver. The KIPS Transactions:PartD, 15, 6, (2008), 777-784. DOI: 10.3745/KIPSTD.2008.15.6.777.