Arithmetic reasoning in DPLL-based SAT solving

被引：2

作者：

Wedler, M ^{[1
]}

Stoffel, D ^{[1
]}

Kunz, W ^{[1
]}

机构：

[1] Univ Kaiserslautern, Dept Elect & Comp Engn, D-67663 Kaiserslautern, Germany

来源：

DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS | 2004年

关键词：

D O I：

10.1109/DATE.2004.1268823

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We propose a new arithmetic reasoning calculus to speed up a SAT solver based on the Davis Putnam Longman Loveland (DPLL) procedure. It is based on an arithmetic bit level description of the arithmetic circuit parts and the property. This description can easily be provided by the front-end of an RTL property checker The calculus yields significant speedup and more robustness on hard SAT instances derived from the formal verification of arithmetic circuits.

引用

页码：30 / 35

页数：6

共 50 条

[1] A DPLL-based High-Concurrent SAT Solver with FPGA
Yu, Lvying
Zuo, Yi
Li, Caihong
He, Anping
2ND INTERNATIONAL CONFERENCE ON COMPUTER ENGINEERING, INFORMATION SCIENCE AND INTERNET TECHNOLOGY, CII 2017, 2017, : 118 - 123
[2] Technical Foundations of a DPLL-Based SAT Solver for Propositional Godel Logic
Guller, Dusan
IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2018, 26 (01) : 84 - 100
[3] On finding minimal-models using DPLL-based SAT solver
Shikada, Norihide
Taniguchi, Kiyonori
Hasegawa, Ryuzo
Fujita, Hiroshi
Koshimura, Miyuki
Research Reports on Information Science and Electrical Engineering of Kyushu University, 2007, 12 (02): : 81 - 86
[4] The Mechanical Verification of a DPLL-Based Satisfiability Solver
Shankar, Natarajan
Vaucher, Marc
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2011, 269 : 3 - 17
[5] A DPLL-based calculus for ground satisfiability modulo theories
Tinelli, C
LOGICS IN ARTIFICIAL INTELLIGENCE 8TH, 2002, 2424 : 308 - 319
[6] From Resolution and DPLL to Solving Arithmetic Constraints
Korovin, Konstantin
FRONTIERS OF COMBINING SYSTEMS (FROCOS 2013), 2013, 8152 : 261 - 262
[7] DPLL-Based VRO of Time-to-Digital Converter
Liu, Jen-Chieh
Chen, Yan-Xun
IEEE SOLID-STATE CIRCUITS LETTERS, 2023, 6 : 45 - 48
[8] Foundations of a DPLL-Based Solver for Fuzzy Answer Set Programs
Uhliarik, Ivor
COMPUTATIONAL INTELLIGENCE, IJCCI 2017, 2019, 829 : 99 - 117
[9] On solving Presburger and linear arithmetic with SAT
Strichman, O
FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2002, 2517 : 160 - 170
[10] Solving Linear Arithmetic with SAT-based Model Checking
Vizel, Yakir
Nadel, Alexander
Malik, Sharad
PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 47 - 54

← 1 2 3 4 5 →