Finding Efficient Circuits Using SAT-Solvers

被引：0
|
作者：
Kojevnikov, Arist
Kulikov, Alexander S.
Yaroslavtsev, Grigory
机构：
来源：
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2009, PROCEEDINGS | 2009年 / 5584卷
关键词：
BOOLEAN FUNCTIONS; COMBINATIONAL COMPLEXITY; LOWER BOUNDS;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we report preliminary results of experiments with finding efficient circuits (over binary bases) using SAT-solvers. We present upper bounds for functions with constant number of inputs as well as general upper bounds that were found automatically. We focus mainly on MOD-functions. Besides theoretical interest, these functions are also interesting from a practical point of view as they are the core of the residue number system. In particular, we present, a circuit of size 3n + c over the full binary basis computing MOD(3)(n).
引用
收藏
页码：32 / 44
页数：13
相关论文
共 50 条
  • [21] Attacking Bivium using SAT solvers
    Eibach, Tobias
    Pilz, Enrico
    Voelkel, Gunnar
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2008, PROCEEDINGS, 2008, 4996 : 63 - 76
  • [22] Improving system level design space exploration by incorporating SAT-solvers into multi-objective evolutionary algorithms
    Schlichter, Thomas
    Lukasiewycz, Martin
    Haubelt, Christian
    Teich, Juergen
    [J]. IEEE COMPUTER SOCIETY ANNUAL SYMPOSIUM ON VLSI, PROCEEDINGS: EMERGING VLSI TECHNOLOGIES AND ARCHITECTURES, 2006, : 309 - +
  • [23] Efficient data structures for backtrack search SAT solvers
    Inês Lynce
    João Marques-Silva
    [J]. Annals of Mathematics and Artificial Intelligence, 2005, 43 : 137 - 152
  • [24] Building efficient decision procedures on top of SAT solvers
    Cimatti, Alessandro
    Sebastiani, Roberto
    [J]. FORMAL METHODS FOR HARDWARE VERIFICATION, 2006, 3965 : 144 - 175
  • [25] Efficient data structures for backtrack search SAT solvers
    Lynce, I
    Marques-Silva, J
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2005, 43 (1-4) : 137 - 152
  • [26] Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers
    Banbara, Mutsunori
    Matsunaka, Haruki
    Tamura, Naoyuki
    Inoue, Katsumi
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 112 - +
  • [27] Efficient Model Checking Timed and Weighted Interpreted Systems Using SMT and SAT Solvers
    Zbrzezny, Agnieszka M.
    Zbrzezny, Andrzej
    Raimondi, Franco
    [J]. AGENT AND MULTI-AGENT SYSTEMS: TECHNOLOGY AND APPLICATIONS, KES-AMSTA 2016, 2016, 58 : 45 - 55
  • [28] Strategies on Algebraic Attacks Using SAT Solvers
    Chen, Baiqiang
    [J]. PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE FOR YOUNG COMPUTER SCIENTISTS, VOLS 1-5, 2008, : 2204 - 2209
  • [29] Exact DFA Identification Using SAT Solvers
    Heule, Marijn J. H.
    Verwer, Sicco
    [J]. GRAMMATICAL INFERENCE: THEORETICAL RESULTS AND APPLICATIONS, ICGI 2010, 2010, 6339 : 66 - 79
  • [30] On the Parallelization of SAT Solvers
    Abd El Khalek, Yasmeen
    Safar, Mona
    El-Kharashi, M. Watheq
    [J]. 2015 TENTH INTERNATIONAL CONFERENCE ON COMPUTER ENGINEERING & SYSTEMS (ICCES), 2015, : 119 - 128
12345