IPASIR-up: user propagators for CDCL

DOI10.4230/LIPICS.SAT.2023.8MaRDI QIDQ6643080zbMATH OpenFDO

Authors Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere

Publication date 26 November 2024

Full work available at URL https://doi.org/10.4230/LIPICS.SAT.2023.8

zbMATH Keywords

CDCLSATsatisfiability modulo symmetriessatisfiability modulo theories

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cited in

(9)

• SAT modulo symmetries for graph generation and enumeration
• Constraint learning for non-confluent proof search
• Finding connections via satisfiability solving
• Towards universally accessible SAT technology
• Ground truth: checking \textsc{Vampire} proofs via satisfiability modulo theories
• Certifying incremental SAT solving
• SAT and lattice reduction for integer factorization
• Satisfiability modulo user propagators
• PACE solver description: crossy -- an exact solver for one-sided crossing minimization

This page was built for publication: IPASIR-up: user propagators for CDCL

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