DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions. - Alexey Ignatiev; Alexander A. Semenov (SAT, 2011)

Maximal Falsifiability - Definitions, Algorithms, and Applications. - Alexey Ignatiev; António Morgado 001; Jordi Planes; João Marques-Silva 001 (LPAR, 2013)

Quantified Maximum Satisfiability: - A Core-Guided Approach. - Alexey Ignatiev; Mikolás Janota; João Marques-Silva 001 (SAT, 2013)

Progression in Maximum Satisfiability. - Alexey Ignatiev; António Morgado 001; Vasco Manquinho; Inês Lynce; João Marques-Silva 001 (ECAI, 2014)

Efficient Autarkies. - João Marques-Silva 001; Alexey Ignatiev; António Morgado 001; Vasco Manquinho; Inês Lynce (ECAI, 2014)

Towards efficient optimization in package management systems. - Alexey Ignatiev; Mikolás Janota; João Marques-Silva 001 (ICSE, 2014)

On Reducing Maximum Independent Set to Minimum Satisfiability. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (SAT, 2014)

MSCG: Robust Core-Guided MaxSAT Solving. - António Morgado 001; Alexey Ignatiev; João Marques-Silva 001 (J. Satisf. Boolean Model. Comput., 2014)

Smallest MUS Extraction with Minimal Hitting Set Dualization. - Alexey Ignatiev; Alessandro Previti; Mark H. Liffiton; João Marques-Silva 001 (CP, 2015)

Efficient Model Based Diagnosis with Maximum Satisfiability. - João Marques-Silva 001; Mikolás Janota; Alexey Ignatiev; António Morgado 001 (IJCAI, 2015)

Prime Compilation of Non-Clausal Formulae. - Alessandro Previti; Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (IJCAI, 2015)

SAT-Based Formula Simplification. - Alexey Ignatiev; Alessandro Previti; João Marques-Silva 001 (SAT, 2015)

On Finding Minimum Satisfying Assignments. - Alexey Ignatiev; Alessandro Previti; João Marques-Silva 001 (CP, 2016)

On Incremental Core-Guided MaxSAT Solving. - Xujie Si; Xin Zhang 035; Vasco Manquinho; Mikolás Janota; Alexey Ignatiev; Mayur Naik (CP, 2016)

Propositional Abduction with Implicit Hitting Sets. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (ECAI, 2016)

Efficient Reasoning for Inconsistent Horn Formulae. - João Marques-Silva 001; Alexey Ignatiev; Carlos Mencía; Rafael Peñaloza (JELIA, 2016)

BEACON: An Efficient SAT-Based Tool for Debugging EL^+ Ontologies. - M. Fareed Arif; Carlos Mencía; Alexey Ignatiev; Norbert Manthey; Rafael Peñaloza; João Marques-Silva 001 (SAT, 2016)

MCS Extraction with Sublinear Oracle Queries. - Carlos Mencía; Alexey Ignatiev; Alessandro Previti; João Marques-Silva 001 (SAT, 2016)

Maximal falsifiability. - Alexey Ignatiev; António Morgado 001; Jordi Planes; João Marques-Silva 001 (AI Commun., 2016)

Quantified maximum satisfiability. - Alexey Ignatiev; Mikolás Janota; João Marques-Silva 001 (Constraints An Int. J., 2016)

Debugging EL+ Ontologies through Horn MUS Enumeration. - Alexey Ignatiev; João Marques-Silva 001; Carlos Mencía; Rafael Peñaloza (Description Logics, 2017)

Horn Maximum Satisfiability: Reductions, Algorithms and Applications. - João Marques-Silva 001; Alexey Ignatiev; António Morgado 001 (EPIA, 2017)

Lean Kernels in Description Logics. - Rafael Peñaloza; Carlos Mencía; Alexey Ignatiev; João Marques-Silva 001 (ESWC (1), 2017)

On Computing Generalized Backbones. - Alessandro Previti; Alexey Ignatiev; Matti Järvisalo; João Marques-Silva 001 (ICTAI, 2017)

Cardinality Encodings for Graph Optimization Problems. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (IJCAI, 2017)

On Tackling the Limits of Resolution in SAT Solving. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (SAT, 2017)

Model Based Diagnosis of Multiple Observations with Implicit Hitting Sets. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (CoRR, 2017)

Horn Maximum Satisfiability: Reductions, Algorithms & Applications. - João Marques-Silva 001; Alexey Ignatiev; António Morgado 001 (CoRR, 2017)

MaxSAT Resolution With the Dual Rail Encoding. - Maria Luisa Bonet; Sam Buss; Alexey Ignatiev; João Marques-Silva 001; António Morgado 001 (AAAI, 2018)

On Cryptographic Attacks Using Backdoors for SAT. - Alexander A. Semenov; Oleg Zaikin 002; Ilya V. Otpuschennikov; Stepan Kochemazov; Alexey Ignatiev (AAAI, 2018)

A SAT-Based Approach to Learn Explainable Decision Sets. - Alexey Ignatiev; Filipe Pereira; Nina Narodytska; João Marques-Silva 001 (IJCAR, 2018)

Learning Optimal Decision Trees with SAT. - Nina Narodytska; Alexey Ignatiev; Filipe Pereira; João Marques-Silva 001 (IJCAI, 2018)

PySAT: A Python Toolkit for Prototyping with SAT Oracles. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (SAT, 2018)

Abduction-Based Explanations for Machine Learning Models. - Alexey Ignatiev; Nina Narodytska; João Marques-Silva 001 (AAAI, 2019)

Model-Based Diagnosis with Multiple Observations. - Alexey Ignatiev; António Morgado 001; Georg Weissenbacher; João Marques-Silva 001 (IJCAI, 2019)

Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference. - Ilya Zakirzyanov; António Morgado 001; Alexey Ignatiev; Vladimir Ulyantsev; João Marques-Silva 001 (LATA, 2019)

On Relating Explanations and Adversarial Examples. - Alexey Ignatiev; Nina Narodytska; João Marques-Silva 001 (NeurIPS, 2019)

On Computing the Union of MUSes. - Carlos Mencía; Oliver Kullmann; Alexey Ignatiev; João Marques-Silva 001 (SAT, 2019)

DRMaxSAT with MaxHS: First Contact. - António Morgado 001; Alexey Ignatiev; Maria Luisa Bonet; João Marques-Silva 001; Sam Buss (SAT, 2019)

Assessing Heuristic Machine Learning Explanations with Model Counting. - Nina Narodytska; Aditya A. Shrotri; Kuldeep S. Meel; Alexey Ignatiev; João Marques-Silva 001 (SAT, 2019)

On Validating, Repairing and Refining Heuristic ML Explanations. - Alexey Ignatiev; Nina Narodytska; João Marques-Silva 001 (CoRR, 2019)

RC2: an Efficient MaxSAT Solver. - Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (J. Satisf. Boolean Model. Comput., 2019)

From Contrastive to Abductive Explanations and Back Again. - Alexey Ignatiev; Nina Narodytska; Nicholas Asher; João Marques-Silva 001 (AI*IA, 2020)

Towards Formal Fairness in Machine Learning. - Alexey Ignatiev; Martin C. Cooper; Mohamed Siala 002; Emmanuel Hebrard; João Marques-Silva 001 (CP, 2020)

Computing Optimal Decision Sets with SAT. - Jinqiang Yu; Alexey Ignatiev; Peter J. Stuckey; Pierre Le Bodic (CP, 2020)

Branch Location Problems with Maximum Satisfiability. - Oleg Zaikin 002; Alexey Ignatiev; João Marques-Silva 001 (ECAI, 2020)

Towards Trustable Explainable AI. - Alexey Ignatiev (IJCAI, 2020)

Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay. - João Marques-Silva 001; Thomas Gerspacher; Martin C. Cooper; Alexey Ignatiev; Nina Narodytska (NeurIPS, 2020)

Optimal Decision Lists using SAT. - Jinqiang Yu; Alexey Ignatiev; Pierre Le Bodic; Peter J. Stuckey (CoRR, 2020)

On Explaining Decision Trees. - Yacine Izza; Alexey Ignatiev; João Marques-Silva 001 (CoRR, 2020)

On Relating 'Why?' and 'Why Not?' Explanations. - Alexey Ignatiev; Nina Narodytska; Nicholas Asher; João Marques-Silva 001 (CoRR, 2020)

A Scalable Two Stage Approach to Computing Optimal Decision Sets. - Alexey Ignatiev; Edward Lam 001; Peter J. Stuckey; João Marques-Silva 001 (AAAI, 2021)

Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms. - Alexander A. Semenov; Daniil Chivilikhin; Artem Pavlenko; Ilya V. Otpuschennikov; Vladimir Ulyantsev; Alexey Ignatiev (CP, 2021)

Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. - Gianpiero Cabodi; Paolo E. Camurati; Alexey Ignatiev; João Marques-Silva 001; Marco Palena; Paolo Pasini (DATE, 2021)

Explanations for Monotonic Classifiers. - João Marques-Silva 001; Thomas Gerspacher; Martin C. Cooper; Alexey Ignatiev; Nina Narodytska (ICML, 2021)

Reasoning-Based Learning of Interpretable ML Models. - Alexey Ignatiev; João Marques-Silva 001; Nina Narodytska; Peter J. Stuckey (IJCAI, 2021)

On Efficiently Explaining Graph-Based Classifiers. - Xuanxiang Huang; Yacine Izza; Alexey Ignatiev; João Marques-Silva 001 (KR, 2021)

SAT-Based Rigorous Explanations for Decision Lists. - Alexey Ignatiev; João Marques-Silva 001 (SAT, 2021)

Assessing Progress in SAT Solvers Through the Lens of Incremental SAT. - Stepan Kochemazov; Alexey Ignatiev; João Marques-Silva 001 (SAT, 2021)

Propositional proof systems based on maximum satisfiability. - Maria Luisa Bonet; Sam Buss; Alexey Ignatiev; António Morgado 001; João Marques-Silva 001 (Artif. Intell., 2021)

Efficient Explanations With Relevant Sets. - Yacine Izza; Alexey Ignatiev; Nina Narodytska; Martin C. Cooper; João Marques-Silva 001 (CoRR, 2021)

Efficient Explanations for Knowledge Compilation Languages. - Xuanxiang Huang; Yacine Izza; Alexey Ignatiev; Martin C. Cooper; Nicholas Asher; João Marques-Silva 001 (CoRR, 2021)

Learning Optimal Decision Sets and Lists with SAT. - Jinqiang Yu; Alexey Ignatiev; Peter J. Stuckey; Pierre Le Bodic (J. Artif. Intell. Res., 2021)

Delivering Trustworthy AI through Formal XAI. - João Marques-Silva 001; Alexey Ignatiev (AAAI, 2022)

Tractable Explanations for d-DNNF Classifiers. - Xuanxiang Huang; Yacine Izza; Alexey Ignatiev; Martin C. Cooper; Nicholas Asher; João Marques-Silva 001 (AAAI, 2022)

Using MaxSAT for Efficient Explanations of Tree Ensembles. - Alexey Ignatiev; Yacine Izza; Peter J. Stuckey; João Marques-Silva 001 (AAAI, 2022)

Constraint-Driven Explanations for Black-Box ML Models. - Aditya A. Shrotri; Nina Narodytska; Alexey Ignatiev; Kuldeep S. Meel; João Marques-Silva 001; Moshe Y. Vardi (AAAI, 2022)

Provably Precise, Succinct and Efficient Explanations for Decision Trees. - Yacine Izza; Alexey Ignatiev; Nina Narodytska; Martin C. Cooper; João Marques-Silva 001 (CoRR, 2022)

Eliminating The Impossible, Whatever Remains Must Be True. - Jinqiang Yu; Alexey Ignatiev; Peter J. Stuckey; Nina Narodytska; João Marques-Silva 001 (CoRR, 2022)

On Tackling Explanation Redundancy in Decision Trees. - Yacine Izza; Alexey Ignatiev; João Marques-Silva 001 (J. Artif. Intell. Res., 2022)

Eliminating the Impossible, Whatever Remains Must Be True: On Extracting and Applying Background Knowledge in the Context of Formal Explanations. - Jinqiang Yu; Alexey Ignatiev; Peter J. Stuckey; Nina Narodytska; João Marques-Silva 001 (AAAI, 2023)

From Formal Boosted Tree Explanations to Interpretable Rule Sets. - Jinqiang Yu; Alexey Ignatiev; Peter J. Stuckey (CP, 2023)

On Tackling Explanation Redundancy in Decision Trees (Extended Abstract). - Yacine Izza; Alexey Ignatiev; João Marques-Silva 001 (IJCAI, 2023)

On Formal Feature Attribution and Its Approximation. - Jinqiang Yu; Alexey Ignatiev; Peter J. Stuckey (CoRR, 2023)

No silver bullet: interpretable ML models must be explained. - João Marques-Silva 001; Alexey Ignatiev (Frontiers Artif. Intell., 2023)

On computing probabilistic abductive explanations. - Yacine Izza; Xuanxiang Huang; Alexey Ignatiev; Nina Narodytska; Martin C. Cooper; João Marques-Silva 001 (Int. J. Approx. Reason., 2023)

Delivering Inflated Explanations. - Yacine Izza; Alexey Ignatiev; Peter J. Stuckey; João Marques-Silva 001 (AAAI, 2024)

Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. - Yacine Izza; Xuanxiang Huang; António Morgado 001; Jordi Planes; Alexey Ignatiev; João Marques-Silva 001 (KR, 2024)

Towards Universally Accessible SAT Technology. - Alexey Ignatiev; Zi Li Tan; Christos Karamanos (SAT, 2024)

Anytime Approximate Formal Feature Attribution. - Jinqiang Yu; Graham Farr; Alexey Ignatiev; Peter J. Stuckey (SAT, 2024)

NEUSIS: A Compositional Neuro-Symbolic Framework for Autonomous Perception, Reasoning, and Planning in Complex UAV Search Missions. - Zhixi Cai; Cristian Rojas Cardenas; Kevin Leo; Chenyuan Zhang; Kal Backman; Hanbing Li; Boying Li; Mahsa Ghorbanali; Stavya Datta; Lizhen Qu; Julian Gutierrez Santiago; Alexey Ignatiev; et al. (CoRR, 2024)

Formal Explanations for Neuro-Symbolic AI. - Sushmita Paul; Jinqiang Yu; Jip J. Dekker; Alexey Ignatiev; Peter J. Stuckey (CoRR, 2024)

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. - Elvira Albert; Maria Garcia de la Banda; Alejandro Hernández-Cerezo; Alexey Ignatiev; Albert Rubio; Peter J. Stuckey (Proc. ACM Program. Lang., 2024)

Artifact for "SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-based, and SAT Techniques". - Elvira Albert; Maria Garcia de la Banda; Alejandro Hernández-Cerezo; Alexey Ignatiev; Albert Rubio; Peter J. Stuckey (Zenodo, 2024)

A Formal Explainer for Just-In-Time Defect Predictions. - Jinqiang Yu; Michael Fu; Alexey Ignatiev; Chakkrit Tantithamthavorn; Peter J. Stuckey (ACM Trans. Softw. Eng. Methodol., 2024)

Towards Modern and Modular SAT for LCG (Short Paper). - Jip J. Dekker; Alexey Ignatiev; Peter J. Stuckey; Allen Z. Zhong (CP, 2025)

Most General Explanations of Tree Ensembles (Extended Version). - Yacine Izza; Alexey Ignatiev; Sasha Rubin; João Marques-Silva 001; Peter J. Stuckey (CoRR, 2025)

NEUSIS: A Compositional Neuro-Symbolic Framework for Autonomous Perception, Reasoning, and Planning in Complex UAV Search Missions. - Zhixi Cai; Cristian Rojas Cardenas; Kevin Leo; Chenyuan Zhang; Kal Backman; Hanbing Li; Boying Li; Mahsa Ghorbanali; Stavya Datta; Lizhen Qu; Julian Gutierrez 001; Alexey Ignatiev; et al. (IEEE Robotics Autom. Lett., 2025)