João Marques-Silva

343 papers A* 44A 75B 25C 8Misc 8Journal 133Unranked 44

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Feature Necessity and Relevancy in Machine Learning Explanations. J. Autom. Reason. Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, João Marques-Silva
2026	J	`jnl`	Modelling and optimising switching on a physical binary sorter. Ann. Oper. Res. Josep Maria Salvia Hornos, Cèsar Fernández Camón, Carles Mateu Piñol, João Marques-Silva, Ivet Rafegas Fonoll, Josep Cirera Balcells
2026	J	`jnl`	Rigorous Explanations for Tree Ensembles. CoRR Yacine Izza, Alexey Ignatiev, Xuanxiang Huang, Peter J. Stuckey, João Marques-Silva
2025	J	`jnl`	Efficient & Correct Predictive Equivalence for Decision Trees. CoRR João Marques-Silva, Alexey Ignatiev
2025	A*	`conf`	Efficient and Rigorous Model-Agnostic Explanations. IJCAI João Marques-Silva, Jairo A. Lefebre-Lobaina, Maria Vanina Martinez
2025	—	`conf`	Explanations of Unsatisfiability Beyond Minimal Subsets. JELIA (2) Pablo Martínez-Naredo, Raúl Mencía, João Marques-Silva, Carlos Mencía
2025	—	`conf`	Formal Explanations of Black-Box Ranking Functions. JELIA (1) Francesco Chiariello, João Marques-Silva
2025	J	`jnl`	Most General Explanations of Tree Ensembles (Extended Version). CoRR Yacine Izza, Alexey Ignatiev, Sasha Rubin, João Marques-Silva, Peter J. Stuckey
2025	A*	`conf`	Most General Explanations of Tree Ensembles. IJCAI Yacine Izza, Alexey Ignatiev, Sasha Rubin, João Marques-Silva, Peter J. Stuckey
2025	—	`conf`	On Trustworthy Rule-Based Models and Explanations. ECML/PKDD (4) Mohamed Siala, Jordi Planes, João Marques-Silva
2025	J	`jnl`	On Trustworthy Rule-Based Models and Explanations. CoRR Mohamed Siala, Jordi Planes, João Marques-Silva
2025	J	`jnl`	Rigorous Feature Importance Scores based on Shapley Value and Banzhaf Index. CoRR Xuanxiang Huang, Olivier Létoffé, João Marques-Silva
2025	J	`jnl`	The Explanation Game - Rekindled (Extended Version). CoRR João Marques-Silva, Xuanxiang Huang, Olivier Letoffe
2025	—	`conf`	The Pros and Cons of Adversarial Robustness. ICAART (2) Yacine Izza, João Marques-Silva
2025	A*	`conf`	Towards Trustable SHAP Scores. AAAI Olivier Létoffé, Xuanxiang Huang, João Marques-Silva
2025	J	`jnl`	Uncovering Bugs in Formal Explainers: A Case Study with PyXAI. CoRR Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, João Marques-Silva
2025	—	`conf`	Uncovering and Correcting XAI's Misconceptions Logic to the Rescue. IDEAL (2) João Marques-Silva
2024	A*	`conf`	Delivering Inflated Explanations. AAAI Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, João Marques-Silva
2024	A*	`conf`	Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. KR Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, João Marques-Silva
2024	J	`jnl`	Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. CoRR Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, João Marques-Silva
2024	J	`jnl`	Efficient Contrastive Explanations on Demand. CoRR Yacine Izza, João Marques-Silva
2024	J	`jnl`	Explainability Is Commun. ACM João Marques-Silva, Xuanxiang Huang
2024	J	`jnl`	From SHAP Scores to Feature Importance Scores. CoRR Olivier Letoffe, Xuanxiang Huang, Nicholas Asher, João Marques-Silva
2024	A	`conf`	Locally-Minimal Probabilistic Explanations. ECAI Yacine Izza, Kuldeep S. Meel, João Marques-Silva
2024	J	`jnl`	Logic-Based Explainability: Past, Present & Future. CoRR João Marques-Silva
2024	—	`conf`	Logic-Based Explainability: Past, Present and Future. ISoLA (4) João Marques-Silva
2024	J	`jnl`	On Correcting SHAP Scores. CoRR Olivier Letoffe, Xuanxiang Huang, João Marques-Silva
2024	J	`jnl`	On the failings of Shapley values for explainability. Int. J. Approx. Reason. Xuanxiang Huang, João Marques-Silva
2024	J	`jnl`	Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Gianpiero Cabodi, Paolo E. Camurati, João Marques-Silva, Marco Palena, Paolo Pasini
2024	J	`jnl`	SHAP scores fail pervasively even when Lipschitz succeeds. CoRR Olivier Letoffe, Xuanxiang Huang, João Marques-Silva
2024	J	`jnl`	Synergies between machine learning and reasoning - An introduction by the Kay R. Amel group. Int. J. Approx. Reason. Ismaïl Baaj, Zied Bouraoui, Antoine Cornuéjols, Thierry Denoeux, Sébastien Destercke, Didier Dubois, Marie-Jeanne Lesot, João Marques-Silva, Jérôme Mengin, Henri Prade, Steven Schockaert, Mathieu Serrurier, Olivier Strauss, Christel Vrain
2024	J	`jnl`	The Sets of Power. CoRR João Marques-Silva, Carlos Mencía, Raúl Mencía
2024	A*	`conf`	Updates on the Complexity of SHAP Scores. IJCAI Xuanxiang Huang, João Marques-Silva
2024	J	`jnl`	XAI is in trouble. AI Mag. Rosina O. Weber, Adam J. Johs, Prateek Goel, João Marques-Silva
2023	J	`jnl`	A Refutation of Shapley Values for Explainability. CoRR Xuanxiang Huang, João Marques-Silva
2023	C	`conf`	Certified Logic-Based Explainable AI - The Case of Monotonic Classifiers. TAP Aurélie Hurault, João Marques-Silva
2023	J	`jnl`	Delivering Inflated Explanations. CoRR Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, João Marques-Silva
2023	B	`conf`	Disproving XAI Myths with Formal Methods - Initial Results. ICECCS João Marques-Silva
2023	J	`jnl`	Disproving XAI Myths with Formal Methods - Initial Results. CoRR João Marques-Silva
2023	A*	`conf`	Efficient Reasoning about Infeasible One Machine Sequencing. ICAPS Raúl Mencía, Carlos Mencía, João Marques-Silva
2023	A*	`conf`	Eliminating the Impossible, Whatever Remains Must Be True: On Extracting and Applying Background Knowledge in the Context of Formal Explanations. AAAI Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, Nina Narodytska, João Marques-Silva
2023	J	`jnl`	Explainability is NOT a Game. CoRR João Marques-Silva, Xuanxiang Huang
2023	—	`conf`	Feature Necessity & Relevancy in ML Classifier Explanations. TACAS (1) Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, João Marques-Silva
2023	A	`conf`	From Decision Trees to Explained Decision Sets. ECAI Xuanxiang Huang, João Marques-Silva
2023	J	`jnl`	From Robustness to Explainability and Back Again. CoRR Xuanxiang Huang, João Marques-Silva
2023	J	`jnl`	Locally-Minimal Probabilistic Explanations. CoRR Yacine Izza, Kuldeep S. Meel, João Marques-Silva
2023	J	`jnl`	No silver bullet: interpretable ML models must be explained. Frontiers Artif. Intell. João Marques-Silva, Alexey Ignatiev
2023	—	`conf`	On Computing Relevant Features for Explaining NBCs. ENIGMA@KR Yacine Izza, João Marques-Silva
2023	J	`jnl`	On Logic-Based Explainability with Partially Specified Inputs. CoRR Ramón Béjar, António Morgado, Jordi Planes, João Marques-Silva
2023	A*	`conf`	On Tackling Explanation Redundancy in Decision Trees (Extended Abstract). IJCAI Yacine Izza, Alexey Ignatiev, João Marques-Silva
2023	J	`jnl`	On computing probabilistic abductive explanations. Int. J. Approx. Reason. Yacine Izza, Xuanxiang Huang, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, João Marques-Silva
2023	J	`jnl`	Refutation of Shapley Values for XAI - Additional Evidence. CoRR Xuanxiang Huang, João Marques-Silva
2023	A*	`conf`	Solving Explainability Queries with Quantification: The Case of Feature Relevancy. AAAI Xuanxiang Huang, Yacine Izza, João Marques-Silva
2023	J	`jnl`	The Inadequacy of Shapley Values for Explainability. CoRR Xuanxiang Huang, João Marques-Silva
2023	J	`jnl`	The Pros and Cons of Adversarial Robustness. CoRR Yacine Izza, João Marques-Silva
2023	J	`jnl`	Tractability of explaining classifier decisions. Artif. Intell. Martin C. Cooper, João Marques-Silva
2023	A*	`conf`	Tractable Explaining of Multivariate Decision Trees. KR Clément Carbonnel, Martin C. Cooper, João Marques-Silva
2022	A*	`conf`	Constraint-Driven Explanations for Black-Box ML Models. AAAI Aditya A. Shrotri, Nina Narodytska, Alexey Ignatiev, Kuldeep S. Meel, João Marques-Silva, Moshe Y. Vardi
2022	A*	`conf`	Delivering Trustworthy AI through Formal XAI. AAAI João Marques-Silva, Alexey Ignatiev
2022	J	`jnl`	Eliminating The Impossible, Whatever Remains Must Be True. CoRR Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, Nina Narodytska, João Marques-Silva
2022	J	`jnl`	Feature Necessity & Relevancy in ML Classifier Explanations. CoRR Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, João Marques-Silva
2022	—	`conf`	Logic-Based Explainability in Machine Learning. RW João Marques-Silva
2022	J	`jnl`	Logic-Based Explainability in Machine Learning. CoRR João Marques-Silva
2022	J	`jnl`	On Computing Probabilistic Abductive Explanations. CoRR Yacine Izza, Xuanxiang Huang, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, João Marques-Silva
2022	J	`jnl`	On Computing Relevant Features for Explaining NBCs. CoRR Yacine Izza, João Marques-Silva
2022	J	`jnl`	On Deciding Feature Membership in Explanations of SDD & Related Classifiers. CoRR Xuanxiang Huang, João Marques-Silva
2022	J	`jnl`	On Tackling Explanation Redundancy in Decision Trees. CoRR Yacine Izza, Alexey Ignatiev, João Marques-Silva
2022	J	`jnl`	On Tackling Explanation Redundancy in Decision Trees. J. Artif. Intell. Res. Yacine Izza, Alexey Ignatiev, João Marques-Silva
2022	J	`jnl`	Provably Precise, Succinct and Efficient Explanations for Decision Trees. CoRR Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, João Marques-Silva
2022	A*	`conf`	Tractable Explanations for d-DNNF Classifiers. AAAI Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, João Marques-Silva
2022	A*	`conf`	Using MaxSAT for Efficient Explanations of Tree Ensembles. AAAI Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, João Marques-Silva
2021	A*	`conf`	A Scalable Two Stage Approach to Computing Optimal Decision Sets. AAAI Alexey Ignatiev, Edward Lam, Peter J. Stuckey, João Marques-Silva
2021	J	`jnl`	A Scalable Two Stage Approach to Computing Optimal Decision Sets. CoRR Alexey Ignatiev, Edward Lam, Peter J. Stuckey, João Marques-Silva
2021	A	`conf`	Assessing Progress in SAT Solvers Through the Lens of Incremental SAT. SAT Stepan Kochemazov, Alexey Ignatiev, João Marques-Silva
2021	J	`jnl`	Auditing static machine learning anti-Malware tools against metamorphic attacks. Comput. Secur. Daniel Gibert, Carles Mateu, Jordi Planes, João Marques-Silva
2021	—	`conf`	Automated Reasoning in Explainable AI. CCIA João Marques-Silva
2021	—	`ch.`	Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability João Marques-Silva, Inês Lynce, Sharad Malik
2021	J	`jnl`	Efficient Explanations With Relevant Sets. CoRR Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, João Marques-Silva
2021	J	`jnl`	Efficient Explanations for Knowledge Compilation Languages. CoRR Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, João Marques-Silva
2021	A*	`conf`	Explanations for Monotonic Classifiers. ICML João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska
2021	J	`jnl`	Explanations for Monotonic Classifiers. CoRR João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska
2021	J	`jnl`	Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361). Dagstuhl Reports João Marques-Silva, Rafael Peñaloza, Uli Sattler
2021	J	`jnl`	MILP for the Multi-objective VM Reassignment Problem. CoRR Takfarinas Saber, Anthony Ventresque, João Marques-Silva, James Thorburn, Liam Murphy
2021	A*	`conf`	On Efficiently Explaining Graph-Based Classifiers. KR Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, João Marques-Silva
2021	J	`jnl`	On Efficiently Explaining Graph-Based Classifiers. CoRR Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, João Marques-Silva
2021	A*	`conf`	On Explaining Random Forests with SAT. IJCAI Yacine Izza, João Marques-Silva
2021	J	`jnl`	On Explaining Random Forests with SAT. CoRR Yacine Izza, João Marques-Silva
2021	A	`conf`	On the Tractability of Explaining Decisions of Classifiers. CP Martin C. Cooper, João Marques-Silva
2021	A	`conf`	Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. DATE Gianpiero Cabodi, Paolo E. Camurati, Alexey Ignatiev, João Marques-Silva, Marco Palena, Paolo Pasini
2021	J	`jnl`	Propositional proof systems based on maximum satisfiability. Artif. Intell. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, António Morgado, João Marques-Silva
2021	A*	`conf`	Reasoning-Based Learning of Interpretable ML Models. IJCAI Alexey Ignatiev, João Marques-Silva, Nina Narodytska, Peter J. Stuckey
2021	A	`conf`	SAT-Based Rigorous Explanations for Decision Lists. SAT Alexey Ignatiev, João Marques-Silva
2021	J	`jnl`	SAT-Based Rigorous Explanations for Decision Lists. CoRR Alexey Ignatiev, João Marques-Silva
2020	A	`conf`	Branch Location Problems with Maximum Satisfiability. ECAI Oleg Zaikin, Alexey Ignatiev, João Marques-Silva
2020	A*	`conf`	Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay. NeurIPS João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska
2020	J	`jnl`	Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay. CoRR João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska
2020	—	`conf`	From Contrastive to Abductive Explanations and Back Again. AI*IA Alexey Ignatiev, Nina Narodytska, Nicholas Asher, João Marques-Silva
2020	J	`jnl`	On Explaining Decision Trees. CoRR Yacine Izza, Alexey Ignatiev, João Marques-Silva
2020	J	`jnl`	On Relating 'Why?' and 'Why Not?' Explanations. CoRR Alexey Ignatiev, Nina Narodytska, Nicholas Asher, João Marques-Silva
2020	J	`jnl`	Optimum stable model search: algorithms and implementation. J. Log. Comput. Mario Alviano, Carmine Dodaro, João Marques-Silva, Francesco Ricca
2020	A*	`conf`	Reasoning About Inconsistent Formulas. IJCAI João Marques-Silva, Carlos Mencía
2020	A	`conf`	Reasoning About Strong Inconsistency in ASP. SAT Carlos Mencía, João Marques-Silva
2020	A	`conf`	Towards Formal Fairness in Machine Learning. CP Alexey Ignatiev, Martin C. Cooper, Mohamed Siala, Emmanuel Hebrard, João Marques-Silva
2019	A*	`conf`	Abduction-Based Explanations for Machine Learning Models. AAAI Alexey Ignatiev, Nina Narodytska, João Marques-Silva
2019	A	`conf`	Assessing Heuristic Machine Learning Explanations with Model Counting. SAT Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, João Marques-Silva
2019	—	`conf`	Computing Shortest Resolution Proofs. EPIA (2) Carlos Mencía, João Marques-Silva
2019	A	`conf`	DRMaxSAT with MaxHS: First Contact. SAT António Morgado, Alexey Ignatiev, Maria Luisa Bonet, João Marques-Silva, Sam Buss
2019	C	`conf`	Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference. LATA Ilya Zakirzyanov, António Morgado, Alexey Ignatiev, Vladimir Ulyantsev, João Marques-Silva
2019	J	`jnl`	Formally Verifying the Solution to the Boolean Pythagorean Triples Problem. J. Autom. Reason. Luís Cruz-Filipe, João Marques-Silva, Peter Schneider-Kamp
2019	J	`jnl`	From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group). CoRR Zied Bouraoui, Antoine Cornuéjols, Thierry Denoeux, Sébastien Destercke, Didier Dubois, Romain Guillaume, João Marques-Silva, Jérôme Mengin, Henri Prade, Steven Schockaert, Mathieu Serrurier, Christel Vrain
2019	A*	`conf`	Model-Based Diagnosis with Multiple Observations. IJCAI Alexey Ignatiev, António Morgado, Georg Weissenbacher, João Marques-Silva
2019	A	`conf`	On Computing the Union of MUSes. SAT Carlos Mencía, Oliver Kullmann, Alexey Ignatiev, João Marques-Silva
2019	A*	`conf`	On Relating Explanations and Adversarial Examples. NeurIPS Alexey Ignatiev, Nina Narodytska, João Marques-Silva
2019	J	`jnl`	On Validating, Repairing and Refining Heuristic ML Explanations. CoRR Alexey Ignatiev, Nina Narodytska, João Marques-Silva
2019	J	`jnl`	RC2: an Efficient MaxSAT Solver. J. Satisf. Boolean Model. Comput. Alexey Ignatiev, António Morgado, João Marques-Silva
2018	A	`conf`	A SAT-Based Approach to Learn Explainable Decision Sets. IJCAR Alexey Ignatiev, Filipe Pereira, Nina Narodytska, João Marques-Silva
2018	J	`jnl`	Abduction-Based Explanations for Machine Learning Models. CoRR Alexey Ignatiev, Nina Narodytska, João Marques-Silva
2018	C	`conf`	Computing with SAT Oracles: Past, Present and Future. CiE João Marques-Silva
2018	A*	`conf`	Learning Optimal Decision Trees with SAT. IJCAI Nina Narodytska, Alexey Ignatiev, Filipe Pereira, João Marques-Silva
2018	A*	`conf`	MaxSAT Resolution With the Dual Rail Encoding. AAAI Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, António Morgado
2018	A*	`conf`	Premise Set Caching for Enumerating Minimal Correction Subsets. AAAI Alessandro Previti, Carlos Mencía, Matti Järvisalo, João Marques-Silva
2018	—	`ch.`	Propositional SAT Solving. Handbook of Model Checking João Marques-Silva, Sharad Malik
2018	A	`conf`	PySAT: A Python Toolkit for Prototyping with SAT Oracles. SAT Alexey Ignatiev, António Morgado, João Marques-Silva
2017	Misc	`conf`	An Achilles' Heel of Term-Resolution. EPIA Mikolás Janota, João Marques-Silva
2017	A*	`conf`	Cardinality Encodings for Graph Optimization Problems. IJCAI Alexey Ignatiev, António Morgado, João Marques-Silva
2017	—	`conf`	Debugging EL+ Ontologies through Horn MUS Enumeration. Description Logics Alexey Ignatiev, João Marques-Silva, Carlos Mencía, Rafael Peñaloza
2017	—	`conf`	Efficient Certified Resolution Proof Checking. TACAS (1) Luís Cruz-Filipe, João Marques-Silva, Peter Schneider-Kamp
2017	J	`jnl`	Exact and Hybrid Solutions for the Multi-Objective VM Reassignment Problem. Int. J. Artif. Intell. Tools Takfarinas Saber, João Marques-Silva, James Thorburn, Anthony Ventresque
2017	J	`jnl`	Horn Maximum Satisfiability: Reductions, Algorithms & Applications. CoRR João Marques-Silva, Alexey Ignatiev, António Morgado
2017	Misc	`conf`	Horn Maximum Satisfiability: Reductions, Algorithms and Applications. EPIA João Marques-Silva, Alexey Ignatiev, António Morgado
2017	A	`conf`	Improving MCS Enumeration via Caching. SAT Alessandro Previti, Carlos Mencía, Matti Järvisalo, João Marques-Silva
2017	—	`conf`	Lean Kernels in Description Logics. ESWC (1) Rafael Peñaloza, Carlos Mencía, Alexey Ignatiev, João Marques-Silva
2017	J	`jnl`	Minimal sets on propositional formulae. Problems and reductions. Artif. Intell. João Marques-Silva, Mikolás Janota, Carlos Mencía
2017	J	`jnl`	Model Based Diagnosis of Multiple Observations with Implicit Hitting Sets. CoRR Alexey Ignatiev, António Morgado, João Marques-Silva
2017	B	`conf`	On Computing Generalized Backbones. ICTAI Alessandro Previti, Alexey Ignatiev, Matti Järvisalo, João Marques-Silva
2017	—	`conf`	On Minimal Corrections in ASP. RCRA@AI*IA Mikolás Janota, João Marques-Silva
2017	A	`conf`	On Tackling the Limits of Resolution in SAT Solving. SAT Alexey Ignatiev, António Morgado, João Marques-Silva
2017	J	`jnl`	On Tackling the Limits of Resolution in SAT Solving. CoRR Alexey Ignatiev, António Morgado, João Marques-Silva
2016	A	`conf`	BEACON: An Efficient SAT-Based Tool for Debugging SAT M. Fareed Arif, Carlos Mencía, Alexey Ignatiev, Norbert Manthey, Rafael Peñaloza, João Marques-Silva
2016	J	`jnl`	Efficient Certified Resolution Proof Checking. CoRR Luís Cruz-Filipe, João Marques-Silva, Peter Schneider-Kamp
2016	B	`conf`	Efficient Reasoning for Inconsistent Horn Formulae. JELIA João Marques-Silva, Alexey Ignatiev, Carlos Mencía, Rafael Peñaloza
2016	J	`jnl`	Fast, flexible MUS enumeration. Constraints An Int. J. Mark H. Liffiton, Alessandro Previti, Ammar Malik, João Marques-Silva
2016	A	`conf`	MCS Extraction with Sublinear Oracle Queries. SAT Carlos Mencía, Alexey Ignatiev, Alessandro Previti, João Marques-Silva
2016	J	`jnl`	Maximal falsifiability. AI Commun. Alexey Ignatiev, António Morgado, Jordi Planes, João Marques-Silva
2016	A	`conf`	On Finding Minimum Satisfying Assignments. CP Alexey Ignatiev, Alessandro Previti, João Marques-Silva
2016	J	`jnl`	On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell. Mikolás Janota, João Marques-Silva
2016	—	`conf`	Preface: The Beyond NP Workshop. AAAI Workshop: Beyond NP Adnan Darwiche, João Marques-Silva, Pierre Marquis
2016	A	`conf`	Propositional Abduction with Implicit Hitting Sets. ECAI Alexey Ignatiev, António Morgado, João Marques-Silva
2016	J	`jnl`	Propositional Abduction with Implicit Hitting Sets. CoRR Alexey Ignatiev, António Morgado, João Marques-Silva
2016	J	`jnl`	Quantified maximum satisfiability. Constraints An Int. J. Alexey Ignatiev, Mikolás Janota, João Marques-Silva
2016	J	`jnl`	Reports of the 2016 AAAI Workshop Program. AI Mag. Stefano V. Albrecht, Bruno Bouchard, John S. Brownstein, David L. Buckeridge, Cornelia Caragea, Kevin M. Carter, Adnan Darwiche, Blaz Fortuna, Yannick Francillette, Sébastien Gaboury, C. Lee Giles, Marko Grobelnik, Estevam R. Hruschka Jr., Jeffrey O. Kephart, Parisa Kordjamshidi, Viliam Lisý, Daniele Magazzeni, João Marques-Silva, Pierre Marquis, David R. Martinez, Marek P. Michalowski, Arash Shaban-Nejad, Zeinab Noorian, Enrico Pontelli, Alex Rogers, Stephanie Rosenthal, Dan Roth, Arunesh Sinha, William W. Streilein, Sylvie Thiébaux, Tran Cao Son, Byron C. Wallace, Toby Walsh, Michael Witbrock, Jie Zhang
2016	J	`jnl`	Solving QBF with counterexample guided refinement. Artif. Intell. Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
2015	J	`jnl`	Algorithms for computing backbones of propositional formulae. AI Commun. Mikolás Janota, Inês Lynce, João Marques-Silva
2015	A	`conf`	Computing Maximal Autarkies with Few and Simple Oracle Queries. SAT Oliver Kullmann, João Marques-Silva
2015	J	`jnl`	Computing maximal autarkies with few and simple oracle queries. CoRR Oliver Kullmann, João Marques-Silva
2015	Misc	`conf`	Efficient Axiom Pinpointing with EL2MCS. KI M. Fareed Arif, Carlos Mencía, João Marques-Silva
2015	A	`conf`	Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing. SAT M. Fareed Arif, Carlos Mencía, João Marques-Silva
2015	J	`jnl`	Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing. CoRR M. Fareed Arif, Carlos Mencía, João Marques-Silva
2015	A*	`conf`	Efficient Model Based Diagnosis with Maximum Satisfiability. IJCAI João Marques-Silva, Mikolás Janota, Alexey Ignatiev, António Morgado
2015	J	`jnl`	Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. Mikolás Janota, João Marques-Silva
2015	A*	`conf`	Literal-Based MCS Extraction. IJCAI Carlos Mencía, Alessandro Previti, João Marques-Silva
2015	B	`conf`	MILP for the Multi-objective VM Reassignment Problem. ICTAI Takfarinas Saber, Anthony Ventresque, João Marques-Silva, James Thorburn, Liam Murphy
2015	J	`jnl`	MaxSAT-based encodings for Group MaxSAT. AI Commun. Federico Heras, António Morgado, João Marques-Silva
2015	A*	`conf`	Prime Compilation of Non-Clausal Formulae. IJCAI Alessandro Previti, Alexey Ignatiev, António Morgado, João Marques-Silva
2015	A	`conf`	SAT-Based Formula Simplification. SAT Alexey Ignatiev, Alessandro Previti, João Marques-Silva
2015	A	`conf`	SAT-Based Horn Least Upper Bounds. SAT Carlos Mencía, Alessandro Previti, João Marques-Silva
2015	A	`conf`	Smallest MUS Extraction with Minimal Hitting Set Dualization. CP Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, João Marques-Silva
2015	A*	`conf`	Solving QBF by Clause Selection. IJCAI Mikolás Janota, João Marques-Silva
2015	J	`jnl`	Towards Efficient Axiom Pinpointing of EL+ Ontologies. CoRR M. Fareed Arif, João Marques-Silva
2014	B	`conf`	A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. CPAIOR Yuri Malitsky, Barry O'Sullivan, Alessandro Previti, João Marques-Silva
2014	J	`jnl`	Algorithms for computing minimal equivalent subformulas. Artif. Intell. Anton Belov, Mikolás Janota, Inês Lynce, João Marques-Silva
2014	J	`jnl`	Computing Minimal Sets on Propositional Formulae I: Problems & Reductions. CoRR João Marques-Silva, Mikolás Janota
2014	A	`conf`	Core-Guided MaxSAT with Soft Cardinality Constraints. CP António Morgado, Carmine Dodaro, João Marques-Silva
2014	A	`conf`	Efficient Autarkies. ECAI João Marques-Silva, Alexey Ignatiev, António Morgado, Vasco Manquinho, Inês Lynce
2014	B	`conf`	Efficient Relaxations of Over-constrained CSPs. ICTAI Carlos Mencía, João Marques-Silva
2014	B	`conf`	Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form. JELIA Saïd Jabbour, João Marques-Silva, Lakhdar Sais, Yakoub Salhi
2014	J	`jnl`	MSCG: Robust Core-Guided MaxSAT Solving. J. Satisf. Boolean Model. Comput. António Morgado, Alexey Ignatiev, João Marques-Silva
2014	A	`conf`	MUS Extraction Using Clausal Proofs. SAT Anton Belov, Marijn Heule, João Marques-Silva
2014	A	`conf`	On Computing Preferred MUSes and MCSes. SAT João Marques-Silva, Alessandro Previti
2014	J	`jnl`	On Minimal Corrections in ASP. CoRR Mikolás Janota, João Marques-Silva
2014	A	`conf`	On Reducing Maximum Independent Set to Minimum Satisfiability. SAT Alexey Ignatiev, António Morgado, João Marques-Silva
2014	—	`conf`	On lazy and eager interactive reconfiguration. VaMoS Mikolás Janota, Goetz Botterweck, João Marques-Silva
2014	J	`jnl`	On the Query Complexity of Selecting Few Minimal Sets. Electron. Colloquium Comput. Complex. João Marques-Silva, Mikolás Janota
2014	A	`conf`	Progression in Maximum Satisfiability. ECAI Alexey Ignatiev, António Morgado, Vasco Manquinho, Inês Lynce, João Marques-Silva
2014	—	`ch.`	SAT Solvers. Tractability João Marques-Silva, Inês Lynce
2014	A	`conf`	Synthesizing Safe Bit-Precise Invariants. TACAS Arie Gurfinkel, Anton Belov, João Marques-Silva
2014	A	`conf`	Timeout-Sensitive Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. ECAI Yuri Malitsky, Barry O'Sullivan, Alessandro Previti, João Marques-Silva
2014	A*	`conf`	Towards efficient optimization in package management systems. ICSE Alexey Ignatiev, Mikolás Janota, João Marques-Silva
2013	J	`jnl`	A Two-Variable Model for SAT-Based ATPG. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Huan Chen, João Marques-Silva
2013	A	`conf`	Core minimization in SAT-based abstraction. DATE Anton Belov, Huan Chen, Alan Mishchenko, João Marques-Silva
2013	A	`conf`	Formula Preprocessing in MUS Extraction. TACAS Anton Belov, Matti Järvisalo, João Marques-Silva
2013	J	`jnl`	Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J. António Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, João Marques-Silva
2013	B	`conf`	Maximal Falsifiability - Definitions, Algorithms, and Applications. LPAR Alexey Ignatiev, António Morgado, Jordi Planes, João Marques-Silva
2013	A*	`conf`	Minimal Sets over Monotone Predicates in Boolean Formulae. CAV João Marques-Silva, Mikolás Janota, Anton Belov
2013	B	`conf`	Model-Guided Approaches for MaxSAT Solving. ICTAI António Morgado, Federico Heras, João Marques-Silva
2013	A*	`conf`	On Computing Minimal Correction Subsets. IJCAI João Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, Anton Belov
2013	A	`conf`	On Propositional QBF Expansions and Q-Resolution. SAT Mikolás Janota, João Marques-Silva
2013	J	`jnl`	On Propositional QBF Expansions and Q-Resolution. Electron. Colloquium Comput. Complex. Mikolás Janota, João Marques-Silva
2013	B	`conf`	On QBF Proofs and Preprocessing. LPAR Mikolás Janota, Radu Grigore, João Marques-Silva
2013	J	`jnl`	On QBF Proofs and Preprocessing. CoRR Mikolás Janota, Radu Grigore, João Marques-Silva
2013	A	`conf`	Parallel MUS Extraction. SAT Anton Belov, Norbert Manthey, João Marques-Silva
2013	A*	`conf`	Partial MUS Enumeration. AAAI Alessandro Previti, João Marques-Silva
2013	A	`conf`	Quantified Maximum Satisfiability: - A Core-Guided Approach. SAT Alexey Ignatiev, Mikolás Janota, João Marques-Silva
2013	B	`conf`	SAT-Based Preprocessing for MaxSAT. LPAR Anton Belov, António Morgado, João Marques-Silva
2013	J	`jnl`	SAT-based Preprocessing for MaxSAT (extended version). CoRR Anton Belov, António Morgado, João Marques-Silva
2013	A	`conf`	Solving QBF with Free Variables. CP William Klieber, Mikolás Janota, João Marques-Silva, Edmund M. Clarke
2012	—	`conf`	An Empirical Study of Encodings for Group MaxSAT. Canadian AI Federico Heras, António Morgado, João Marques-Silva
2012	J	`jnl`	Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions. J. Multiple Valued Log. Soft Comput. João Marques-Silva
2012	J	`jnl`	Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality CoRR Anton Belov, João Marques-Silva
2012	J	`jnl`	Hybrid Incremental Algorithms for Boolean Satisfiability. Int. J. Artif. Intell. Tools Florian Letombe, João Marques-Silva
2012	A	`conf`	Improvements to Core-Guided Binary Search for MaxSAT. SAT António Morgado, Federico Heras, João Marques-Silva
2012	B	`conf`	Iterative SAT Solving for Minimum Satisfiability. ICTAI Federico Heras, António Morgado, Jordi Planes, João Marques-Silva
2012	B	`conf`	Knowledge Compilation with Empowerment. SOFSEM Lucas Bordeaux, João Marques-Silva
2012	—	`conf`	Lower Bounds and Upper Bounds for MaxSAT. LION Federico Heras, António Morgado, João Marques-Silva
2012	J	`jnl`	MUSer2: An Efficient MUS Extractor. J. Satisf. Boolean Model. Comput. Anton Belov, João Marques-Silva
2012	—	`conf`	MaxSAT-Based MCS Enumeration. Haifa Verification Conference António Morgado, Mark H. Liffiton, João Marques-Silva
2012	—	`conf`	New & improved models for SAT-based bi-decomposition. ACM Great Lakes Symposium on VLSI Huan Chen, João Marques-Silva
2012	A	`conf`	On Computing Minimal Equivalent Subformulas. CP Anton Belov, Mikolás Janota, Inês Lynce, João Marques-Silva
2012	A	`conf`	On Efficient Computation of Variable MUSes. SAT Anton Belov, Alexander Ivrii, Arie Matsliah, João Marques-Silva
2012	A*	`conf`	On Unit-Refutation Complete Formulae with Existentially Quantified Variables. KR Lucas Bordeaux, Mikolás Janota, João Marques-Silva, Pierre Marquis
2012	J	`jnl`	PackUp: Tools for Package Upgradability Solving. J. Satisf. Boolean Model. Comput. Mikolás Janota, Inês Lynce, Vasco Manquinho, João Marques-Silva
2012	A	`conf`	QBf-based boolean function bi-decomposition. DATE Huan Chen, Mikolás Janota, João Marques-Silva
2012	J	`jnl`	SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Trans. Software Eng. Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva
2012	A	`conf`	Solving QBF with Counterexample Guided Refinement. SAT Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
2012	J	`jnl`	TG-Pro: A SAT-based ATPG System. J. Satisf. Boolean Model. Comput. Huan Chen, João Marques-Silva
2012	J	`jnl`	Towards efficient MUS extraction. AI Commun. Anton Belov, Inês Lynce, João Marques-Silva
2011	A	`conf`	Abstraction-Based Algorithm for 2QBF. SAT Mikolás Janota, João Marques-Silva
2011	B	`conf`	Accelerating MUS extraction with recursive model rotation. FMCAD Anton Belov, João Marques-Silva
2011	J	`jnl`	Anatomy and Empirical Evaluation of Modern SAT Solvers. Bull. EATCS Karem A. Sakallah, João Marques-Silva
2011	J	`jnl`	Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. João Marques-Silva, Josep Argelich, Ana Graça, Inês Lynce
2011	A*	`conf`	Core-Guided Binary Search Algorithms for Maximum Satisfiability. AAAI Federico Heras, António Morgado, João Marques-Silva
2011	—	`ch.`	Haplotype Inference Using Propositional Satisfiability. Mathematical Approaches to Polymer Sequence Analysis and Related Problems Ana Graça, João Marques-Silva, Inês Lynce
2011	J	`jnl`	Haplotype inference with pseudo-Boolean optimization. Ann. Oper. Res. Ana Graça, João Marques-Silva, Inês Lynce, Arlindo L. Oliveira
2011	—	`conf`	Improvements to Satisfiability-Based Boolean Function Bi-Decomposition. VLSI-SoC (Selected Papers) Huan Chen, João Marques-Silva
2011	C	`conf`	Improvements to satisfiability-based boolean function bi-decomposition. VLSI-SoC Huan Chen, João Marques-Silva
2011	—	`conf`	Lazy Decomposition for Distributed Decision Procedures PDMC Youssef Hamadi, João Marques-Silva, Christoph M. Wintersteiger
2011	A	`conf`	Minimally Unsatisfiable Boolean Circuits. SAT Anton Belov, João Marques-Silva
2011	A	`conf`	On Deciding MUS Membership with QBF. CP Mikolás Janota, João Marques-Silva
2011	A	`conf`	On Improving MUS Extraction Algorithms. SAT João Marques-Silva, Inês Lynce
2011	J	`jnl`	On Validating Boolean Optimizers CoRR António Morgado, João Marques-Silva
2011	B	`conf`	On Validating Boolean Optimizers. ICTAI António Morgado, João Marques-Silva
2011	J	`jnl`	QBF-Based Boolean Function Bi-Decomposition CoRR Huan Chen, Mikolás Janota, João Marques-Silva
2011	A*	`conf`	Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms. IJCAI Federico Heras, João Marques-Silva
2011	J	`jnl`	Restoring CSP Satisfiability with MaxSAT. Fundam. Informaticae Inês Lynce, João Marques-Silva
2011	B	`conf`	cmMUS: A Tool for Circumscription-Based MUS Membership Testing. LPNMR Mikolás Janota, João Marques-Silva
2010	J	`jnl`	Automated Design Debugging With Maximum Satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Yibin Chen, Sean Safarpour, João Marques-Silva, Andreas G. Veneris
2010	—	`conf`	Boolean Lexicographic Optimization. RCRA@CPAIOR João Marques-Silva, Josep Argelich, Ana Graça, Inês Lynce
2010	J	`jnl`	Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem. Fundam. Informaticae António Morgado, João Marques-Silva
2010	—	`conf`	Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking. ECBS Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva
2010	J	`jnl`	Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription CoRR Mikolás Janota, João Marques-Silva, Radu Grigore
2010	B	`conf`	Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. JELIA Mikolás Janota, Radu Grigore, João Marques-Silva
2010	—	`conf`	Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information. ANB Ana Graça, Inês Lynce, João Marques-Silva, Arlindo L. Oliveira
2010	J	`jnl`	Haplotype Inference by Pure Parsimony: A Survey. J. Comput. Biol. Ana Graça, Inês Lynce, João Marques-Silva, Arlindo L. Oliveira
2010	B	`conf`	How to Complete an Interactive Configuration Process? SOFSEM Mikolás Janota, Goetz Botterweck, Radu Grigore, João Marques-Silva
2010	C	`conf`	Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking. ICTAC Ashish Darbari, Bernd Fischer, João Marques-Silva
2010	—	`conf`	Minimal Unsatisfiability: Models, Algorithms and Applications (Invited Paper). ISMVL João Marques-Silva
2010	A	`conf`	On Computing Backbones of Propositional Theories. ECAI João Marques-Silva, Mikolás Janota, Inês Lynce
2010	—	`conf`	Solving Linux Upgradeability Problems Using Boolean Optimization LoCoCo Josep Argelich, Daniel Le Berre, Inês Lynce, João Marques-Silva, Pascal Rapicault
2009	C	`conf`	A Lazy Unbounded Model Checker for Event-B. ICFEM Paulo J. Matos, Bernd Fischer, João Marques-Silva
2009	J	`jnl`	A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints An Int. J. Mark H. Liffiton, Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva, Karem A. Sakallah
2009	J	`jnl`	Algorithms for Weighted Boolean Optimization CoRR Vasco Manquinho, João Marques-Silva, Jordi Planes
2009	A	`conf`	Algorithms for Weighted Boolean Optimization. SAT Vasco Manquinho, João Marques-Silva, Jordi Planes
2009	J	`jnl`	Algorithms for finding dispensable variables CoRR Mikolás Janota, João Marques-Silva, Radu Grigore
2009	—	`ch.`	Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability João Marques-Silva, Inês Lynce, Sharad Malik
2009	J	`jnl`	Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking CoRR Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva
2009	J	`jnl`	How to Complete an Interactive Configuration Process? CoRR Mikolás Janota, Goetz Botterweck, Radu Grigore, João Marques-Silva
2009	J	`jnl`	Industrial-Strength Formally Certified SAT Solving CoRR Ashish Darbari, Bernd Fischer, João Marques-Silva
2009	J	`jnl`	On Solving Boolean Multilevel Optimization Problems CoRR Josep Argelich, Inês Lynce, João Marques-Silva
2009	A*	`conf`	On Solving Boolean Multilevel Optimization Problemse. IJCAI Josep Argelich, Inês Lynce, João Marques-Silva
2009	—	`conf`	Restoring CSP Satisfiability with MaxSAT. RCRA@AI*IA Inês Lynce, João Marques-Silva
2009	J	`jnl`	SMT-Based Bounded Model Checking for Embedded ANSI-C Software CoRR Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva
2009	A*	`conf`	SMT-Based Bounded Model Checking for Embedded ANSI-C Software. ASE Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva
2009	—	`conf`	Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. ICESS Lucas C. Cordeiro, Bernd Fischer, Huan Chen, João Marques-Silva
2009	—	`conf`	Spatial and temporal design debug using partial MaxSAT. ACM Great Lakes Symposium on VLSI Yibin Chen, Sean Safarpour, Andreas G. Veneris, João Marques-Silva
2009	—	`conf`	TG-PRO: A new model for SAT-based ATPG. HLDVT Huan Chen, João Marques-Silva
2008	A	`conf`	A MAX-SAT Algorithm Portfolio. ECAI Paulo J. Matos, Jordi Planes, Florian Letombe, João Marques-Silva
2008	J	`jnl`	A Pseudo-Boolean Solution to the Maximum Quartet Consistency Problem CoRR António Morgado, João Marques-Silva
2008	A	`conf`	Algorithms for Maximum Satisfiability using Unsatisfiable Cores. DATE João Marques-Silva, Jordi Planes
2008	—	`ch.`	Backtracking. Wiley Encyclopedia of Computer Science and Engineering Inês Lynce, Vasco Manquinho, João Marques-Silva
2008	J	`jnl`	Boosting Haplotype Inference with Local Search. Constraints An Int. J. Inês Lynce, João Marques-Silva, Steve Prestwich
2008	—	`conf`	Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem. RCRA António Morgado, João Marques-Silva
2008	B	`conf`	Efficient Haplotype Inference with Combined CP and OR Techniques. CPAIOR Ana Graça, João Marques-Silva, Inês Lynce, Arlindo L. Oliveira
2008	—	`conf`	Haplotype Inference with Boolean Constraint Solving: An Overview. ICTAI (1) Inês Lynce, Ana Graça, João Marques-Silva, Arlindo L. Oliveira
2008	J	`jnl`	Haplotype Inference with Boolean Satisfiability. Int. J. Artif. Intell. Tools Inês Lynce, João Marques-Silva
2008	A	`conf`	Improvements to Hybrid Incremental SAT Algorithms. SAT Florian Letombe, João Marques-Silva
2008	J	`jnl`	Model Checking Event-B by Encoding into Alloy CoRR Paulo J. Matos, João Marques-Silva
2008	C	`conf`	Model Checking Event-B by Encoding into Alloy. ABZ Paulo J. Matos, João Marques-Silva
2008	J	`jnl`	Model checking with Boolean Satisfiability. J. Algorithms João Marques-Silva
2008	Misc	`conf`	On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization. FLAIRS Federico Heras, Vasco Manquinho, João Marques-Silva
2008	J	`jnl`	Symmetry Breaking for Maximum Satisfiability CoRR João Marques-Silva, Inês Lynce, Vasco Manquinho
2008	B	`conf`	Symmetry Breaking for Maximum Satisfiability. LPAR João Marques-Silva, Inês Lynce, Vasco Manquinho
2008	A	`conf`	Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms. SAT João Marques-Silva, Vasco Manquinho
2007	A	`conf`	Breaking Symmetries in SAT Matrix Models. SAT Inês Lynce, João Marques-Silva
2007	—	`conf`	Efficient Haplotype Inference with Pseudo-boolean Optimization. AB Ana Graça, João Marques-Silva, Inês Lynce, Arlindo L. Oliveira
2007	—	`conf`	Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony Using Delayed Haplotype Selection. EPIA Workshops João Marques-Silva, Inês Lynce, Ana Graça, Arlindo L. Oliveira
2007	J	`jnl`	On Using Unsatisfiability for Solving Maximum Satisfiability CoRR João Marques-Silva, Jordi Planes
2007	J	`jnl`	Random backtracking in backtrack search algorithms for satisfiability. Discret. Appl. Math. Inês Lynce, João Marques-Silva
2007	J	`jnl`	Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing. AI Mag. João Marques-Silva, Karem A. Sakallah, Inês Lynce
2007	A	`ed.`	Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings SAT João Marques-Silva, Karem A. Sakallah
2007	C	`conf`	Towards Equivalence Checking Between TLM and RTL Models. MEMOCODE Nicola Bombieri, Franco Fummi, Graziano Pravadelli, João Marques-Silva
2007	A	`conf`	Towards Robust CNF Encodings of Cardinality Constraints. CP João Marques-Silva, Inês Lynce
2006	A	`conf`	Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel. SAT Oliver Kullmann, Inês Lynce, João Marques-Silva
2006	A	`conf`	Counting Models in Integer Domains. SAT António Morgado, Paulo J. Matos, Vasco Manquinho, João Marques-Silva
2006	A*	`conf`	Efficient Haplotype Inference with Boolean Satisfiability. AAAI Inês Lynce, João Marques-Silva
2006	—	`conf`	Interpolant Learning and Reuse in SAT-Based Model Checking. BMC@FLoC João Marques-Silva
2006	J	`jnl`	On Using Cutting Planes in Pseudo-Boolean Optimization. J. Satisf. Boolean Model. Comput. Vasco M. Manquinho, João Marques-Silva
2006	A	`conf`	SAT in Bioinformatics: Making the Case with Haplotype Inference. SAT Inês Lynce, João Marques-Silva
2005	A	`conf`	A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. SAT Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva, Karem A. Sakallah
2005	A	`conf`	Effective Lower Bounding Techniques for Pseudo-Boolean Optimization. DATE Vasco M. Manquinho, João Marques-Silva
2005	J	`jnl`	Efficient data structures for backtrack search SAT solvers. Ann. Math. Artif. Intell. Inês Lynce, João Marques-Silva
2005	B	`conf`	Good Learning and Implicit Model Enumeration. ICTAI António Morgado, João Marques-Silva
2005	J	`jnl`	Heuristic-Based Backtracking Relaxation for Propositional Satisfiability. J. Autom. Reason. Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva
2005	—	`conf`	Improvements to the Implementation of Interpolant-Based Model Checking. CHARME João Marques-Silva
2005	A	`conf`	On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization. SAT Vasco Manquinho, João Marques-Silva
2005	B	`conf`	Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts. ICTAI Vasco M. Manquinho, João Marques-Silva
2004	B	`conf`	Hidden Structure in Unsatisfiable Random 3-SAT: An Empirical Study. ICTAI Inês Lynce, João Marques-Silva
2004	B	`conf`	Integration of Lower Bound Estimates in Pseudo-Boolean Optimization. ICTAI Vasco M. Manquinho, João Marques-Silva
2004	A	`conf`	On Computing Minimum Unsatisfiable Cores. SAT Inês Lynce, João Marques-Silva
2004	A	`conf`	Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization. SAT Vasco M. Manquinho, João Marques-Silva
2004	A	`conf`	Using Rewarding Mechanisms for Improving Branching Heuristics. SAT Elsa Carvalho, João Marques-Silva
2003	—	`conf`	Heuristic Backtracking Algorithms for SAT. MTV Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva
2003	Misc	`conf`	Heuristic-Based Backtracking for Propositional Satisfiability. EPIA Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva
2003	B	`conf`	Probing-Based Preprocessing Techniques for Propositional Satisfiability. ICTAI Inês Lynce, João Marques-Silva
2003	J	`jnl`	Solving Satisfiability in Combinational Circuits. IEEE Des. Test Comput. João Marques-Silva, Luís Guerra e Silva
2002	A	`conf`	Building State-of-the-Art SAT Solvers. ECAI Inês Lynce, João Marques-Silva
2002	J	`jnl`	Satisfiability models and algorithms for circuit delay computation. ACM Trans. Design Autom. Electr. Syst. Luís Guerra e Silva, João Marques-Silva, Luís Miguel Silveira, Karem A. Sakallah
2002	—	`conf`	The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms. International Workshop on Constraint Solving and Constraint Logic Programming Inês Lynce, João Marques-Silva
2002	A	`conf`	Tuning Randomization in Backtrack Search SAT Algorithms. CP Inês Lynce, João Marques-Silva
2001	A	`conf`	Improving SAT Algorithms by Using Search Pruning Techniques. CP Inês Lynce, João Marques-Silva
2001	J	`jnl`	Stochastic Systematic Search Algorithms for Satisfiability. Electron. Notes Discret. Math. Inês Lynce, Luís Baptista, João Marques-Silva
2001	Misc	`conf`	Towards Provably Complete Stochastic Search Algorithms for Satisfiability. EPIA Inês Lynce, Luís Baptista, João Marques-Silva
2000	A	`conf`	Algebraic Simplification Techniques for Propositional Satisfiability. CP João Marques-Silva
2000	A*	`conf`	Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. CAV João Marques-Silva, Karem A. Sakallah
2000	—	`conf`	On Solving Boolean Optimization with Satisfiability-Based Algorithms. AI&M Vasco M. Manquinho, João Marques-Silva
2000	A	`conf`	On Using Satisfiability-Based Pruning Techniques in Covering Algorithms. DATE Vasco M. Manquinho, João Marques-Silva
2000	A	`conf`	Search Pruning Conditions for Boolean Optimization. ECAI Vasco M. Manquinho, João Marques-Silva
2000	A	`conf`	Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability. CP Luís Baptista, João Marques-Silva
1999	A	`conf`	Algorithms for Solving Boolean Satisfiability in Combinational Circuits. DATE Luís Guerra e Silva, Luís Miguel Silveira, João Marques-Silva
1999	Misc	`conf`	Assignment and Reordering of Incompletely Specified Pattern Sequences Targetting Minimum Power Dissipation. VLSI Design Paulo F. Flores, José C. Costa, Horácio C. Neto, José Monteiro, João Marques-Silva
1999	A	`conf`	Combinational Equivalence Checking Using Satisfiability and Recursive Learning. DATE João Marques-Silva, Thomas Glass
1999	—	`conf`	Satisfiability-Based Functional Delay Fault Testing. VLSI Joonyoung Kim, João Marques-Silva, Karem A. Sakallah
1999	—	`conf`	Test pattern generation for width compression in BIST. ISCAS (1) Paulo F. Flores, Horácio C. Neto, Krishnendu Chakrabarty, João Marques-Silva
1999	Misc	`conf`	The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. EPIA João Marques-Silva