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 条
  • [41] Analyzing context-free grammars using an incremental SAT solver
    Axelsson, Roland
    Heljanko, Keijo
    Lange, Martin
    AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, PROCEEDINGS, 2008, 5126 : 410 - +
  • [42] Accelerating a continuous-time analog SAT solver using GPUs
    Molnar, Ferenc
    Kharel, Shubha R.
    Hu, Xiaobo Sharon
    Toroczkai, Zoltan
    COMPUTER PHYSICS COMMUNICATIONS, 2020, 256
  • [43] The Configurable SAT Solver Challenge (CSSC)
    Hutter, Frank
    Lindauer, Marius
    Balint, Adrian
    Bayless, Sam
    Hoos, Holger
    Leyton-Brown, Kevin
    ARTIFICIAL INTELLIGENCE, 2017, 243 : 1 - 25
  • [44] DSatz: A directional SAT solver for planning
    Iwen, M
    Mali, AD
    14TH IEEE INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2002, : 199 - 208
  • [45] HAIFASAT: A new robust SAT solver
    Gershman, Roman
    Strichman, Ofer
    HARDWARE AND SOFTWARE VERIFICATION AND TESTING, 2006, 3875 : 76 - 89
  • [46] MajorSat: A SAT Solver to Majority Logic
    Chou, Yu-Min
    Chen, Yung-Chih
    Wang, Chun-Yao
    Huang, Ching-Yi
    2016 21ST ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC), 2016, : 480 - 485
  • [47] FPGA-based sat solver
    Safar, Mona
    El-Kharashi, M. Watheq
    Salem, Ashraf
    2006 CANADIAN CONFERENCE ON ELECTRICAL AND COMPUTER ENGINEERING, VOLS 1-5, 2006, : 1480 - +
  • [48] RegSTAB: A SAT Solver for Propositional Schemata
    Aravantinos, Vincent
    Caferra, Ricardo
    Peltier, Nicolas
    AUTOMATED REASONING, 2010, 6173 : 309 - 315
  • [49] versat: A Verified Modern SAT Solver
    Oe, Duckki
    Stump, Aaron
    Oliver, Corey
    Clancy, Kevin
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2012, 7148 : 363 - 378
  • [50] On implementing a configware/software SAT solver
    Reis, NA
    de Sousa, JT
    10TH ANNUAL IEEE SYMPOSIUM ON FIELD-PROGRAMMABLE CUSTOM COMPUTING MACHINES, PROCEEDINGS, 2002, : 282 - 283