Art

J-GLOBAL ID：201702217872150046   Reference number：17A1224569

An Approach for Solving SAT/MaxSAT-Encoded Formal Verification Problems on FPGA

FPGAのSAT/MaxSAT符号化した形式検証問題を解くための手法

Author (2)： KANAZAWA Kenji (Division of Information Engineering, Faculty of Engineering, Information and Systems, University of Tsukuba) ,  MARUYAMA Tsutomu (Division of Intelligent Interaction Technologies, Faculty of Engineering, Information and Systems, University of Tsukuba)
Material： IEICE Transactions on Information and Systems (Web)  (IEICE Trans Inf Syst (Web))
Volume： E100.D  Issue： 8  Page： 1807-1818(J-STAGE)  Publication year： 2017 
JST Material Number： U0469A  ISSN： 1745-1361  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： ENGLISH (EN)

Thesaurus term： *FPGA ,  *coding(signal) ,  satisfiability problem ,  local search method ,  digital circuit ,  heuristics ,  burst ,  DRAM
Semi thesaurus term： instance ,  heuristic ,  Boolean satisfiability ,  *formal verification ,  concurrency

Author keywords (4)： FPGA ,  SAT ,  MaxSAT ,  WalkSAT

JST classification (1)： Computer system operational management  (JD02020C)

Reference (25)：

• [1] B. Selman, H. Kautz, and B. Cohen, “Noise Strategies for Improving Local Search,” AAAI-94, pp.337-343, 1994.
• [2] D. McAllester, B. Selman, and H. Kautz, “Evidence for invariants in local search,” AAAI-97, pp.321-326, 1997. 10.1090/dimacs/026/25
• [3] H.H. Hoos, “An adaptive noise mechanism for WalkSAT,” AAAI-02, pp.655-660, 2002.
• [4] F. Hutter, D.A.D. Tompkins, and H.H. Hoos, “Scaling and probabilistic smoothing: Efficient dynamic local search for SAT,” CP-02, vol.2470, pp.233-248, 2002. 10.1007/3-540-46135-3_16
• [5] C.M. Li, W. Wei, and H. Zhang, “Combining adaptive noise and look-ahead in local search for SAT,” SAT-07, pp.121-133, 2007.

Terms in the title (4)： FPGA ,  SAT ,  形式検証 ,  手法