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 条

[41] The effect of nogood recording in DPLL-CBJ SAT algorithms
Lynce, I
Marques-Silva, J
RECENT ADVANCES IN CONSTRAINTS, 2003, 2627 : 144 - 158
[42] Extending Clause Learning DPLL with Parity Reasoning
Laitinen, Tero
Junttila, Tommi
Niemela, Ilkka
ECAI 2010 - 19TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2010, 215 : 21 - 26
[43] Effects of a Complex Physical Activity Program on Children's Arithmetic Problem Solving and Arithmetic Reasoning Abilities
Greco, Gianpiero
Poli, Luca
Carvutto, Roberto
Patti, Antonino
Fischetti, Francesco
Cataldi, Stefania
EUROPEAN JOURNAL OF INVESTIGATION IN HEALTH PSYCHOLOGY AND EDUCATION, 2023, 13 (01) : 141 - 150
[44] A fast linear-arithmetic solver for DPLL(T)
Dutertre, Bruno
de Moura, Leonardo
COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2006, 4144 : 81 - 94
[45] Fuzzy arithmetic-based interpolative reasoning
Setnes, M
Kaymak, U
Lemke, HRV
Verbruggen, HB
ARTIFICIAL INTELLIGENCE IN REAL-TIME CONTROL 1997, 1998, : 379 - 384
[46] Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL
Krstic, Sava
Goel, Amit
FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2007, 4720 : 1 - +
[47] CUD@SAT: SAT solving on GPUs
Dal Palu, Alessandro
Dovier, Agostino
Formisano, Andrea
Pontelli, Enrico
JOURNAL OF EXPERIMENTAL & THEORETICAL ARTIFICIAL INTELLIGENCE, 2015, 27 (03) : 293 - 316
[48] Automated Goal Operationalisation Based on Interpolation and SAT SolvingAutomated Goal Operationalisation Based on Interpolation and SAT Solving
Degiovanni, Renzo
Alrajeh, Dalal
Aguirre, Nazareno
Uchitel, Sebastian
36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2014), 2014, : 129 - 139
[49] Multithreaded SAT solving
Lewis, Matthew
Schubert, Tobias
Becker, Bernd
PROCEEDINGS OF THE ASP-DAC 2007, 2007, : 926 - +
[50] SAT-Solving Based on Boundary Point Elimination
Goldberg, Eugene
Manolios, Panagiotis
HARDWARE AND SOFTWARE: VERIFICATION AND TESTING, 2011, 6504 : 93 - 111

← 1 2 3 4 5 →