SATIRE: A new incremental satisfiability engine

被引：0
|
作者：
Whittemore, J [1 ]
Kim, J [1 ]
Sakallah, K [1 ]
机构：
[1] Univ Michigan, Ann Arbor, MI 48109 USA
来源：
38TH DESIGN AUTOMATION CONFERENCE PROCEEDINGS 2001 | 2001年
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We introduce SATIRE, a new satisfiability solver that is particularly suited to verification and optimization problems in electronic design automation. SATIRE builds on the most recent advances in satisfiability research, and includes two new features to achieve even higher performance: a facility for incrementally solving sets of related problems, and the ability to handle non-CNF constraints. We provide experimental evidence showing the effectiveness of these additions to classical satisfiability solvers.
引用
收藏
页码：542 / 545
页数：4
相关论文
共 50 条
  • [41] New approach on solving 3-satisfiability
    Lect Notes Comput Sci, (197):
  • [42] New upper bounds for the problem of maximal satisfiability
    Kulikov, A. S.
    Kutskov, K.
    DISCRETE MATHEMATICS AND APPLICATIONS, 2009, 19 (02): : 155 - 172
  • [43] Analysis of a new reduction calculus for the satisfiability problem
    Noureddine, S.
    Mathematical Logic in Asia, 2006, : 166 - 174
  • [44] Caching Search Engine Results over Incremental Indices
    Blanco, Roi
    Bortnikov, Edward
    Junqueira, Flavio P.
    Lempel, Ronny
    Telloli, Luca
    Zaragoza, Hugo
    SIGIR 2010: PROCEEDINGS OF THE 33RD ANNUAL INTERNATIONAL ACM SIGIR CONFERENCE ON RESEARCH DEVELOPMENT IN INFORMATION RETRIEVAL, 2010, : 82 - 89
  • [45] Incremental Linearization: A practical approach to Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions (Invited Paper)
    Cimatti, Alessandro
    Griggio, Alberto
    Irfan, Ahmed
    Roveri, Marco
    Sebastiani, Roberto
    2018 20TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2018), 2019, : 19 - 26
  • [46] Modelling the 3-coloring of Serial-Parallel Graphs via Incremental Satisfiability.
    Lopez-Ramirez, C.
    De Ita, G.
    IEEE LATIN AMERICA TRANSACTIONS, 2019, 17 (04) : 607 - 614
  • [47] Muddling through in innovation - On incremental failure in developing an engine
    Rehn, Alf
    Lindahl, Marcus
    JOURNAL OF BUSINESS RESEARCH, 2012, 65 (06) : 807 - 813
  • [48] Reasoning and inference for (Maximum) satisfiability: new insights
    Mohamed Sami Cherif
    Constraints, 2023, 28 : 513 - 514
  • [49] NEW ENGINE, NEW ENGINE PLANT FOR CATERPILLAR
    OSENGA, M
    DIESEL PROGRESS ENGINES & DRIVES, 1995, 61 (01): : 32 - &
  • [50] SATIRE AND SYMPATHY - A NEW WAVE OF YUGOSLAVIAN FILMMAKERS
    HORTON, A
    CINEASTE, 1981, 11 (02): : 18 - 22
12345