SAT-based analysis of cellular automata

被引：0
|
作者：
D'Antonio, M [1 ]
Delzanno, G [1 ]
机构：
[1] Univ Genoa, Dipartimento Informat & Sci Informaz, I-16146 Genoa, Italy
来源：
CELLULAR AUTOMATA, PROCEEDINGS | 2004年 / 3305卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In the last decade there has been a dramatic speed-up for algorithms solving the Satisfiability (SAT) problem for propositional formulas, a well known NP-complete problem. In this paper we will investigate the applicability of modern SAT solvers to the qualitative analysis of Cellular Automata. For this purpose we have defined an encoding of the evolution of Cellular Automata into formulas in propositional logic. The resulting formula can be used to test forward and inverse reachability problems for the original Cellular Automata in a modular way. In the paper we will report on experimental results obtained by applying the SAT-solver zChaff to reachability problems for classical examples of Cellular Automata like the Firing Squad Synchronization Problem.
引用
收藏
页码：745 / 754
页数：10
相关论文
共 50 条
  • [41] SAT-Based Methods for Circuit Synthesis
    Bloem, Roderick
    Egly, Uwe
    Klampfl, Patrick
    Koenighofer, Robert
    Lonsing, Florian
    [J]. 2014 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2014, : 31 - 34
  • [42] Logic as energy:: A SAT-Based approach
    Lima, Priscila M. V.
    Mariela, M.
    Morveli-Espinoza, M.
    Franca, Felipe M. G.
    [J]. ADVANCES IN BRAIN, VISION, AND ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2007, 4729 : 458 - +
  • [43] CryptoSAT: a tool for SAT-based cryptanalysis
    Lafitte, Frederic
    [J]. IET INFORMATION SECURITY, 2018, 12 (06) : 463 - 474
  • [44] SAT-Based Arithmetic Support for Alloy
    Cornejo, Cesar
    [J]. 2020 35TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2020), 2020, : 1161 - 1163
  • [45] Instance generation for SAT-based ATPG
    Tille, Daniel
    Fey, Goerschwin
    Drechsler, Rolf
    [J]. PROCEEDINGS OF THE 2007 IEEE WORKSHOP ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS, 2007, : 153 - +
  • [46] SAT-based sequential depth computation
    Mneimneh, M
    Sakallah, K
    [J]. ASP-DAC 2003: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2003, : 87 - 92
  • [47] SAT-Based Quantum Circuit Adaptation
    Brandhofer, Sebastian
    Kim, Jinwoong
    Niu, Siyuan
    Bronn, Nicholas T.
    [J]. 2023 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION, DATE, 2023,
  • [48] SAT-based lazy formal analysis method for security protocols
    Gu, Chun-Xiang
    Wang, Huan-Xiao
    Zheng, Yong-Hui
    Xin, Dan
    Liu, Nan
    [J]. Tongxin Xuebao/Journal on Communications, 2014, 35 (11): : 117 - 125
  • [49] A SAT-based preimage analysis of reduced KECCAK hash functions
    Morawiecki, Pawel
    Srebrny, Marian
    [J]. INFORMATION PROCESSING LETTERS, 2013, 113 (10-11) : 392 - 397
  • [50] A Dataflow Analysis to Improve SAT-Based Bounded Program Verification
    Cuervo Parrino, Bruno
    Pablo Galeotti, Juan
    Garbervetsky, Diego
    Frias, Marcelo F.
    [J]. SOFTWARE ENGINEERING AND FORMAL METHODS, 2011, 7041 : 138 - +
12345