using #AI #neural-networks to make #SAT solvers work better. #toread #formal-methods
on 02026-03-18TeX source code to Yurichev's #ebook about #SAT/#SMT.
on 02024-06-23#PDF #ebook “#SAT/#SMT by Example” by Dennis Yurichev, 671 pp. “The author of these lines is no expert in SAT/SMT, by any means. This is not a book, rather a student’s notes.” A very extensive set of examples; the English isn’t perfect but generally is comprehensible. #toread
on 02024-06-23the main #documentation on how to use #Z3, including for #optimization #SAT #SMT
on 02024-06-23#Z3 #tutorial #documentation that covers things like validating numerical approximation algorithms and training neural networks with it #SAT #SMT
on 02024-06-23Leonardo de Moura’s #tutorial #documentation #introduction to #Z3 in Python. It starts out focusing on things like integers, real numbers, and arbitrary precision, but then moves on to bitvectors, bit-twiddling hacks, sudoku, N-queens, and package management. #SAT #SMT
on 02024-06-23"SMTInterpol" #SMT solver. #formal-methods #SAT
on 02024-06-16#SMT-COMP #PDF #paper about #SMTInterpol, a DPLL(T)/CDCL #SMT solver in Java licensed under LGPLv3. #toread #formal-methods #SAT
on 02024-06-16"CVC5" (Cooperating Validity Checker 5), based on #Minisat, written in C++, and licensed under a 3-clause BSD license, is kind of the top #SMT solver according to the #SMT-COMP results. You can hook it up to #ABC, #CryptoMiniSat, #libpoly, #GMP, #CaDiCal, #symfpu, #CLN (the Class Library for Numbers), and #GLPK. #toread #formal-methods #SAT
on 02024-06-16#SMT-COMP #PDF #paper about the #CVC5 CDCL(T) #SMT solver, the top winner in many categories, licensed under a BSD license. #SAT #formal-methods #toread
on 02024-06-16#SMT-COMP #PDF #paper about #iProver. #toread #formal-methods #SMT #SAT
on 02024-06-16#SMT-COMP winner "iProver" is a first-order theorem prover written in OCaml licensed under GPL2+. It wraps #Z3 and #Minisat #SAT solvers. #formal-methods #SMT
on 02024-06-16#SMT-COMP winner "Vampire" is under a 3-clause BSD license. #SMT #SAT #formal-methods
on 02024-06-16#SMT-COMP #PDF #paper about #Vampire, a first-order theorem prover. #toread #formal-methods #SMT #SAT
on 02024-06-16#SMT-COMP winner "Yices2" #SMT #SAT #formal-methods
on 02024-06-16#PDF #SMT-COMP paper about the #Yices2 CDCL(T) #SMT solver, which supports three different #SAT solver backends: CaDiCaL, CryptoMiniSat, and Kissat. #formal-methods
on 02024-06-16#PDF #paper about the #Bitwuzla #SMT solver at #SMT-COMP, a C++ rewrite of a fork of Boolector. #SAT #toread #formal-methods
on 02024-06-16#PDF #paper about the #Z3++ #SMT solver, which is based on #Z3. #SAT #toread #formal-methods
on 02024-06-16#PDF #paper about the #OpenSMT T-DPLL #SMT solver, which is based on MiniSAT. #SAT #toread #formal-methods
on 02024-06-16The "OpenSMT" #SMT (#SAT plus theories) solver, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16#SMT and #SAT competition "SMT-COMP" has many divisions now. #formal-methods
on 02024-06-16#ebook about #Selfie, the #bootstrapping system that emulates a subset of #RISC-V and compiles itself from a subset of #C and has a #SAT #solver for bounded model checking
on 02021-02-09comments on an #introduction to the #Z3 #SAT #solver
on 02019-02-15some notes on #SAT #solver #performance and the relationship with backtracking search
on 02019-02-15#SAT #solver #introduction with implementation in Haskell.
on 02017-06-07A #smallisbeautiful but high-performance #SAT #solver; the original version in 2003 was 600 lines with “conflict-clause recording, conflict-driven backjumping, VSIDS dynamic variable order,” and a “two-literal watch scheme”, plus “extensions for incremental SAT and for non-clausal constraints over boolean variables”, by Niklas Eén and Niklas Sörensson.
on 02017-03-22CBMC is a bounded model checker for #C and C++, using #SAT solvers and SMT solvers to statically check array bounds. Licensed under a 4-clause BSD license. Intended for embedded software. #formal-methods
on 02016-07-04A #SAT problem generator, explaining a bit about how to prepare difficult SAT problems for SAT solvers like MiniSat.
on 02015-11-21SMT-LIB is a library of problems and theories for SMT solvers (#SAT modulo theories).
on 02015-11-16Dejan Jovanović and Leonardo de Moura wrote a #paper about deciding #SAT for nonlinear arithmetic #constraint-programming. Not Diophantine.
on 02015-09-18a huge list of free software for verification and synthesis, including SMT solvers (#SAT modulo theories), #logic-programming, and dozens of pages of stuff I don’t understand.
on 02015-09-18a blog about #constraint-programming and #logic-programming. Talks a bit about #SAT solvers and their relationship to CP, which I still don’t understand.
on 02015-09-18an overview of #probabilistic-programming systems, #SAT solvers, with a paragraph or so about each.
on 02015-09-18