| 2026 | CP | Efficient Explanations for Rule Ensembles. | Hao Hu, Alexey Ignatiev, Joo Marques-Silva |
| 2026 | KR | Model-Agnostic Explanations by Consensus. | Carlos Menca, Ramn Bjar, Ral Menca, Joo Marques-Silva |
| 2026 | SAT | Trustable Explainable AI - SAT to the Rescue (Invited Talk). | Joo Marques-Silva |
| 2026 | SAT | Shapley-Shubik Attribution from Minimal Subsets (Short Paper). | Pablo Martnez-Naredo, Ral Menca, Joo Marques-Silva, Carlos Menca |
| 2025 | AAAI | Towards Trustable SHAP Scores. | Olivier Ltoff, Xuanxiang Huang, Joo Marques-Silva |
| 2025 | ICAART | The Pros and Cons of Adversarial Robustness. | Yacine Izza, Joo Marques-Silva |
| 2025 | IJCAI | Efficient and Rigorous Model-Agnostic Explanations. | Joo Marques-Silva, Jairo A. Lefebre-Lobaina, Maria Vanina Martinez |
| 2025 | IJCAI | Most General Explanations of Tree Ensembles. | Yacine Izza, Alexey Ignatiev, Sasha Rubin, Joo Marques-Silva, Peter J. Stuckey |
| 2025 | IDEAL | Uncovering and Correcting XAI's Misconceptions Logic to the Rescue. | Joo Marques-Silva |
| 2025 | JELIA | Formal Explanations of Black-Box Ranking Functions. | Francesco Chiariello, Joo Marques-Silva |
| 2025 | JELIA | Explanations of Unsatisfiability Beyond Minimal Subsets. | Pablo Martnez-Naredo, Ral Menca, Joo Marques-Silva, Carlos Menca |
| 2024 | AAAI | Delivering Inflated Explanations. | Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, Joo Marques-Silva |
| 2024 | ECAI | Locally-Minimal Probabilistic Explanations. | Yacine Izza, Kuldeep S. Meel, Joo Marques-Silva |
| 2024 | IJCAI | Updates on the Complexity of SHAP Scores. | Xuanxiang Huang, Joo Marques-Silva |
| 2024 | ISoLA | Logic-Based Explainability: Past, Present and Future. | Joo Marques-Silva |
| 2024 | KR | Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. | Yacine Izza, Xuanxiang Huang, Antnio Morgado, Jordi Planes, Alexey Ignatiev, Joo Marques-Silva |
| 2023 | AAAI | Solving Explainability Queries with Quantification: The Case of Feature Relevancy. | Xuanxiang Huang, Yacine Izza, Joo Marques-Silva |
| 2023 | AAAI | 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, Joo Marques-Silva |
| 2023 | ECAI | From Decision Trees to Explained Decision Sets. | Xuanxiang Huang, Joo Marques-Silva |
| 2023 | ICECCS | Disproving XAI Myths with Formal Methods - Initial Results. | Joo Marques-Silva |
| 2023 | IJCAI | On Tackling Explanation Redundancy in Decision Trees (Extended Abstract). | Yacine Izza, Alexey Ignatiev, Joo Marques-Silva |
| 2023 | KR | Tractable Explaining of Multivariate Decision Trees. | Clment Carbonnel, Martin C. Cooper, Joo Marques-Silva |
| 2023 | KR | On Computing Relevant Features for Explaining NBCs. | Yacine Izza, Joo Marques-Silva |
| 2023 | TACAS | Feature Necessity & Relevancy in ML Classifier Explanations. | Xuanxiang Huang, Martin C. Cooper, Antnio Morgado, Jordi Planes, Joo Marques-Silva |
| 2023 | TAP | Certified Logic-Based Explainable AI - The Case of Monotonic Classifiers. | Aurlie Hurault, Joo Marques-Silva |
| 2022 | AAAI | Delivering Trustworthy AI through Formal XAI. | Joo Marques-Silva, Alexey Ignatiev |
| 2022 | AAAI | Tractable Explanations for d-DNNF Classifiers. | Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, Joo Marques-Silva |
| 2022 | AAAI | Using MaxSAT for Efficient Explanations of Tree Ensembles. | Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, Joo Marques-Silva |
| 2022 | AAAI | Constraint-Driven Explanations for Black-Box ML Models. | Aditya A. Shrotri, Nina Narodytska, Alexey Ignatiev, Kuldeep S. Meel, Joo Marques-Silva, Moshe Y. Vardi |
| 2021 | AAAI | A Scalable Two Stage Approach to Computing Optimal Decision Sets. | Alexey Ignatiev, Edward Lam, Peter J. Stuckey, Joo Marques-Silva |
| 2021 | CP | On the Tractability of Explaining Decisions of Classifiers. | Martin C. Cooper, Joo Marques-Silva |
| 2021 | DATE | Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. | Gianpiero Cabodi, Paolo E. Camurati, Alexey Ignatiev, Joo Marques-Silva, Marco Palena, Paolo Pasini |
| 2021 | ICML | Explanations for Monotonic Classifiers. | Joo Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska |
| 2021 | IJCAI | Reasoning-Based Learning of Interpretable ML Models. | Alexey Ignatiev, Joo Marques-Silva, Nina Narodytska, Peter J. Stuckey |
| 2021 | IJCAI | On Explaining Random Forests with SAT. | Yacine Izza, Joo Marques-Silva |
| 2021 | KR | On Efficiently Explaining Graph-Based Classifiers. | Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Joo Marques-Silva |
| 2021 | SAT | SAT-Based Rigorous Explanations for Decision Lists. | Alexey Ignatiev, Joo Marques-Silva |
| 2021 | SAT | Assessing Progress in SAT Solvers Through the Lens of Incremental SAT. | Stepan Kochemazov, Alexey Ignatiev, Joo Marques-Silva |
| 2020 | CP | Towards Formal Fairness in Machine Learning. | Alexey Ignatiev, Martin C. Cooper, Mohamed Siala, Emmanuel Hebrard, Joo Marques-Silva |
| 2020 | ECAI | Branch Location Problems with Maximum Satisfiability. | Oleg Zaikin, Alexey Ignatiev, Joo Marques-Silva |
| 2020 | IJCAI | Reasoning About Inconsistent Formulas. | Joo Marques-Silva, Carlos Menca |
| 2020 | SAT | Reasoning About Strong Inconsistency in ASP. | Carlos Menca, Joo Marques-Silva |
| 2019 | AAAI | Abduction-Based Explanations for Machine Learning Models. | Alexey Ignatiev, Nina Narodytska, Joo Marques-Silva |
| 2019 | EPIA | Computing Shortest Resolution Proofs. | Carlos Menca, Joo Marques-Silva |
| 2019 | IJCAI | Model-Based Diagnosis with Multiple Observations. | Alexey Ignatiev, Antnio Morgado, Georg Weissenbacher, Joo Marques-Silva |
| 2019 | LATA | Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference. | Ilya Zakirzyanov, Antnio Morgado, Alexey Ignatiev, Vladimir Ulyantsev, Joo Marques-Silva |
| 2019 | SAT | On Computing the Union of MUSes. | Carlos Menca, Oliver Kullmann, Alexey Ignatiev, Joo Marques-Silva |
| 2019 | SAT | DRMaxSAT with MaxHS: First Contact. | Antnio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joo Marques-Silva, Sam Buss |
| 2019 | SAT | Assessing Heuristic Machine Learning Explanations with Model Counting. | Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, Joo Marques-Silva |
| 2018 | AAAI | MaxSAT Resolution With the Dual Rail Encoding. | Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Joo Marques-Silva, Antnio Morgado |
| 2018 | AAAI | Premise Set Caching for Enumerating Minimal Correction Subsets. | Alessandro Previti, Carlos Menca, Matti Jrvisalo, Joo Marques-Silva |
| 2018 | CADE | A SAT-Based Approach to Learn Explainable Decision Sets. | Alexey Ignatiev, Filipe Pereira, Nina Narodytska, Joo Marques-Silva |
| 2018 | CiE | Computing with SAT Oracles: Past, Present and Future. | Joo Marques-Silva |
| 2018 | IJCAI | Learning Optimal Decision Trees with SAT. | Nina Narodytska, Alexey Ignatiev, Filipe Pereira, Joo Marques-Silva |
| 2018 | SAT | PySAT: A Python Toolkit for Prototyping with SAT Oracles. | Alexey Ignatiev, Antnio Morgado, Joo Marques-Silva |
| 2017 | EPIA | An Achilles' Heel of Term-Resolution. | Mikols Janota, Joo Marques-Silva |
| 2017 | EPIA | Horn Maximum Satisfiability: Reductions, Algorithms and Applications. | Joo Marques-Silva, Alexey Ignatiev, Antnio Morgado |
| 2017 | IJCAI | Cardinality Encodings for Graph Optimization Problems. | Alexey Ignatiev, Antnio Morgado, Joo Marques-Silva |
| 2017 | ICTAI | On Computing Generalized Backbones. | Alessandro Previti, Alexey Ignatiev, Matti Jrvisalo, Joo Marques-Silva |
| 2017 | SAT | On Tackling the Limits of Resolution in SAT Solving. | Alexey Ignatiev, Antnio Morgado, Joo Marques-Silva |
| 2017 | SAT | Improving MCS Enumeration via Caching. | Alessandro Previti, Carlos Menca, Matti Jrvisalo, Joo Marques-Silva |
| 2017 | TACAS | Efficient Certified Resolution Proof Checking. | Lus Cruz-Filipe, Joo Marques-Silva, Peter Schneider-Kamp |
| 2016 | AAAI | Preface: The Beyond NP Workshop. | Adnan Darwiche, Joo Marques-Silva, Pierre Marquis |
| 2016 | CP | On Finding Minimum Satisfying Assignments. | Alexey Ignatiev, Alessandro Previti, Joo Marques-Silva |
| 2016 | ECAI | Propositional Abduction with Implicit Hitting Sets. | Alexey Ignatiev, Antnio Morgado, Joo Marques-Silva |
| 2016 | JELIA | Efficient Reasoning for Inconsistent Horn Formulae. | Joo Marques-Silva, Alexey Ignatiev, Carlos Menca, Rafael Pealoza |
| 2016 | SAT | BEACON: An Efficient SAT-Based Tool for Debugging | M. Fareed Arif, Carlos Menca, Alexey Ignatiev, Norbert Manthey, Rafael Pealoza, Joo Marques-Silva |
| 2016 | SAT | MCS Extraction with Sublinear Oracle Queries. | Carlos Menca, Alexey Ignatiev, Alessandro Previti, Joo Marques-Silva |
| 2015 | CP | Smallest MUS Extraction with Minimal Hitting Set Dualization. | Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, Joo Marques-Silva |
| 2015 | IJCAI | Solving QBF by Clause Selection. | Mikols Janota, Joo Marques-Silva |
| 2015 | IJCAI | Efficient Model Based Diagnosis with Maximum Satisfiability. | Joo Marques-Silva, Mikols Janota, Alexey Ignatiev, Antnio Morgado |
| 2015 | IJCAI | Literal-Based MCS Extraction. | Carlos Menca, Alessandro Previti, Joo Marques-Silva |
| 2015 | IJCAI | Prime Compilation of Non-Clausal Formulae. | Alessandro Previti, Alexey Ignatiev, Antnio Morgado, Joo Marques-Silva |
| 2015 | ICTAI | MILP for the Multi-objective VM Reassignment Problem. | Takfarinas Saber, Anthony Ventresque, Joo Marques-Silva, James Thorburn, Liam Murphy |
| 2015 | KI | Efficient Axiom Pinpointing with EL2MCS. | M. Fareed Arif, Carlos Menca, Joo Marques-Silva |
| 2015 | SAT | Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing. | M. Fareed Arif, Carlos Menca, Joo Marques-Silva |
| 2015 | SAT | SAT-Based Formula Simplification. | Alexey Ignatiev, Alessandro Previti, Joo Marques-Silva |
| 2015 | SAT | Computing Maximal Autarkies with Few and Simple Oracle Queries. | Oliver Kullmann, Joo Marques-Silva |
| 2015 | SAT | SAT-Based Horn Least Upper Bounds. | Carlos Menca, Alessandro Previti, Joo Marques-Silva |
| 2014 | CP | Core-Guided MaxSAT with Soft Cardinality Constraints. | Antnio Morgado, Carmine Dodaro, Joo Marques-Silva |
| 2014 | CPAIOR | A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. | Yuri Malitsky, Barry O'Sullivan, Alessandro Previti, Joo Marques-Silva |
| 2014 | ECAI | Progression in Maximum Satisfiability. | Alexey Ignatiev, Antnio Morgado, Vasco Manquinho, Ins Lynce, Joo Marques-Silva |
| 2014 | ECAI | Timeout-Sensitive Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. | Yuri Malitsky, Barry O'Sullivan, Alessandro Previti, Joo Marques-Silva |
| 2014 | ECAI | Efficient Autarkies. | Joo Marques-Silva, Alexey Ignatiev, Antnio Morgado, Vasco Manquinho, Ins Lynce |
| 2014 | ICSE | Towards efficient optimization in package management systems. | Alexey Ignatiev, Mikols Janota, Joo Marques-Silva |
| 2014 | ICTAI | Efficient Relaxations of Over-constrained CSPs. | Carlos Menca, Joo Marques-Silva |
| 2014 | JELIA | Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form. | Sad Jabbour, Joo Marques-Silva, Lakhdar Sais, Yakoub Salhi |
| 2014 | SAT | MUS Extraction Using Clausal Proofs. | Anton Belov, Marijn Heule, Joo Marques-Silva |
| 2014 | SAT | On Reducing Maximum Independent Set to Minimum Satisfiability. | Alexey Ignatiev, Antnio Morgado, Joo Marques-Silva |
| 2014 | SAT | On Computing Preferred MUSes and MCSes. | Joo Marques-Silva, Alessandro Previti |
| 2014 | TACAS | Synthesizing Safe Bit-Precise Invariants. | Arie Gurfinkel, Anton Belov, Joo Marques-Silva |
| 2013 | AAAI | Partial MUS Enumeration. | Alessandro Previti, Joo Marques-Silva |
| 2013 | CAV | Minimal Sets over Monotone Predicates in Boolean Formulae. | Joo Marques-Silva, Mikols Janota, Anton Belov |
| 2013 | CP | Solving QBF with Free Variables. | William Klieber, Mikols Janota, Joo Marques-Silva, Edmund M. Clarke |
| 2013 | DATE | Core minimization in SAT-based abstraction. | Anton Belov, Huan Chen, Alan Mishchenko, Joo Marques-Silva |
| 2013 | IJCAI | On Computing Minimal Correction Subsets. | Joo Marques-Silva, Federico Heras, Mikols Janota, Alessandro Previti, Anton Belov |
| 2013 | ICTAI | Model-Guided Approaches for MaxSAT Solving. | Antnio Morgado, Federico Heras, Joo Marques-Silva |
| 2013 | LPAR | SAT-Based Preprocessing for MaxSAT. | Anton Belov, Antnio Morgado, Joo Marques-Silva |
| 2013 | LPAR | Maximal Falsifiability - Definitions, Algorithms, and Applications. | Alexey Ignatiev, Antnio Morgado, Jordi Planes, Joo Marques-Silva |
| 2013 | LPAR | On QBF Proofs and Preprocessing. | Mikols Janota, Radu Grigore, Joo Marques-Silva |
| 2013 | SAT | Parallel MUS Extraction. | Anton Belov, Norbert Manthey, Joo Marques-Silva |
| 2013 | SAT | Quantified Maximum Satisfiability: - A Core-Guided Approach. | Alexey Ignatiev, Mikols Janota, Joo Marques-Silva |
| 2013 | SAT | On Propositional QBF Expansions and Q-Resolution. | Mikols Janota, Joo Marques-Silva |
| 2013 | TACAS | Formula Preprocessing in MUS Extraction. | Anton Belov, Matti Jrvisalo, Joo Marques-Silva |
| 2012 | AI | An Empirical Study of Encodings for Group MaxSAT. | Federico Heras, Antnio Morgado, Joo Marques-Silva |
| 2012 | CP | On Computing Minimal Equivalent Subformulas. | Anton Belov, Mikols Janota, Ins Lynce, Joo Marques-Silva |
| 2012 | DATE | QBf-based boolean function bi-decomposition. | Huan Chen, Mikols Janota, Joo Marques-Silva |
| 2012 | ICTAI | Iterative SAT Solving for Minimum Satisfiability. | Federico Heras, Antnio Morgado, Jordi Planes, Joo Marques-Silva |
| 2012 | KR | On Unit-Refutation Complete Formulae with Existentially Quantified Variables. | Lucas Bordeaux, Mikols Janota, Joo Marques-Silva, Pierre Marquis |
| 2012 | SAT | On Efficient Computation of Variable MUSes. | Anton Belov, Alexander Ivrii, Arie Matsliah, Joo Marques-Silva |
| 2012 | SAT | Solving QBF with Counterexample Guided Refinement. | Mikols Janota, William Klieber, Joo Marques-Silva, Edmund M. Clarke |
| 2012 | SAT | Improvements to Core-Guided Binary Search for MaxSAT. | Antnio Morgado, Federico Heras, Joo Marques-Silva |
| 2012 | SOFSEM | Knowledge Compilation with Empowerment. | Lucas Bordeaux, Joo Marques-Silva |
| 2011 | AAAI | Core-Guided Binary Search Algorithms for Maximum Satisfiability. | Federico Heras, Antnio Morgado, Joo Marques-Silva |
| 2011 | CP | On Deciding MUS Membership with QBF. | Mikols Janota, Joo Marques-Silva |
| 2011 | FMCAD | Accelerating MUS extraction with recursive model rotation. | Anton Belov, Joo Marques-Silva |
| 2011 | IJCAI | Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms. | Federico Heras, Joo Marques-Silva |
| 2011 | ICTAI | On Validating Boolean Optimizers. | Antnio Morgado, Joo Marques-Silva |
| 2011 | LPNMR | cmMUS: A Tool for Circumscription-Based MUS Membership Testing. | Mikols Janota, Joo Marques-Silva |
| 2011 | SAT | Minimally Unsatisfiable Boolean Circuits. | Anton Belov, Joo Marques-Silva |
| 2011 | SAT | Abstraction-Based Algorithm for 2QBF. | Mikols Janota, Joo Marques-Silva |
| 2011 | SAT | On Improving MUS Extraction Algorithms. | Joo Marques-Silva, Ins Lynce |
| 2010 | CPAIOR | Boolean Lexicographic Optimization. | Joo Marques-Silva, Josep Argelich, Ana Graa, Ins Lynce |
| 2010 | ECAI | On Computing Backbones of Propositional Theories. | Joo Marques-Silva, Mikols Janota, Ins Lynce |
| 2010 | ICTAC | Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking. | Ashish Darbari, Bernd Fischer, Joo Marques-Silva |
| 2010 | JELIA | Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. | Mikols Janota, Radu Grigore, Joo Marques-Silva |
| 2010 | SOFSEM | How to Complete an Interactive Configuration Process? | Mikols Janota, Goetz Botterweck, Radu Grigore, Joo Marques-Silva |
| 2009 | ICFEM | A Lazy Unbounded Model Checker for Event-B. | Paulo J. Matos, Bernd Fischer, Joo Marques-Silva |
| 2009 | IJCAI | On Solving Boolean Multilevel Optimization Problemse. | Josep Argelich, Ins Lynce, Joo Marques-Silva |
| 2009 | SAT | Algorithms for Weighted Boolean Optimization. | Vasco Manquinho, Joo Marques-Silva, Jordi Planes |
| 2008 | CPAIOR | Efficient Haplotype Inference with Combined CP and OR Techniques. | Ana Graa, Joo Marques-Silva, Ins Lynce, Arlindo L. Oliveira |
| 2008 | DATE | Algorithms for Maximum Satisfiability using Unsatisfiable Cores. | Joo Marques-Silva, Jordi Planes |
| 2008 | ECAI | A MAX-SAT Algorithm Portfolio. | Paulo J. Matos, Jordi Planes, Florian Letombe, Joo Marques-Silva |
| 2008 | FlAIRS | On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization. | Federico Heras, Vasco Manquinho, Joo Marques-Silva |
| 2008 | ICTAI | Haplotype Inference with Boolean Constraint Solving: An Overview. | Ins Lynce, Ana Graa, Joo Marques-Silva, Arlindo L. Oliveira |
| 2008 | LPAR | Symmetry Breaking for Maximum Satisfiability. | Joo Marques-Silva, Ins Lynce, Vasco Manquinho |
| 2008 | SAT | Improvements to Hybrid Incremental SAT Algorithms. | Florian Letombe, Joo Marques-Silva |
| 2008 | SAT | Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms. | Joo Marques-Silva, Vasco Manquinho |
| 2007 | CP | Towards Robust CNF Encodings of Cardinality Constraints. | Joo Marques-Silva, Ins Lynce |
| 2007 | EPIA | Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony Using Delayed Haplotype Selection. | Joo Marques-Silva, Ins Lynce, Ana Graa, Arlindo L. Oliveira |
| 2007 | MEMOCODE | Towards Equivalence Checking Between TLM and RTL Models. | Nicola Bombieri, Franco Fummi, Graziano Pravadelli, Joo Marques-Silva |
| 2007 | SAT | Breaking Symmetries in SAT Matrix Models. | Ins Lynce, Joo Marques-Silva |
| 2006 | AAAI | Efficient Haplotype Inference with Boolean Satisfiability. | Ins Lynce, Joo Marques-Silva |
| 2006 | SAT | Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel. | Oliver Kullmann, Ins Lynce, Joo Marques-Silva |
| 2006 | SAT | SAT in Bioinformatics: Making the Case with Haplotype Inference. | Ins Lynce, Joo Marques-Silva |
| 2006 | SAT | Counting Models in Integer Domains. | Antnio Morgado, Paulo J. Matos, Vasco Manquinho, Joo Marques-Silva |
| 2005 | DATE | Effective Lower Bounding Techniques for Pseudo-Boolean Optimization. | Vasco M. Manquinho, Joo Marques-Silva |
| 2005 | ICTAI | Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts. | Vasco M. Manquinho, Joo Marques-Silva |
| 2005 | ICTAI | Good Learning and Implicit Model Enumeration. | Antnio Morgado, Joo Marques-Silva |
| 2005 | SAT | On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization. | Vasco Manquinho, Joo Marques-Silva |
| 2005 | SAT | A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. | Maher N. Mneimneh, Ins Lynce, Zaher S. Andraus, Joo Marques-Silva, Karem A. Sakallah |
| 2004 | ICTAI | Hidden Structure in Unsatisfiable Random 3-SAT: An Empirical Study. | Ins Lynce, Joo Marques-Silva |
| 2004 | ICTAI | Integration of Lower Bound Estimates in Pseudo-Boolean Optimization. | Vasco M. Manquinho, Joo Marques-Silva |
| 2004 | SAT | Using Rewarding Mechanisms for Improving Branching Heuristics. | Elsa Carvalho, Joo Marques-Silva |
| 2004 | SAT | On Computing Minimum Unsatisfiable Cores. | Ins Lynce, Joo Marques-Silva |
| 2004 | SAT | Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization. | Vasco M. Manquinho, Joo Marques-Silva |
| 2003 | EPIA | Heuristic-Based Backtracking for Propositional Satisfiability. | Ateet Bhalla, Ins Lynce, Jos T. de Sousa, Joo Marques-Silva |
| 2003 | ICTAI | Probing-Based Preprocessing Techniques for Propositional Satisfiability. | Ins Lynce, Joo Marques-Silva |
| 2002 | CP | Tuning Randomization in Backtrack Search SAT Algorithms. | Ins Lynce, Joo Marques-Silva |
| 2002 | ECAI | Building State-of-the-Art SAT Solvers. | Ins Lynce, Joo Marques-Silva |
| 2001 | CP | Improving SAT Algorithms by Using Search Pruning Techniques. | Ins Lynce, Joo Marques-Silva |
| 2001 | EPIA | Towards Provably Complete Stochastic Search Algorithms for Satisfiability. | Ins Lynce, Lus Baptista, Joo Marques-Silva |
| 2000 | CAV | Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. | Joo Marques-Silva, Karem A. Sakallah |
| 2000 | CP | Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability. | Lus Baptista, Joo Marques-Silva |
| 2000 | CP | Algebraic Simplification Techniques for Propositional Satisfiability. | Joo Marques-Silva |
| 2000 | DATE | On Using Satisfiability-Based Pruning Techniques in Covering Algorithms. | Vasco M. Manquinho, Joo Marques-Silva |
| 2000 | ECAI | Search Pruning Conditions for Boolean Optimization. | Vasco M. Manquinho, Joo Marques-Silva |
| 1999 | DATE | Combinational Equivalence Checking Using Satisfiability and Recursive Learning. | Joo Marques-Silva, Thomas Glass |
| 1999 | DATE | Algorithms for Solving Boolean Satisfiability in Combinational Circuits. | Lus Guerra e Silva, Lus Miguel Silveira, Joo Marques-Silva |
| 1999 | EPIA | The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. | Joo Marques-Silva |
| 1999 | ISCAS | Test pattern generation for width compression in BIST. | Paulo F. Flores, Horcio C. Neto, Krishnendu Chakrabarty, Joo Marques-Silva |
| 1999 | VLSID | Assignment and Reordering of Incompletely Specified Pattern Sequences Targetting Minimum Power Dissipation. | Paulo F. Flores, Jos C. Costa, Horcio C. Neto, Jos Monteiro, Joo Marques-Silva |