Targeted configuration of an SMT solver

DOI10.1007/978-3-031-16681-5_18MaRDI QIDQ6160570zbMATH OpenFDO

Authors Jan Hůla, Jan Jakubův, Mikoláš Janota, Lukáš Kubej

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-16681-5_18

zbMATH Keywords

machine learningsatisfiability module theoriesstrategy inventionstrategy scheduling

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• The strategy challenge in SMT solving
• The configurable SAT solver challenge (CSSC)
• SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
• SATenstein: automatically building local search SAT solvers from components
• SpyBug: automated bug detection in the configuration space of SAT solvers

Cites work

• \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
• Concrete semantics. With Isabelle/HOL
• Extending Sledgehammer with SMT solvers
• Hammering towards QED
• Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
• Hierarchical invention of theorem proving strategies
• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• Machine learning for combinatorial optimization: a methodological tour d'horizon
• Paramils: an automatic algorithm configuration framework
• Refutation-based synthesis in SMT
• SATzilla: portfolio-based algorithm selection for SAT
• SMAC3: a versatile Bayesian optimization package for hyperparameter optimization
• Structural analysis of narratives with the Coq proof assistant
• System description: E 1.8

Cited in

(5)

• Solving hard Mizar problems with instantiation and strategy invention
• Graph sequence learning for premise selection
• Learning conjecturing from scratch
• Machine learning for quantifier selection in cvc5
• Regularization in Spider-style strategy discovery and schedule construction

This page was built for publication: Targeted configuration of an SMT solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6160570)