Extending Multiple-Valued Clausal Forms with Linear Integer Arithmetic

被引：3
|
作者：
Ansotegui, Carlos [1 ]
Bofill, Miquel [2 ]
Manya, Felip [3 ]
Villaret, Mateu [2 ]
机构：
[1] Univ Lleida, Lleida, Spain
[2] Univ Girona, Girona, Spain
[3] CSIC, IIIA, Bellaterra, Spain
来源：
2011 41ST IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC (ISMVL) | 2011年
关键词：
D O I：
10.1109/ISMVL.2011.53
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We extend the language of signed many-valued clausal forms with linear integer arithmetic constraints. In this way, we get a simple modeling language in which a wide range of practical combinatorial problems admit compact and natural encodings. We then define efficient translations from our language into the SAT and SMT formalism, and propose to use SAT and SMT solvers for finding solutions.
引用
收藏
页码：230 / 235
页数：6
相关论文
共 50 条
  • [1] A Formal Approach to Designing Multiple-Valued Arithmetic Circuits
    Saito, Kazuya
    Homma, Naofumi
    Aoki, Takafumi
    [J]. JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2015, 24 (1-4) : 21 - 34
  • [2] Logical not polynomial forms to represent multiple-valued functions
    Zaitseva, EN
    Kalganova, TG
    Kochergov, EG
    [J]. 1996 26TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 1996, : 302 - 307
  • [3] Systematic Approach to Designing Multiple-Valued Arithmetic Circuits Based on Arithmetic Description Language
    Homma, Naofumi
    Watanabe, Yuki
    Degawa, Katsuhiko
    Aoki, Takafumi
    Higuchi, Tatsuo
    [J]. JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2009, 15 (04) : 329 - 340
  • [4] Residue arithmetic circuits based on the signed-digit multiple-valued arithmetic circuits
    Wei, SG
    Shimizu, K
    [J]. 1998 28TH IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC - PROCEEDINGS, 1998, : 276 - 281
  • [5] Design of multiple-valued arithmetic circuits using counter tree diagrams
    Homma, Naofumi
    Degawa, Katsuhiko
    Aoki, Takafumi
    Higuchi, Tatsuo
    [J]. JOURNAL OF MULTIPLE-VALUED LOGIC AND SOFT COMPUTING, 2007, 13 (4-6) : 487 - 502
  • [6] AN INTEGER-VALUED ARITHMETIC FUNCTION WITH NO INFINITE LINEAR SUBSET
    JUST, E
    SCHAUMBE.N
    LANGFORD, ES
    [J]. AMERICAN MATHEMATICAL MONTHLY, 1965, 72 (04): : 427 - &
  • [7] Systematic interpretation of redundant arithmetic adders in binary and multiple-valued logic
    Homma, Naofumi
    Aoki, Takafumi
    Higuchi, Tatsuo
    [J]. IEICE TRANSACTIONS ON ELECTRONICS, 2006, E89C (11): : 1645 - 1654
  • [8] Reconfigurable current-mode multiple-valued residue arithmetic circuits
    Shimabukuro, K
    Zukeran, C
    [J]. 1998 28TH IEEE INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC - PROCEEDINGS, 1998, : 282 - 287
  • [9] Synthesis of multiple-valued arithmetic circuits using Evolutionary Graph Generation
    Natsui, M
    Aoki, T
    Higuchi, T
    [J]. 31ST INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC, PROCEEDINGS, 2001, : 253 - 258
  • [10] Linear Problems of Optimal Control of Multiple-Valued Trajectories
    A. V. Plotnikov
    [J]. Cybernetics and Systems Analysis, 2002, 38 (5) : 772 - 782
12345