Extracting Subsequence of Boolean Variables using SAT-solver 


Vol. 15,  No. 6, pp. 777-784, Dec.  2008
10.3745/KIPSTD.2008.15.6.777


PDF
  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
  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.

Forms

Search
(IN TITLE, AUTHOR, ABSTRACT,KEYWORDS)

Advanced Search ▼

POPULAR KEYWORDS
(TOP 10 KEYWORDS)

Recent Publications
(LAST 3 YEARS)

Old Journals

Indexing

All publications of TKIPS is indexed in DOI, EBSCO, Google Scholar, Crossref, and CrossCheck.

TKIPS is also selected as the Journal for Accreditation by NRF (National Research Foundation of Korea).

Related Journals