A SAT solver using advanced reasoning

被引:0
|
作者
Ding, M [1 ]
Tang, P [1 ]
机构
[1] Fudan Univ, Microelect Dept, ASIC, Shanghai 200433, Peoples R China
关键词
D O I
10.1109/ICASIC.2003.1277519
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
This paper presents a SAT solver. The main purpose is to study the tradeoff between more reasoning and quicker decision. It shows that though good result can be obtained by quick decision and fast implementation. the reasoning step is still useful in several benchmarks. We choose FLD as our reasoning technique and discuss heuristic of obtaining the set of literals to be tested in FLD. Experiment results show that by careful implementation. this old technique still can be used in a fast SAT solver.
引用
收藏
页码:183 / 186
页数:4
相关论文
共 50 条
  • [31] Automated Reasoning with Epistemic Graphs Using SAT Solvers
    Hunter, Anthony
    COMPUTATIONAL MODELS OF ARGUMENT, COMMA 2022, 2022, 353 : 176 - 187
  • [32] Bounded model checking of Time Petri Nets using SAT solver
    Yokogawa, Tomoyuki
    Kondo, Masafumi
    Miyazaki, Hisashi
    Amasaki, Sousuke
    Sato, Yoichiro
    Arimoto, Kazutami
    IEICE ELECTRONICS EXPRESS, 2015, 12 (02):
  • [33] An AIG-Based QBF-Solver Using SAT for Preprocessing
    Pigorsch, Florian
    Scholl, Christoph
    PROCEEDINGS OF THE 47TH DESIGN AUTOMATION CONFERENCE, 2010, : 170 - 175
  • [34] Chaff: Engineering an efficient SAT solver
    Moskewicz, MW
    Madigan, CF
    Zhao, Y
    Zhang, LT
    Malik, S
    38TH DESIGN AUTOMATION CONFERENCE PROCEEDINGS 2001, 2001, : 530 - 535
  • [35] Integration of supercubing and learning in a SAT solver
    Babic, Domagoj
    Hu, Alan J.
    ASP-DAC 2005: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2005, : 438 - 444
  • [36] Active Learning for SAT Solver Benchmarking
    Fuchs, Tobias
    Bach, Jakob
    Iser, Markus
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2023, 2023, 13993 : 407 - 425
  • [37] A software/reconfigurable hardware SAT solver
    Skliarova, I
    Ferrari, AB
    IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2004, 12 (04) : 408 - 419
  • [38] Coverage-Driven Design Verification Using a Diverse SAT Solver
    Kakiuchi, Yosuke
    Hamaguchi, Kiyoharu
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2017, E100A (07) : 1481 - 1487
  • [39] Model Abstraction for Discrete-Event Systems Using a SAT Solver
    Cheng, Lihong
    Feng, Lei
    IEEE ACCESS, 2023, 11 : 17334 - 17347
  • [40] MFSAT: A SAT solver using multi-flip local search
    Mali, AD
    Lipen, YG
    15TH IEEE INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2003, : 84 - 93