default search action
João Marques-Silva 0001
João P. Marques Silva – João Paulo Marques Silva
Person information
- affiliation: ICREA, University of Lleida, Catalunya, Spain
- affiliation (former): IRIT, CNRS, Toulouse, France
- affiliation (former): University of Toulouse, ANITI, Toulouse, France
- affiliation (former): University of Lisbon, Portugal
Other persons with the same name
- João Marques-Silva 0002 — Instituto Universitário de Lisboa, Lisbon, Portugal
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j62]Rosina O. Weber
, Adam J. Johs, Prateek Goel, João Marques-Silva:
XAI is in trouble. AI Mag. 45(3): 300-316 (2024) - [j61]João Marques-Silva
Explainability Is Not a Game. Commun. ACM 67(7): 66-75 (2024) - [j60]Xuanxiang Huang
On the failings of Shapley values for explainability. Int. J. Approx. Reason. 171: 109112 (2024) - [j59]Ismaïl Baaj
Synergies between machine learning and reasoning - An introduction by the Kay R. Amel group. Int. J. Approx. Reason. 171: 109206 (2024) - [j58]Gianpiero Cabodi
Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 43(10): 3083-3087 (2024) - [c214]Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, João Marques-Silva:
Delivering Inflated Explanations. AAAI 2024: 12744-12753 - [c213]Yacine Izza, Kuldeep S. Meel, João Marques-Silva:
Locally-Minimal Probabilistic Explanations. ECAI 2024: 1092-1099 - [c212]Xuanxiang Huang, João Marques-Silva:
Updates on the Complexity of SHAP Scores. IJCAI 2024: 403-412 - [c211]João Marques-Silva:
Logic-Based Explainability: Past, Present and Future. ISoLA (4) 2024: 181-204 - [c210]Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, João Marques-Silva:
Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. KR 2024 - [i67]Olivier Letoffe, Xuanxiang Huang, João Marques-Silva:
On Correcting SHAP Scores. CoRR abs/2405.00076 (2024) - [i66]Yacine Izza, Xuanxiang Huang, António Morgado, Jordi Planes, Alexey Ignatiev, João Marques-Silva:
Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation. CoRR abs/2405.08297 (2024) - [i65]Olivier Letoffe, Xuanxiang Huang, Nicholas Asher, João Marques-Silva:
From SHAP Scores to Feature Importance Scores. CoRR abs/2405.11766 (2024) - [i64]João Marques-Silva:
Logic-Based Explainability: Past, Present & Future. CoRR abs/2406.11873 (2024) - [i63]João Marques-Silva, Carlos Mencía, Raúl Mencía:
The Sets of Power. CoRR abs/2410.07867 (2024) - 2023
- [j57]Martin C. Cooper
Tractability of explaining classifier decisions. Artif. Intell. 316: 103841 (2023) - [j56]João Marques-Silva, Alexey Ignatiev
No silver bullet: interpretable ML models must be explained. Frontiers Artif. Intell. 6 (2023) - [j55]Yacine Izza
On computing probabilistic abductive explanations. Int. J. Approx. Reason. 159: 108939 (2023) - [c209]Xuanxiang Huang
Solving Explainability Queries with Quantification: The Case of Feature Relevancy. AAAI 2023: 3996-4006 - [c208]Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, Nina Narodytska, João Marques-Silva:
Eliminating the Impossible, Whatever Remains Must Be True: On Extracting and Applying Background Knowledge in the Context of Formal Explanations. AAAI 2023: 4123-4131 - [c207]Raúl Mencía, Carlos Mencía, João Marques-Silva:
Efficient Reasoning about Infeasible One Machine Sequencing. ICAPS 2023: 268-276 - [c206]Xuanxiang Huang
From Decision Trees to Explained Decision Sets. ECAI 2023: 1100-1108 - [c205]João Marques-Silva:
Disproving XAI Myths with Formal Methods - Initial Results. ICECCS 2023: 12-21 - [c204]Yacine Izza, Alexey Ignatiev, João Marques-Silva:
On Tackling Explanation Redundancy in Decision Trees (Extended Abstract). IJCAI 2023: 6900-6904 - [c203]Yacine Izza, João Marques-Silva:
On Computing Relevant Features for Explaining NBCs. ENIGMA@KR 2023: 75-86 - [c202]Clément Carbonnel, Martin C. Cooper, João Marques-Silva:
Tractable Explaining of Multivariate Decision Trees. KR 2023: 127-135 - [c201]Xuanxiang Huang
Feature Necessity & Relevancy in ML Classifier Explanations. TACAS (1) 2023: 167-186 - [c200]Aurélie Hurault
Certified Logic-Based Explainable AI - The Case of Monotonic Classifiers. TAP 2023: 51-67 - [i62]Xuanxiang Huang, João Marques-Silva:
The Inadequacy of Shapley Values for Explainability. CoRR abs/2302.08160 (2023) - [i61]João Marques-Silva:
Disproving XAI Myths with Formal Methods - Initial Results. CoRR abs/2306.01744 (2023) - [i60]Xuanxiang Huang, João Marques-Silva:
From Robustness to Explainability and Back Again. CoRR abs/2306.03048 (2023) - [i59]Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, João Marques-Silva:
Delivering Inflated Explanations. CoRR abs/2306.15272 (2023) - [i58]Ramón Béjar, António Morgado, Jordi Planes, João Marques-Silva:
On Logic-Based Explainability with Partially Specified Inputs. CoRR abs/2306.15803 (2023) - [i57]João Marques-Silva, Xuanxiang Huang:
Explainability is NOT a Game. CoRR abs/2307.07514 (2023) - [i56]Xuanxiang Huang, João Marques-Silva:
A Refutation of Shapley Values for Explainability. CoRR abs/2309.03041 (2023) - [i55]Xuanxiang Huang, João Marques-Silva:
Refutation of Shapley Values for XAI - Additional Evidence. CoRR abs/2310.00416 (2023) - [i54]Yacine Izza, João Marques-Silva:
The Pros and Cons of Adversarial Robustness. CoRR abs/2312.10911 (2023) - [i53]Yacine Izza, Kuldeep S. Meel, João Marques-Silva:
Locally-Minimal Probabilistic Explanations. CoRR abs/2312.11831 (2023) - 2022
- [j54]Yacine Izza, Alexey Ignatiev
On Tackling Explanation Redundancy in Decision Trees. J. Artif. Intell. Res. 75: 261-321 (2022) - [c199]Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, João Marques-Silva:
Using MaxSAT for Efficient Explanations of Tree Ensembles. AAAI 2022: 3776-3785 - [c198]Xuanxiang Huang
Tractable Explanations for d-DNNF Classifiers. AAAI 2022: 5719-5728 - [c197]Aditya A. Shrotri, Nina Narodytska, Alexey Ignatiev, Kuldeep S. Meel, João Marques-Silva, Moshe Y. Vardi:
Constraint-Driven Explanations for Black-Box ML Models. AAAI 2022: 8304-8314 - [c196]João Marques-Silva, Alexey Ignatiev:
Delivering Trustworthy AI through Formal XAI. AAAI 2022: 12342-12350 - [c195]João Marques-Silva:
Logic-Based Explainability in Machine Learning. RW 2022: 24-104 - [i52]Xuanxiang Huang, João Marques-Silva:
On Deciding Feature Membership in Explanations of SDD & Related Classifiers. CoRR abs/2202.07553 (2022) - [i51]Yacine Izza, Alexey Ignatiev
Provably Precise, Succinct and Efficient Explanations for Decision Trees. CoRR abs/2205.09569 (2022) - [i50]Yacine Izza, Alexey Ignatiev
On Tackling Explanation Redundancy in Decision Trees. CoRR abs/2205.09971 (2022) - [i49]Jinqiang Yu, Alexey Ignatiev
Eliminating The Impossible, Whatever Remains Must Be True. CoRR abs/2206.09551 (2022) - [i48]Yacine Izza, João Marques-Silva:
On Computing Relevant Features for Explaining NBCs. CoRR abs/2207.04748 (2022) - [i47]Xuanxiang Huang, Martin C. Cooper, António Morgado, Jordi Planes, João Marques-Silva:
Feature Necessity & Relevancy in ML Classifier Explanations. CoRR abs/2210.15675 (2022) - [i46]João Marques-Silva:
Logic-Based Explainability in Machine Learning. CoRR abs/2211.00541 (2022) - [i45]Yacine Izza, Xuanxiang Huang, Alexey Ignatiev
On Computing Probabilistic Abductive Explanations. CoRR abs/2212.05990 (2022) - 2021
- [j53]Maria Luisa Bonet, Sam Buss, Alexey Ignatiev
Propositional proof systems based on maximum satisfiability. Artif. Intell. 300: 103552 (2021) - [j52]Daniel Gibert
Auditing static machine learning anti-Malware tools against metamorphic attacks. Comput. Secur. 102: 102159 (2021) - [c194]Alexey Ignatiev, Edward Lam, Peter J. Stuckey, João Marques-Silva:
A Scalable Two Stage Approach to Computing Optimal Decision Sets. AAAI 2021: 3806-3814 - [c193]João Marques-Silva:
Automated Reasoning in Explainable AI. CCIA 2021: 4 - [c192]Martin C. Cooper
On the Tractability of Explaining Decisions of Classifiers. CP 2021: 21:1-21:18 - [c191]Gianpiero Cabodi, Paolo E. Camurati, Alexey Ignatiev
Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification. DATE 2021: 1122-1125 - [c190]João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska:
Explanations for Monotonic Classifiers. ICML 2021: 7469-7479 - [c189]Yacine Izza, João Marques-Silva:
On Explaining Random Forests with SAT. IJCAI 2021: 2584-2591 - [c188]Alexey Ignatiev, João Marques-Silva, Nina Narodytska, Peter J. Stuckey:
Reasoning-Based Learning of Interpretable ML Models. IJCAI 2021: 4458-4465 - [c187]Xuanxiang Huang
On Efficiently Explaining Graph-Based Classifiers. KR 2021: 356-367 - [c186]Alexey Ignatiev, João Marques-Silva:
SAT-Based Rigorous Explanations for Decision Lists. SAT 2021: 251-269 - [c185]Stepan Kochemazov
Assessing Progress in SAT Solvers Through the Lens of Incremental SAT. SAT 2021: 280-298 - [p6]João Marques-Silva, Inês Lynce, Sharad Malik
Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability 2021: 133-182 - [i44]Alexey Ignatiev, Edward Lam, Peter J. Stuckey, João Marques-Silva:
A Scalable Two Stage Approach to Computing Optimal Decision Sets. CoRR abs/2102.01904 (2021) - [i43]Takfarinas Saber, Anthony Ventresque, João Marques-Silva, James Thorburn, Liam Murphy:
MILP for the Multi-objective VM Reassignment Problem. CoRR abs/2103.10410 (2021) - [i42]Alexey Ignatiev, João Marques-Silva:
SAT-Based Rigorous Explanations for Decision Lists. CoRR abs/2105.06782 (2021) - [i41]Yacine Izza, João Marques-Silva:
On Explaining Random Forests with SAT. CoRR abs/2105.10278 (2021) - [i40]João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska:
Explanations for Monotonic Classifiers. CoRR abs/2106.00154 (2021) - [i39]Yacine Izza, Alexey Ignatiev, Nina Narodytska, Martin C. Cooper, João Marques-Silva:
Efficient Explanations With Relevant Sets. CoRR abs/2106.00546 (2021) - [i38]Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, João Marques-Silva:
On Efficiently Explaining Graph-Based Classifiers. CoRR abs/2106.01350 (2021) - [i37]Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, João Marques-Silva:
Efficient Explanations for Knowledge Compilation Languages. CoRR abs/2107.01654 (2021) - [i36]João Marques-Silva, Rafael Peñaloza, Uli Sattler:
Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361). Dagstuhl Reports 11(8): 1-10 (2021) - 2020
- [j51]Mario Alviano, Carmine Dodaro
Optimum stable model search: algorithms and implementation. J. Log. Comput. 30(4): 863-897 (2020) - [c184]Alexey Ignatiev
From Contrastive to Abductive Explanations and Back Again. AI*IA 2020: 335-355 - [c183]Alexey Ignatiev, Martin C. Cooper
Towards Formal Fairness in Machine Learning. CP 2020: 846-867 - [c182]Oleg Zaikin
Branch Location Problems with Maximum Satisfiability. ECAI 2020: 379-386 - [c181]João Marques-Silva, Carlos Mencía
Reasoning About Inconsistent Formulas. IJCAI 2020: 4899-4906 - [c180]João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, Nina Narodytska:
Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay. NeurIPS 2020 - [c179]Carlos Mencía, João Marques-Silva:
Reasoning About Strong Inconsistency in ASP. SAT 2020: 332-342 - [i35]João Marques-Silva, Thomas Gerspacher, Martin C. Cooper
Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay. CoRR abs/2008.05803 (2020) - [i34]Yacine Izza, Alexey Ignatiev, João Marques-Silva:
On Explaining Decision Trees. CoRR abs/2010.11034 (2020) - [i33]Alexey Ignatiev, Nina Narodytska, Nicholas Asher, João Marques-Silva:
On Relating 'Why?' and 'Why Not?' Explanations. CoRR abs/2012.11067 (2020)
2010 – 2019
- 2019
- [j50]Luís Cruz-Filipe
Formally Verifying the Solution to the Boolean Pythagorean Triples Problem. J. Autom. Reason. 63(3): 695-722 (2019) - [j49]Alexey Ignatiev, António Morgado, João Marques-Silva:
RC2: an Efficient MaxSAT Solver. J. Satisf. Boolean Model. Comput. 11(1): 53-64 (2019) - [c178]Alexey Ignatiev
Abduction-Based Explanations for Machine Learning Models. AAAI 2019: 1511-1519 - [c177]Carlos Mencía, João Marques-Silva:
Computing Shortest Resolution Proofs. EPIA (2) 2019: 539-551 - [c176]Alexey Ignatiev
Model-Based Diagnosis with Multiple Observations. IJCAI 2019: 1108-1115 - [c175]Ilya Zakirzyanov, António Morgado
Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference. LATA 2019: 159-173 - [c174]Alexey Ignatiev, Nina Narodytska, João Marques-Silva:
On Relating Explanations and Adversarial Examples. NeurIPS 2019: 15857-15867 - [c173]Carlos Mencía
On Computing the Union of MUSes. SAT 2019: 211-221 - [c172]António Morgado
DRMaxSAT with MaxHS: First Contact. SAT 2019: 239-249 - [c171]Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev
Assessing Heuristic Machine Learning Explanations with Model Counting. SAT 2019: 267-278 - [i32]Alexey Ignatiev, Nina Narodytska, João Marques-Silva:
On Validating, Repairing and Refining Heuristic ML Explanations. CoRR abs/1907.02509 (2019) - [i31]Zied Bouraoui, Antoine Cornuéjols, Thierry Denoeux, Sébastien Destercke, Didier Dubois, Romain Guillaume
From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group). CoRR abs/1912.06612 (2019) - 2018
- [c170]Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, João Marques-Silva, António Morgado:
MaxSAT Resolution With the Dual Rail Encoding. AAAI 2018: 6565-6572 - [c169]Alessandro Previti, Carlos Mencía, Matti Järvisalo, João Marques-Silva:
Premise Set Caching for Enumerating Minimal Correction Subsets. AAAI 2018: 6633-6640 - [c168]Alexey Ignatiev
A SAT-Based Approach to Learn Explainable Decision Sets. IJCAR 2018: 627-645 - [c167]João Marques-Silva:
Computing with SAT Oracles: Past, Present and Future. CiE 2018: 264-276 - [c166]Nina Narodytska, Alexey Ignatiev, Filipe Pereira, João Marques-Silva:
Learning Optimal Decision Trees with SAT. IJCAI 2018: 1362-1368 - [c165]Alexey Ignatiev
PySAT: A Python Toolkit for Prototyping with SAT Oracles. SAT 2018: 428-437 - [p5]João Marques-Silva, Sharad Malik:
Propositional SAT Solving. Handbook of Model Checking 2018: 247-275 - [i30]Alexey Ignatiev, Nina Narodytska, João Marques-Silva:
Abduction-Based Explanations for Machine Learning Models. CoRR abs/1811.10656 (2018) - 2017
- [j48]João Marques-Silva
Minimal sets on propositional formulae. Problems and reductions. Artif. Intell. 252: 22-50 (2017) - [j47]Takfarinas Saber
Exact and Hybrid Solutions for the Multi-Objective VM Reassignment Problem. Int. J. Artif. Intell. Tools 26(1): 1760004:1-1760004:36 (2017) - [c164]Mikolás Janota, João Marques-Silva:
On Minimal Corrections in ASP. RCRA@AI*IA 2017: 45-54 - [c163]Alexey Ignatiev, João Marques-Silva, Carlos Mencía, Rafael Peñaloza:
Debugging EL+ Ontologies through Horn MUS Enumeration. Description Logics 2017 - [c162]Mikolás Janota
An Achilles' Heel of Term-Resolution. EPIA 2017: 670-680 - [c161]João Marques-Silva, Alexey Ignatiev
Horn Maximum Satisfiability: Reductions, Algorithms and Applications. EPIA 2017: 681-694 - [c160]Rafael Peñaloza, Carlos Mencía
Lean Kernels in Description Logics. ESWC (1) 2017: 518-533 - [c159]Alessandro Previti, Alexey Ignatiev
On Computing Generalized Backbones. ICTAI 2017: 1050-1056 - [c158]Alexey Ignatiev, António Morgado, João Marques-Silva:
Cardinality Encodings for Graph Optimization Problems. IJCAI 2017: 652-658 - [c157]Alexey Ignatiev
On Tackling the Limits of Resolution in SAT Solving. SAT 2017: 164-183 - [c156]Alessandro Previti, Carlos Mencía
Improving MCS Enumeration via Caching. SAT 2017: 184-194 - [c155]Luís Cruz-Filipe
Efficient Certified Resolution Proof Checking. TACAS (1) 2017: 118-135 - [i29]Alexey Ignatiev, António Morgado, João Marques-Silva:
On Tackling the Limits of Resolution in SAT Solving. CoRR abs/1705.01477 (2017) - [i28]João Marques-Silva, Alexey Ignatiev, António Morgado:
Horn Maximum Satisfiability: Reductions, Algorithms & Applications. CoRR abs/1705.05335 (2017) - [i27]Alexey Ignatiev, António Morgado, João Marques-Silva:
Model Based Diagnosis of Multiple Observations with Implicit Hitting Sets. CoRR abs/1707.01972 (2017) - 2016
- [j46]Mikolás Janota
On the query complexity of selecting minimal sets for monotone predicates. Artif. Intell. 233: 73-83 (2016) - [j45]Mikolás Janota
Solving QBF with counterexample guided refinement. Artif. Intell. 234: 1-25 (2016) - [j44]Alexey Ignatiev
Maximal falsifiability. AI Commun. 29(2): 351-370 (2016) - [j43]Stefano V. Albrecht, Bruno Bouchard, John S. Brownstein, David L. Buckeridge, Cornelia Caragea
Reports of the 2016 AAAI Workshop Program. AI Mag. 37(3): 99-108 (2016) - [j42]Mark H. Liffiton, Alessandro Previti, Ammar Malik, João Marques-Silva:
Fast, flexible MUS enumeration. Constraints An Int. J. 21(2): 223-250 (2016) - [j41]Alexey Ignatiev
Quantified maximum satisfiability. Constraints An Int. J. 21(2): 277-302 (2016) - [c154]Adnan Darwiche, João Marques-Silva, Pierre Marquis:
Preface: The Beyond NP Workshop. AAAI Workshop: Beyond NP 2016 - [c153]Alexey Ignatiev
On Finding Minimum Satisfying Assignments. CP 2016: 287-297 - [c152]Alexey Ignatiev
Propositional Abduction with Implicit Hitting Sets. ECAI 2016: 1327-1335 - [c151]João Marques-Silva, Alexey Ignatiev
Efficient Reasoning for Inconsistent Horn Formulae. JELIA 2016: 336-352 - [c150]Carlos Mencía
MCS Extraction with Sublinear Oracle Queries. SAT 2016: 342-360 - [c149]M. Fareed Arif, Carlos Mencía
BEACON: An Efficient SAT-Based Tool for Debugging EL^+ Ontologies. SAT 2016: 521-530 - [i26]Alexey Ignatiev, António Morgado, João Marques-Silva:
Propositional Abduction with Implicit Hitting Sets. CoRR abs/1604.08229 (2016) - [i25]Luís Cruz-Filipe, João Marques-Silva, Peter Schneider-Kamp:
Efficient Certified Resolution Proof Checking. CoRR abs/1610.06984 (2016) - 2015
- [j40]Mikolás Janota
Algorithms for computing backbones of propositional formulae. AI Commun. 28(2): 161-177 (2015) - [j39]Federico Heras, António Morgado
MaxSAT-based encodings for Group MaxSAT. AI Commun. 28(2): 195-214 (2015) - [j38]Mikolás Janota
Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577: 25-42 (2015) - [c148]Alexey Ignatiev
Smallest MUS Extraction with Minimal Hitting Set Dualization. CP 2015: 173-182 - [c147]Takfarinas Saber
MILP for the Multi-objective VM Reassignment Problem. ICTAI 2015: 41-48 - [c146]Mikolás Janota, João Marques-Silva:
Solving QBF by Clause Selection. IJCAI 2015: 325-331 - [c145]João Marques-Silva, Mikolás Janota, Alexey Ignatiev, António Morgado:
Efficient Model Based Diagnosis with Maximum Satisfiability. IJCAI 2015: 1966-1972 - [c144]Carlos Mencía, Alessandro Previti, João Marques-Silva:
Literal-Based MCS Extraction. IJCAI 2015: 1973-1979 - [c143]Alessandro Previti, Alexey Ignatiev, António Morgado, João Marques-Silva:
Prime Compilation of Non-Clausal Formulae. IJCAI 2015: 1980-1988 - [c142]M. Fareed Arif, Carlos Mencía
Efficient Axiom Pinpointing with EL2MCS. KI 2015: 225-233 - [c141]Oliver Kullmann, João Marques-Silva:
Computing Maximal Autarkies with Few and Simple Oracle Queries. SAT 2015: 138-155 - [c140]Alexey Ignatiev
SAT-Based Formula Simplification. SAT 2015: 287-298 - [c139]M. Fareed Arif, Carlos Mencía
Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing. SAT 2015: 324-342 - [c138]Carlos Mencía
SAT-Based Horn Least Upper Bounds. SAT 2015: 423-433 - [i24]M. Fareed Arif, João Marques-Silva:
Towards Efficient Axiom Pinpointing of EL+ Ontologies. CoRR abs/1503.08454 (2015) - [i23]Oliver Kullmann, João Marques-Silva:
Computing maximal autarkies with few and simple oracle queries. CoRR abs/1505.02371 (2015) - [i22]M. Fareed Arif, Carlos Mencía, João Marques-Silva:
Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing. CoRR abs/1505.04365 (2015) - 2014
- [j37]Anton Belov, Mikolás Janota
Algorithms for computing minimal equivalent subformulas. Artif. Intell. 216: 309-326 (2014) - [j36]António Morgado, Alexey Ignatiev, João Marques-Silva:
MSCG: Robust Core-Guided MaxSAT Solving. J. Satisf. Boolean Model. Comput. 9(1): 129-134 (2014) - [c137]António Morgado
Core-Guided MaxSAT with Soft Cardinality Constraints. CP 2014: 564-573 - [c136]Yuri Malitsky, Barry O'Sullivan
A Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. CPAIOR 2014: 368-376 - [c135]Alexey Ignatiev
Progression in Maximum Satisfiability. ECAI 2014: 453-458 - [c134]João Marques-Silva, Alexey Ignatiev
Efficient Autarkies. ECAI 2014: 603-608 - [c133]Yuri Malitsky, Barry O'Sullivan
Timeout-Sensitive Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems. ECAI 2014: 1065-1066 - [c132]Alexey Ignatiev
Towards efficient optimization in package management systems. ICSE 2014: 745-755 - [c131]Carlos Mencía
Efficient Relaxations of Over-constrained CSPs. ICTAI 2014: 725-732 - [c130]Saïd Jabbour, João Marques-Silva, Lakhdar Sais, Yakoub Salhi
Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form. JELIA 2014: 152-165 - [c129]Anton Belov, Marijn Heule
MUS Extraction Using Clausal Proofs. SAT 2014: 48-57 - [c128]João Marques-Silva, Alessandro Previti:
On Computing Preferred MUSes and MCSes. SAT 2014: 58-74 - [c127]Alexey Ignatiev
On Reducing Maximum Independent Set to Minimum Satisfiability. SAT 2014: 103-120 - [c126]Arie Gurfinkel
Synthesizing Safe Bit-Precise Invariants. TACAS 2014: 93-108 - [c125]Mikolás Janota
On lazy and eager interactive reconfiguration. VaMoS 2014: 8:1-8:8 - [p4]João Marques-Silva, Inês Lynce
SAT Solvers. Tractability 2014: 331-349 - [i21]João Marques-Silva, Mikolás Janota:
Computing Minimal Sets on Propositional Formulae I: Problems & Reductions. CoRR abs/1402.3011 (2014) - [i20]Mikolás Janota, João Marques-Silva:
On Minimal Corrections in ASP. CoRR abs/1406.7838 (2014) - [i19]João Marques-Silva, Mikolás Janota:
On the Query Complexity of Selecting Few Minimal Sets. Electron. Colloquium Comput. Complex. TR14 (2014) - 2013
- [j35]António Morgado
Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints An Int. J. 18(4): 478-534 (2013) - [j34]Huan Chen, João Marques-Silva:
A Two-Variable Model for SAT-Based ATPG. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(12): 1943-1956 (2013) - [c124]Alessandro Previti, João Marques-Silva:
Partial MUS Enumeration. AAAI 2013: 818-825 - [c123]João Marques-Silva
Minimal Sets over Monotone Predicates in Boolean Formulae. CAV 2013: 592-607 - [c122]William Klieber, Mikolás Janota
Solving QBF with Free Variables. CP 2013: 415-431 - [c121]Anton Belov, Huan Chen, Alan Mishchenko, João Marques-Silva:
Core minimization in SAT-based abstraction. DATE 2013: 1411-1416 - [c120]António Morgado
Model-Guided Approaches for MaxSAT Solving. ICTAI 2013: 931-938 - [c119]João Marques-Silva, Federico Heras, Mikolás Janota, Alessandro Previti, Anton Belov:
On Computing Minimal Correction Subsets. IJCAI 2013: 615-622 - [c118]Anton Belov, António Morgado
SAT-Based Preprocessing for MaxSAT. LPAR 2013: 96-111 - [c117]Alexey Ignatiev
Maximal Falsifiability - Definitions, Algorithms, and Applications. LPAR 2013: 439-456 - [c116]Mikolás Janota
On QBF Proofs and Preprocessing. LPAR 2013: 473-489 - [c115]Mikolás Janota
On Propositional QBF Expansions and Q-Resolution. SAT 2013: 67-82 - [c114]Anton Belov, Norbert Manthey, João Marques-Silva
Parallel MUS Extraction. SAT 2013: 133-149 - [c113]Alexey Ignatiev
Quantified Maximum Satisfiability: - A Core-Guided Approach. SAT 2013: 250-266 - [c112]Anton Belov, Matti Järvisalo
Formula Preprocessing in MUS Extraction. TACAS 2013: 108-123 - [i18]Anton Belov, António Morgado, João Marques-Silva:
SAT-based Preprocessing for MaxSAT (extended version). CoRR abs/1310.2298 (2013) - [i17]Mikolás Janota, Radu Grigore, João Marques-Silva:
On QBF Proofs and Preprocessing. CoRR abs/1310.2491 (2013) - [i16]Mikolás Janota, João Marques-Silva:
On Propositional QBF Expansions and Q-Resolution. Electron. Colloquium Comput. Complex. TR13 (2013) - 2012
- [j33]Anton Belov, Inês Lynce
Towards efficient MUS extraction. AI Commun. 25(2): 97-116 (2012) - [j32]Florian Letombe, João Marques-Silva
Hybrid Incremental Algorithms for Boolean Satisfiability. Int. J. Artif. Intell. Tools 21(6) (2012) - [j31]Huan Chen, João Marques-Silva:
TG-Pro: A SAT-based ATPG System. J. Satisf. Boolean Model. Comput. 8(1/2): 83-88 (2012) - [j30]Mikolás Janota, Inês Lynce, Vasco Manquinho, João Marques-Silva:
PackUp: Tools for Package Upgradability Solving. J. Satisf. Boolean Model. Comput. 8(1/2): 89-94 (2012) - [j29]Anton Belov, João Marques-Silva:
MUSer2: An Efficient MUS Extractor. J. Satisf. Boolean Model. Comput. 8(3/4): 123-128 (2012) - [j28]João Marques-Silva:
Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions. J. Multiple Valued Log. Soft Comput. 19(1-3): 163-183 (2012) - [j27]Lucas C. Cordeiro
SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Trans. Software Eng. 38(4): 957-974 (2012) - [c111]Federico Heras, António Morgado
An Empirical Study of Encodings for Group MaxSAT. Canadian AI 2012: 85-96 - [c110]Anton Belov, Mikolás Janota
On Computing Minimal Equivalent Subformulas. CP 2012: 158-174 - [c109]Huan Chen, Mikolás Janota
QBf-based boolean function bi-decomposition. DATE 2012: 816-819 - [c108]Huan Chen, João Marques-Silva
New & improved models for SAT-based bi-decomposition. ACM Great Lakes Symposium on VLSI 2012: 141-146 - [c107]António Morgado, Mark H. Liffiton, João Marques-Silva:
MaxSAT-Based MCS Enumeration. Haifa Verification Conference 2012: 86-101 - [c106]Federico Heras, António Morgado
Iterative SAT Solving for Minimum Satisfiability. ICTAI 2012: 922-927 - [c105]Lucas Bordeaux, Mikolás Janota, João Marques-Silva, Pierre Marquis:
On Unit-Refutation Complete Formulae with Existentially Quantified Variables. KR 2012 - [c104]Federico Heras, António Morgado
Lower Bounds and Upper Bounds for MaxSAT. LION 2012: 402-407 - [c103]Mikolás Janota
Solving QBF with Counterexample Guided Refinement. SAT 2012: 114-128 - [c102]António Morgado
Improvements to Core-Guided Binary Search for MaxSAT. SAT 2012: 284-297 - [c101]Anton Belov, Alexander Ivrii, Arie Matsliah, João Marques-Silva
On Efficient Computation of Variable MUSes. SAT 2012: 298-311 - [c100]Lucas Bordeaux, João Marques-Silva
Knowledge Compilation with Empowerment. SOFSEM 2012: 612-624 - [i15]Anton Belov, João Marques-Silva:
Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality. CoRR abs/1207.1257 (2012) - 2011
- [j26]João Marques-Silva
Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3-4): 317-343 (2011) - [j25]Ana Graça, João Marques-Silva
Haplotype inference with pseudo-Boolean optimization. Ann. Oper. Res. 184(1): 137-162 (2011) - [j24]Karem A. Sakallah, João Marques-Silva:
Anatomy and Empirical Evaluation of Modern SAT Solvers. Bull. EATCS 103: 96-121 (2011) - [j23]Inês Lynce
Restoring CSP Satisfiability with MaxSAT. Fundam. Informaticae 107(2-3): 249-266 (2011) - [c99]Federico Heras, António Morgado, João Marques-Silva:
Core-Guided Binary Search Algorithms for Maximum Satisfiability. AAAI 2011: 36-41 - [c98]Mikolás Janota
On Deciding MUS Membership with QBF. CP 2011: 414-428 - [c97]Anton Belov, João Marques-Silva:
Accelerating MUS extraction with recursive model rotation. FMCAD 2011: 37-40 - [c96]António Morgado
On Validating Boolean Optimizers. ICTAI 2011: 924-926 - [c95]Federico Heras, João Marques-Silva
Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms. IJCAI 2011: 572-577 - [c94]Mikolás Janota
cmMUS: A Tool for Circumscription-Based MUS Membership Testing. LPNMR 2011: 266-271 - [c93]Anton Belov, João Marques-Silva
Minimally Unsatisfiable Boolean Circuits. SAT 2011: 145-158 - [c92]João Marques-Silva
On Improving MUS Extraction Algorithms. SAT 2011: 159-173 - [c91]Mikolás Janota
Abstraction-Based Algorithm for 2QBF. SAT 2011: 230-244 - [c90]Hadi Katebi, Karem A. Sakallah, João P. Marques Silva
Empirical Study of the Anatomy of Modern Sat Solvers. SAT 2011: 343-356 - [c89]Huan Chen, João Marques-Silva
Improvements to Satisfiability-Based Boolean Function Bi-Decomposition. VLSI-SoC (Selected Papers) 2011: 52-72 - [c88]Huan Chen, João Marques-Silva
Improvements to satisfiability-based boolean function bi-decomposition. VLSI-SoC 2011: 142-147 - [c87]Youssef Hamadi, João Marques-Silva, Christoph M. Wintersteiger
Lazy Decomposition for Distributed Decision Procedures. PDMC 2011: 43-54 - [p3]Ana Graça, João Marques-Silva, Inês Lynce
Haplotype Inference Using Propositional Satisfiability. Mathematical Approaches to Polymer Sequence Analysis and Related Problems 2011: 127-147 - [i14]António Morgado, João Marques-Silva:
On Validating Boolean Optimizers. CoRR abs/1109.2752 (2011) - [i13]Huan Chen, Mikolás Janota, João Marques-Silva:
QBF-Based Boolean Function Bi-Decomposition. CoRR abs/1112.2313 (2011) - 2010
- [j22]António Morgado
Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem. Fundam. Informaticae 102(3-4): 363-389 (2010) - [j21]Ana Graça, Inês Lynce
Haplotype Inference by Pure Parsimony: A Survey. J. Comput. Biol. 17(8): 969-992 (2010) - [j20]Yibin Chen, Sean Safarpour, João Marques-Silva
Automated Design Debugging With Maximum Satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(11): 1804-1817 (2010) - [c86]Ana Graça, Inês Lynce
Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information. ANB 2010: 38-56 - [c85]João Marques-Silva, Josep Argelich, Ana Graça, Inês Lynce:
Boolean Lexicographic Optimization. RCRA@CPAIOR 2010 - [c84]João Marques-Silva, Mikolás Janota, Inês Lynce:
On Computing Backbones of Propositional Theories. ECAI 2010: 15-20 - [c83]Lucas C. Cordeiro
Continuous Verification of Large Embedded Software Using SMT-Based Bounded Model Checking. ECBS 2010: 160-169 - [c82]Ashish Darbari, Bernd Fischer
Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking. ICTAC 2010: 260-274 - [c81]João Marques-Silva
Minimal Unsatisfiability: Models, Algorithms and Applications (Invited Paper). ISMVL 2010: 9-14 - [c80]Mikolás Janota
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. JELIA 2010: 195-207 - [c79]Mikolás Janota
How to Complete an Interactive Configuration Process? SOFSEM 2010: 528-539 - [c78]Josep Argelich
Solving Linux Upgradeability Problems Using Boolean Optimization. LoCoCo 2010: 11-22 - [i12]Mikolás Janota, João Marques-Silva, Radu Grigore:
Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription. CoRR abs/1006.5896 (2010)
2000 – 2009
- 2009
- [j19]Mark H. Liffiton, Maher N. Mneimneh, Inês Lynce
A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints An Int. J. 14(4): 415-442 (2009) - [c77]Inês Lynce, João Marques-Silva:
Restoring CSP Satisfiability with MaxSAT. RCRA@AI*IA 2009 - [c76]Yibin Chen, Sean Safarpour, Andreas G. Veneris, João Marques-Silva
Spatial and temporal design debug using partial MaxSAT. ACM Great Lakes Symposium on VLSI 2009: 345-350 - [c75]Huan Chen, João Marques-Silva
TG-PRO: A new model for SAT-based ATPG. HLDVT 2009: 76-81 - [c74]Lucas C. Cordeiro
Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. ICESS 2009: 396-403 - [c73]Paulo J. Matos, Bernd Fischer
A Lazy Unbounded Model Checker for Event-B. ICFEM 2009: 485-503 - [c72]Josep Argelich, Inês Lynce, João Marques-Silva:
On Solving Boolean Multilevel Optimization Problemse. IJCAI 2009: 393-398 - [c71]Lucas C. Cordeiro
SMT-Based Bounded Model Checking for Embedded ANSI-C Software. ASE 2009: 137-148 - [c70]Vasco Manquinho
Algorithms for Weighted Boolean Optimization. SAT 2009: 495-508 - [p2]João Marques-Silva
Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability 2009: 131-153 - [i11]Vasco Manquinho, João Marques-Silva, Jordi Planes:
Algorithms for Weighted Boolean Optimization. CoRR abs/0903.0843 (2009) - [i10]Josep Argelich, Inês Lynce, João Marques-Silva:
On Solving Boolean Multilevel Optimization Problems. CoRR abs/0904.0019 (2009) - [i9]Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva:
SMT-Based Bounded Model Checking for Embedded ANSI-C Software. CoRR abs/0907.2072 (2009) - [i8]Mikolás Janota, João Marques-Silva, Radu Grigore:
Algorithms for finding dispensable variables. CoRR abs/0910.0013 (2009) - [i7]Mikolás Janota, Goetz Botterweck, Radu Grigore, João Marques-Silva:
How to Complete an Interactive Configuration Process? CoRR abs/0910.3913 (2009) - [i6]Ashish Darbari, Bernd Fischer, João Marques-Silva:
Industrial-Strength Formally Certified SAT Solving. CoRR abs/0911.1678 (2009) - [i5]Lucas C. Cordeiro, Bernd Fischer, João Marques-Silva:
Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. CoRR abs/0911.3784 (2009) - 2008
- [j18]Inês Lynce
Boosting Haplotype Inference with Local Search. Constraints An Int. J. 13(1-2): 155-179 (2008) - [j17]Inês Lynce
Haplotype Inference with Boolean Satisfiability. Int. J. Artif. Intell. Tools 17(2): 355-387 (2008) - [j16]João Marques-Silva
Model checking with Boolean Satisfiability. J. Algorithms 63(1-3): 3-16 (2008) - [c69]Paulo J. Matos, João Marques-Silva:
Model Checking Event-B by Encoding into Alloy. ABZ 2008: 346 - [c68]Ana Graça, João Marques-Silva
Efficient Haplotype Inference with Combined CP and OR Techniques. CPAIOR 2008: 308-312 - [c67]João Marques-Silva
Algorithms for Maximum Satisfiability using Unsatisfiable Cores. DATE 2008: 408-413 - [c66]Paulo J. Matos, Jordi Planes
A MAX-SAT Algorithm Portfolio. ECAI 2008: 911-912 - [c65]Federico Heras, Vasco Manquinho, João Marques-Silva:
On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization. FLAIRS 2008: 71-76 - [c64]Inês Lynce
Haplotype Inference with Boolean Constraint Solving: An Overview. ICTAI (1) 2008: 92-100 - [c63]João Marques-Silva
Symmetry Breaking for Maximum Satisfiability. LPAR 2008: 1-15 - [c62]António Morgado, João Marques-Silva:
Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem. RCRA 2008 - [c61]Florian Letombe, João Marques-Silva
Improvements to Hybrid Incremental SAT Algorithms. SAT 2008: 168-181 - [c60]João Marques-Silva
Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms. SAT 2008: 225-230 - [p1]Inês Lynce, Vasco Manquinho
Backtracking. Wiley Encyclopedia of Computer Science and Engineering 2008 - [i4]João Marques-Silva, Inês Lynce, Vasco Manquinho:
Symmetry Breaking for Maximum Satisfiability. CoRR abs/0804.0599 (2008) - [i3]António Morgado, João Marques-Silva:
A Pseudo-Boolean Solution to the Maximum Quartet Consistency Problem. CoRR abs/0805.0202 (2008) - [i2]Paulo J. Matos, João Marques-Silva:
Model Checking Event-B by Encoding into Alloy. CoRR abs/0805.3256 (2008) - 2007
- [j15]João Marques-Silva, Karem A. Sakallah, Inês Lynce:
Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing. AI Mag. 28(4): 135-136 (2007) - [j14]Inês Lynce
Random backtracking in backtrack search algorithms for satisfiability. Discret. Appl. Math. 155(12): 1604-1612 (2007) - [c59]Ana Graça, João Marques-Silva, Inês Lynce, Arlindo L. Oliveira
Efficient Haplotype Inference with Pseudo-boolean Optimization. AB 2007: 125-139 - [c58]João Marques-Silva, Inês Lynce:
Towards Robust CNF Encodings of Cardinality Constraints. CP 2007: 483-497 - [c57]João Marques-Silva, Inês Lynce, Ana Graça, Arlindo L. Oliveira
Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony Using Delayed Haplotype Selection. EPIA Workshops 2007: 621-632 - [c56]Nicola Bombieri
Towards Equivalence Checking Between TLM and RTL Models. MEMOCODE 2007: 113-122 - [c55]Inês Lynce, João Marques-Silva:
Breaking Symmetries in SAT Matrix Models. SAT 2007: 22-27 - [e1]João Marques-Silva, Karem A. Sakallah:
Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings. Lecture Notes in Computer Science 4501, Springer 2007, ISBN 978-3-540-72787-3 [contents] - [i1]João Marques-Silva, Jordi Planes:
On Using Unsatisfiability for Solving Maximum Satisfiability. CoRR abs/0712.1097 (2007) - 2006
- [j13]Vasco M. Manquinho, João Marques-Silva:
On Using Cutting Planes in Pseudo-Boolean Optimization. J. Satisf. Boolean Model. Comput. 2(1-4): 209-219 (2006) - [c54]Inês Lynce, João Marques-Silva:
Efficient Haplotype Inference with Boolean Satisfiability. AAAI 2006: 104-109 - [c53]Oliver Kullmann, Inês Lynce, João Marques-Silva:
Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel. SAT 2006: 22-35 - [c52]Inês Lynce, João Marques-Silva:
SAT in Bioinformatics: Making the Case with Haplotype Inference. SAT 2006: 136-141 - [c51]António Morgado, Paulo J. Matos, Vasco Manquinho, João Marques-Silva:
Counting Models in Integer Domains. SAT 2006: 410-423 - [c50]João Marques-Silva
Interpolant Learning and Reuse in SAT-Based Model Checking. BMC@FLoC 2006: 31-43 - 2005
- [j12]Inês Lynce
Efficient data structures for backtrack search SAT solvers. Ann. Math. Artif. Intell. 43(1): 137-152 (2005) - [j11]Ateet Bhalla, Inês Lynce
Heuristic-Based Backtracking Relaxation for Propositional Satisfiability. J. Autom. Reason. 35(1-3): 3-24 (2005) - [c49]João Marques-Silva
Improvements to the Implementation of Interpolant-Based Model Checking. CHARME 2005: 367-370 - [c48]Vasco M. Manquinho
Effective Lower Bounding Techniques for Pseudo-Boolean Optimization. DATE 2005: 660-665 - [c47]António Morgado
Good Learning and Implicit Model Enumeration. ICTAI 2005: 131-136 - [c46]Vasco M. Manquinho
Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts. ICTAI 2005: 150-155 - [c45]Vasco Manquinho, João Marques-Silva:
On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization. SAT 2005: 451-458 - [c44]Maher N. Mneimneh, Inês Lynce, Zaher S. Andraus, João Marques-Silva, Karem A. Sakallah:
A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas. SAT 2005: 467-474 - 2004
- [j10]Vasco M. Manquinho, João P. Marques Silva:
Satisfiability-Based Algorithms for Boolean Optimization. Ann. Math. Artif. Intell. 40(3-4): 353-372 (2004) - [c43]Inês Lynce, João Marques-Silva:
Hidden Structure in Unsatisfiable Random 3-SAT: An Empirical Study. ICTAI 2004: 246-251 - [c42]Vasco M. Manquinho
Integration of Lower Bound Estimates in Pseudo-Boolean Optimization. ICTAI 2004: 742-748 - [c41]Elsa Carvalho, João Marques-Silva:
Using Rewarding Mechanisms for Improving Branching Heuristics. SAT 2004 - [c40]Inês Lynce, João Marques-Silva:
On Computing Minimum Unsatisfiable Cores. SAT 2004 - [c39]Vasco M. Manquinho
Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization. SAT 2004 - 2003
- [j9]Inês Lynce
An Overview of Backtrack Search Satisfiability Algorithms. Ann. Math. Artif. Intell. 37(3): 307-326 (2003) - [j8]João Marques-Silva
Solving Satisfiability in Combinational Circuits. IEEE Des. Test Comput. 20(4): 16-21 (2003) - [c38]Ateet Bhalla, Inês Lynce, José T. de Sousa
Heuristic-Based Backtracking for Propositional Satisfiability. EPIA 2003: 116-130 - [c37]Inês Lynce
Probing-Based Preprocessing Techniques for Propositional Satisfiability. ICTAI 2003: 105- - [c36]Ateet Bhalla, Inês Lynce
Heuristic Backtracking Algorithms for SAT. MTV 2003: 69-74 - 2002
- [j7]Vasco M. Manquinho
Search pruning techniques in SAT-based branch-and-bound algorithmsfor the binate covering problem. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 21(5): 505-516 (2002) - [j6]Luís Guerra e Silva
Satisfiability models and algorithms for circuit delay computation. ACM Trans. Design Autom. Electr. Syst. 7(1): 137-158 (2002) - [c35]Inês Lynce, João Marques-Silva:
The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms. International Workshop on Constraint Solving and Constraint Logic Programming 2002: 144-158 - [c34]Inês Lynce, João Marques-Silva:
Tuning Randomization in Backtrack Search SAT Algorithms. CP 2002: 769 - [c33]Inês Lynce, João Marques-Silva:
Building State-of-the-Art SAT Solvers. ECAI 2002: 166-170 - 2001
- [j5]Inês Lynce, Luís Baptista, João Marques-Silva:
Stochastic Systematic Search Algorithms for Satisfiability. Electron. Notes Discret. Math. 9: 190-204 (2001) - [j4]Arlindo L. Oliveira
Efficient Algorithms for the Inference of Minimum Size DFAs. Mach. Learn. 44(1/2): 93-119 (2001) - [j3]Paulo F. Flores
An exact solution to the minimum size test pattern problem. ACM Trans. Design Autom. Electr. Syst. 6(4): 629-644 (2001) - [c32]Inês Lynce, João Marques-Silva:
Improving SAT Algorithms by Using Search Pruning Techniques. CP 2001: 770 - [c31]Inês Lynce, Luís Baptista, João Marques-Silva:
Towards Provably Complete Stochastic Search Algorithms for Satisfiability. EPIA 2001: 363-370 - 2000
- [c30]Vasco M. Manquinho, João Marques-Silva:
On Solving Boolean Optimization with Satisfiability-Based Algorithms. AI&M 2000 - [c29]João Marques-Silva, Karem A. Sakallah:
Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation. CAV 2000: 3 - [c28]Luís Baptista, João Marques-Silva:
Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability. CP 2000: 489-494 - [c27]João Marques-Silva:
Algebraic Simplification Techniques for Propositional Satisfiability. CP 2000: 537-542 - [c26]João P. Marques Silva, Karem A. Sakallah:
Boolean satisfiability in electronic design automation. DAC 2000: 675-680 - [c25]Vasco M. Manquinho
On Using Satisfiability-Based Pruning Techniques in Covering Algorithms. DATE 2000: 356-363 - [c24]Joonyoung Kim, Jesse Whittemore, Karem A. Sakallah, João P. Marques Silva:
On Applying Incremental Satisfiability to Delay Fault Testing. DATE 2000: 380-384 - [c23]Karem A. Sakallah, Fadi A. Aloul, João P. Marques Silva:
An Experimental Study of Satisfiability Search Heuristics. DATE 2000: 745 - [c22]Vasco M. Manquinho, João Marques-Silva:
Search Pruning Conditions for Boolean Optimization. ECAI 2000: 103-107
1990 – 1999
- 1999
- [j2]João P. Marques Silva
GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. Computers 48(5): 506-521 (1999) - [c21]João Marques-Silva, Thomas Glass:
Combinational Equivalence Checking Using Satisfiability and Recursive Learning. DATE 1999: 145-149 - [c20]Luís Guerra e Silva, Luís Miguel Silveira
Algorithms for Solving Boolean Satisfiability in Combinational Circuits. DATE 1999: 526-530 - [c19]João Marques-Silva:
The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. EPIA 1999: 62-74 - [c18]Paulo F. Flores, Horácio C. Neto, João P. Marques Silva:
On Applying Set Covering Models to Test Set Compaction. Great Lakes Symposium on VLSI 1999: 8-11 - [c17]Joonyoung Kim, João Marques-Silva, Karem A. Sakallah:
Satisfiability-Based Functional Delay Fault Testing. VLSI 1999: 362-372 - [c16]Paulo F. Flores, Horácio C. Neto, Krishnendu Chakrabarty, João Marques-Silva:
Test pattern generation for width compression in BIST. ISCAS (1) 1999: 114-118 - [c15]Paulo F. Flores, José C. Costa, Horácio C. Neto, José Monteiro, João Marques-Silva:
Assignment and Reordering of Incompletely Specified Pattern Sequences Targetting Minimum Power Dissipation. VLSI Design 1999: 37-41 - 1998
- [c14]João P. Marques Silva:
Integer Programming Models for Optimization Problems in Test Generation. ASP-DAC 1998: 481-487 - [c13]Paulo F. Flores, Horácio C. Neto, João P. Marques Silva:
An exact solution to the minimum size test pattern problem. ICCD 1998: 510-515 - [c12]Luís Guerra e Silva
Timing analysis using propositional satisfiability. ICECS 1998: 95-98 - [c11]Arlindo L. Oliveira
Efficient Search Techniques for the Inference of Minimum Size Finite Automata. SPIRE 1998: 81-89 - 1997
- [c10]João P. Marques Silva, Karem A. Sakallah:
Robust Search Algorithms for Test Pattern Generation. FTCS 1997: 152-161 - [c9]Vasco M. Manquinho, Paulo F. Flores, João P. Marques Silva, Arlindo L. Oliveira:
Prime Implicant Computation Using Satisfiability Algorithms. ICTAI 1997: 232-239 - 1996
- [j1]Michael A. Riepe, João P. Marques Silva
Ravel-XL: a hardware accelerator for assigned-delay compiled-code logic gate simulation. IEEE Trans. Very Large Scale Integr. Syst. 4(1): 113-129 (1996) - [c8]João P. Marques Silva, Karem A. Sakallah:
GRASP - a new search algorithm for satisfiability. ICCAD 1996: 220-227 - [c7]João P. Marques Silva, Karem A. Sakallah:
Conflict Analysis in Search Algorithms for Satisfiability. ICTAI 1996: 467-469 - 1994
- [c6]João P. Marques Silva, Karem A. Sakallah:
Dynamic Search-Space Pruning Techniques in Path Sensitization. DAC 1994: 705-711 - [c5]João P. Marques Silva, Karem A. Sakallah:
Efficient and Robust Test Generation-Based Timing Analysis. ISCAS 1994: 303-306 - 1993
- [c4]João P. Marques Silva, Karem A. Sakallah:
Concurrent path sensitization in timing analysis. EURO-DAC 1993: 196-199 - [c3]João P. Marques Silva, Karem A. Sakallah:
An Analysis of Path Sensitization Criteria. ICCD 1993: 68-72 - [c2]Michael A. Riepe, João P. Marques Silva, Karem A. Sakallah, Richard B. Brown:
Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation. ICCD 1993: 361-364 - 1991
- [c1]João P. Marques Silva, Karem A. Sakallah, Luís M. Vidigal:
FPD - An Environment for Exact Timing Analysis. ICCAD 1991: 212-215
Coauthor Index
[c214] [c210] [i66] [j56] [j55] [c208] [c204] [i59] [j54] [c199] [c198] [c197] [c196] [i51] [i50] [i49] [i45] [j53] [c194] [c191] [c190] [c188] [c187] [c186] [c185] [i44] [i42] [i40] [i39] [i38] [i37] [c184] [c183] [c182] [c180] [i35] [i34] [i33] [j49] [c178] [c176] [c175] [c174] [c173] [c172] [c171] [i32] [c170] [c168] [c166] [c165] [i30] [c163] [c161] [c160] [c159] [c158] [c157] [i29] [i28] [i27] [j44] [j41] [c153] [c152] [c151] [c150] [c149] [i26] [c148] [c145] [c143] [c140] [j36] [c135] [c134] [c132] [c127] [c117] [c113]
[p6] [j40] [j37] [c135] [c134] [p4] [j33] [j30] [c110] [j26] [j25] [j23] [c92] [p3] [j21] [c86] [c85] [c84] [c78] [j19] [c77] [c72] [p2] [i10] [j18] [j17] [c68] [c64] [c63] [p1] [i4] [j15] [j14] [c59] [c58] [c57] [c55] [c54] [c53] [c52] [j12] [j11] [c44] [c43] [c40] [j9] [c38] [c37] [c36] [c35] [c34] [c33] [j5] [c32] [c31]
Vasco Manquinho
aka: Vasco M. Manquinho
aka: Vasco M. Manquinho
[c210] [i66] [c201] [i58] [i47] [j53] [j49] [c176] [c175] [c172] [c170] [c165] [c161] [c158] [c157] [i29] [i28] [i27] [j44] [c152] [i26] [j39] [c145] [c143] [j36] [c137] [c135] [c134] [c127] [j35] [c120] [c118] [c117] [i18] [c111] [c107] [c106] [c104] [c102] [c99] [c96] [i14] [j22] [c62] [i3] [c51] [c47]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-19 22:14 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: