×

DRAT-trim

swMATH ID: 13313
Software Authors: Wetzler, Nathan; Heule, Marijn J.H.; Hunt, Warren A.Jr.
Description: DRAT-trim: efficient checking and trimming using expressive clausal proofs. The DRAT-trim tool is a satisfiability proof checker based on the new DRAT proof format. Unlike its predecessor, DRUP-trim, all presently known SAT solving and preprocessing techniques can be validated using DRAT-trim. Checking time of a proof is comparable to the running time of the proof-producing solver. Memory usage is also similar to solving memory consumption, which overcomes a major hurdle of resolution-based proof checkers. The DRAT-trim tool can emit trimmed formulas, optimized proofs, and new TraceCheck\(^{ + }\) dependency graphs. We describe the output that is produced, what optimizations have been made to check RAT clauses, and potential applications of the tool.
Homepage: http://www.cs.utexas.edu/~marijn/drat-trim/
Related Software: MiniSat; Isabelle/HOL; Lingeling; Coq; Plingeling; z3; Treengeling; PicoSAT; ACL2; VIPR; MIPLIB; SCIP; CryptoMiniSat; CVC4; CaDiCaL; versat; GRAT; HOL Light; Chaff; SMTCoq
Cited in: 41 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
DRAT-trim: efficient checking and trimming using expressive clausal proofs. Zbl 1423.68475
Wetzler, Nathan; Heule, Marijn J. H.; Hunt, Warren A. jun.
2014
all top 5

Cited by 94 Authors

14 Heule, Marijn J. H.
6 Biere, Armin
6 Kiesl, Benjamin
3 Ganesh, Vijay
3 Hunt, Warren A. jun.
3 Philipp, Tobias
3 Rebola-Pardo, Adrián
3 Seidl, Martina
3 Wetzler, Nathan D.
2 Barrett, Clark W.
2 Bright, Curtis
2 Cheung, Kevin K. H.
2 Gleixner, Ambros M.
2 Kaufmann, Matt
2 Kotsireas, Ilias S.
2 Niemetz, Aina
2 Ozdemir, Alex
2 Preiner, Mathias
2 Scheucher, Manfred
2 Zohar, Yoni
1 Aichholzer, Oswin
1 Alviano, Mario
1 Baek, Seulkee
1 Barbosa, Haniel
1 Buss, Samuel R.
1 Chaouiya, Claudine
1 Chihani, Zakaria
1 Codish, Michael
1 Cruz-Filipe, Luís
1 Czarnecki, Krzysztof
1 Davis, Jared
1 Dodaro, Carmine
1 Dudek, Jeffrey M.
1 Egly, Uwe
1 Eifler, Leon
1 Farcot, Etienne
1 Fichte, Johannes Klaus
1 Frank, Michael
1 Froleyks, Nils
1 Fu, Yu-Fu
1 Ge, Cunjing
1 Hecher, Markus
1 Heinle, Albert
1 Huang, Pei
1 Hunt, Warren jun.
1 Iser, Markus
1 Itzhakov, Avraham
1 Järvisalo, Matti
1 Kremer, Gereon
1 Kullmann, Oliver
1 Kyncl, Jan
1 Lachnitt, Hanna
1 Lammich, Peter
1 Li, Chunxiao
1 Liang, Jiahui
1 Liu, Jiaxiang
1 Lonsing, Florian
1 Ma, Feifei
1 Marek, V. Wiktor
1 Marić, Filip
1 Mathew, Minu
1 Miller, Alice Ann
1 Miller, Dale Allen
1 Myreen, Magnus O.
1 Nötzli, Andres
1 Oh, Chanseok
1 Phan, Vu H. N.
1 Rath, Jakob
1 Renaud, Fabien
1 Reynolds, Andrew
1 Roy, Dominique
1 Schneider-Kamp, Peter
1 Shi, Xiaomu
1 Slaney, John K.
1 Steffy, Daniel E.
1 Stevens, Brett
1 Suda, Martin
1 Thapen, Neil
1 Thomas, Ciza
1 Tinelli, Cesare
1 Tompits, Hans
1 Tonello, Elisa
1 Tsai, Ming-Hsien
1 Valtr, Pavel
1 Vardi, Moshe Ya’akov
1 Viswanathan, Arjun
1 Viteri, Scott
1 Vogtenhuber, Birgit
1 Wang, Bow-Yaw
1 Woltzenlogel Paleo, Bruno
1 Yang, Bo-Yin
1 Zhang, Hantao
1 Zhang, Jian
1 Zulkoski, Edward
all top 5

Cited in 9 Serials

9 Journal of Automated Reasoning
3 Logical Methods in Computer Science
2 Computational Geometry
1 Artificial Intelligence
1 Formal Aspects of Computing
1 Applicable Algebra in Engineering, Communication and Computing
1 Constraints
1 Theory and Practice of Logic Programming
1 SIAM Journal on Applied Dynamical Systems
all top 5

Cited in 9 Fields

37 Computer science (68-XX)
11 Mathematical logic and foundations (03-XX)
5 Combinatorics (05-XX)
3 Convex and discrete geometry (52-XX)
2 Operations research, mathematical programming (90-XX)
1 Order, lattices, ordered algebraic structures (06-XX)
1 Geometry (51-XX)
1 Biology and other natural sciences (92-XX)
1 Information and communication theory, circuits (94-XX)

Citations by Year