% Key papers for SAT and model counting solvers (scime atlas, https://atlas.scime.ai). Authors are not included: add them from the paper pages.

@inproceedings{aaai2019_bird_100618,
  title = {{BIRD: Engineering an Efficient CNF-XOR SAT Solver and Its Applications to Approximate Model Counting}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2019},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/3974},
}

@inproceedings{aaai2018_schur_106134,
  title = {{Schur Number Five}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2018},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/12209},
}

@inproceedings{neurips2018_boolean_56920,
  title = {{Boolean Decision Rules via Column Generation}},
  booktitle = {Advances in Neural Information Processing Systems (NeurIPS)},
  year = {2018},
  url = {https://nips.cc/virtual/2018/poster/11458},
}

@inproceedings{aaai2019_an_103242,
  title = {{An Innovative Genetic Algorithm for the Quantum Circuit Compilation Problem}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2019},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/4766},
}

@inproceedings{aaai2019_sat_101349,
  title = {{SAT-Based Explicit LTLf Satisfiability Checking}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2019},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/4150},
}

@inproceedings{aaai2016_the_104950,
  title = {{The Complexity of LTL on Finite Traces: Hard and Easy Fragments}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2016},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/10104},
}

@inproceedings{aaai2017_maximum_106125,
  title = {{Maximum Model Counting}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2017},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/11138},
}

@inproceedings{aaai2016_component_105383,
  title = {{Component Caching in Hybrid Domains with Piecewise Polynomial Densities}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2016},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/10441},
}

@inproceedings{aaai2017_a_106115,
  title = {{A SAT-Based Approach for Solving the Modal Logic S5-Satisfiability Problem}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2017},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/11128},
}

@inproceedings{aaai2021_certifying_238,
  title = {{Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2021},
  url = {https://aaai.org/papers/03768-certifying-parity-reasoning-efficiently-using-pseudo-boolean-proofs/},
}

@inproceedings{aaai2021_cutting_347,
  title = {{Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2021},
  url = {https://aaai.org/papers/03750-cutting-to-the-core-of-pseudo-boolean-optimization-combining-core-guided-search-with-cutting-planes-reasoning/},
}

@inproceedings{aaai2020_justifying_100639,
  title = {{Justifying All Differences Using Pseudo-Boolean Reasoning}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2020},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/5507},
}

@inproceedings{aaai2020_hard_100659,
  title = {{Hard Examples for Common Variable Decision Heuristics}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2020},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/5527},
}

@inproceedings{aaai2018_a_106128,
  title = {{A SAT+CAS Method for Enumerating Williamson Matrices of Even Order}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2018},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/12203},
}

@inproceedings{aaai2020_augmenting_100648,
  title = {{Augmenting the Power of (Partial) MaxSat Resolution with Extension}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2020},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/5516},
}

@inproceedings{aaai2022_certified_1828,
  title = {{Certified Symmetry and Dominance Breaking for Combinatorial Optimisation}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2022},
  url = {https://aaai.org/papers/03698-certified-symmetry-and-dominance-breaking-for-combinatorial-optimisation/},
}

@inproceedings{aaai2020_efficient_101383,
  title = {{Efficient Model-Based Diagnosis of Sequential Circuits}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2020},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/5670},
}

@inproceedings{aaai2021_a_47,
  title = {{A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2021},
  url = {https://aaai.org/papers/03697-a-sharp-leap-from-quantified-boolean-formula-to-stochastic-boolean-satisfiability-solving/},
}

@inproceedings{aaai2021_treewidth_1559,
  title = {{Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2021},
  url = {https://aaai.org/papers/06312-treewidth-aware-complexity-in-asp-not-all-positive-cycles-are-equally-hard/},
}

@inproceedings{aaai2022_on_2491,
  title = {{On Probabilistic Generalization of Backdoors in Boolean Satisfiability}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2022},
  url = {https://aaai.org/papers/10353-on-probabilistic-generalization-of-backdoors-in-boolean-satisfiability/},
}

@inproceedings{aaai2024_an_5170,
  title = {{An Approximate Skolem Function Counter}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28650},
}

@inproceedings{aaai2024_auditable_5226,
  title = {{Auditable Algorithms for Approximate Model Counting}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28936},
}

@inproceedings{aaai2024_cegar_5333,
  title = {{CEGAR-Based Approach for Solving Combinatorial Optimization Modulo Quantified Linear Arithmetics Problems}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28654},
}

@inproceedings{aaai2024_engineering_5838,
  title = {{Engineering an Exact Pseudo-Boolean Model Counter}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28660},
}

@inproceedings{aaai2024_sat_7203,
  title = {{SAT-Based Techniques for Lexicographically Smallest Finite Models}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28643},
}

@inproceedings{aaai2025_quantified_10416,
  title = {{Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2025},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/33213},
}

@inproceedings{aaai2026_a_106711,
  title = {{A Knowledge Compilation Map for Quantum Information}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2026},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/39018},
}

@inproceedings{aaai2024_a_5062,
  title = {{A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem (Student Abstract)}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/30472},
}

@inproceedings{aaai2024_an_5173,
  title = {{An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28649},
}

@inproceedings{aaai2024_model_6660,
  title = {{Model Counting and Sampling via Semiring Extensions}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/30022},
}

@inproceedings{aaai2024_runtime_7194,
  title = {{Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28631},
}

@inproceedings{aaai2024_unifying_7699,
  title = {{Unifying Decision and Function Queries in Stochastic Boolean Satisfiability}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28637},
}

@inproceedings{aaai2025_cirbo_8417,
  title = {{Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2025},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/33207},
}

@inproceedings{aaai2026_faster_106078,
  title = {{Faster Certified Symmetry Breaking Using Orders with Auxiliary Variables}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2026},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/38426},
}

@inproceedings{aaai2026_ordered_106081,
  title = {{Ordered Objectives in Maximum Satisfiability}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2026},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/38429},
}

@inproceedings{aaai2024_a_5061,
  title = {{A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract)}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/30437},
}

@inproceedings{aaai2024_hardness_6188,
  title = {{Hardness of Random Reordered Encodings of Parity for Resolution and CDCL}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28635},
}

@inproceedings{aaai2024_parameterization_6923,
  title = {{Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/28628},
}

@inproceedings{aaai2024_solving_7368,
  title = {{Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration with Provable Guarantees}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2024},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/30032},
}

@inproceedings{aaai2025_ai_7968,
  title = {{AI-Powered Algorithm-Centric Quantum Processor Topology Design}},
  booktitle = {AAAI Conference on Artificial Intelligence (AAAI)},
  year = {2025},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/32023},
}