Edit Profile (opens in new tab) Marques-Silva, João P. Co-Author Distance Author ID: marques-silva.joao-p Published as: Marques-Silva, Joao; Marques-Silva, João; Marques-Silva, João P.; Marques-Silva, J. more...less Documents Indexed: 105 Publications since 1999 1 Contribution as Editor Software Indexed: 13 Packages Co-Authors: 73 Co-Authors with 99 Joint Publications 1,400 Co-Co-Authors all top 5 Co-Authors 7 single-authored 27 Lynce, Inês 23 Ignatyev, Alexey A. 17 Morgado, António 15 Janota, Mikoláš 9 Belov, Anton 9 Manquinho, Vasco M. 9 Mencía, Carlos 6 Previti, Alessandro 6 Sakallah, Karem A. 5 Planes, Jordi 4 Graça, Ana 3 Baptista, Luís 3 Cooper, Martin C. 3 Heras, Federico 3 Huang, Xuanxiang 3 Kullmann, Oliver 3 Liffiton, Mark H. 3 Narodytska, Nina 3 Oliveira, Arlindo L. 2 Andraus, Zaher S. 2 Arif, M. Fareed 2 Bhalla, Ateet 2 Bonet, Maria Luisa 2 Buss, Samuel R. 2 Clarke, Edmund Melson jun. 2 de Sousa, José T. 2 Grigore, Radu 2 Izza, Yacine 2 Järvisalo, Matti 2 Klieber, William 2 Manthey, Norbert 2 Mneimneh, Maher 2 Peñaloza, Rafael 1 Alviano, Mario 1 Argelich, Josep 1 Baaj, Ismaïl 1 Bordeaux, Lucas 1 Bouraoui, Zied 1 Chen, Huan 1 Cornuéjols, Antoine 1 Cruz-Filipe, Luís 1 Denœux, Thierry 1 Destercke, Sébastien 1 Dodaro, Carmine 1 Dubois, Didier 1 Heule, Marijn J. H. 1 Hurault, Aurélie 1 Ivrii, Alexander 1 Jabbour, Said 1 Katebi, Hadi 1 Kochemazov, Stepan 1 Lesot, Marie-Jeanne 1 Letombe, Florian 1 Malik, Ammar 1 Malik, Sharad 1 Matos, Paulo Rogério Faustino 1 Matsliah, Arie 1 Meel, Kuldeep S. 1 Mengin, Jérôme 1 Pereira, Felipe 1 Prade, Henri M. 1 Prestwich, Steven D. 1 Ricca, Francesco 1 Saïs, Lakhdar 1 Salhi, Yakoub 1 Schneider-Kamp, Peter 1 Schockaert, Steven 1 Serrurier, Mathieu 1 Shrotri, Aditya A. 1 Strauss, Olivier 1 Ulyantsev, Vladimir 1 Vrain, Christel 1 Zakirzyanov, Ilya all top 5 Serials 6 Artificial Intelligence 5 Constraints 5 Journal of Satisfiability, Boolean Modeling and Computation 4 AI Communications 4 Annals of Mathematics and Artificial Intelligence 3 International Journal of Approximate Reasoning 2 Journal of Automated Reasoning 2 Fundamenta Informaticae 1 Discrete Applied Mathematics 1 IEEE Transactions on Computers 1 Theoretical Computer Science 1 Journal of Algorithms 1 Annals of Operations Research 1 Journal of Logic and Computation 1 The Journal of Artificial Intelligence Research (JAIR) 1 Bulletin of the European Association for Theoretical Computer Science EATCS 1 Journal of Multiple-Valued Logic and Soft Computing 1 Lecture Notes in Computer Science all top 5 Fields 95 Computer science (68-XX) 18 Operations research, mathematical programming (90-XX) 11 Mathematical logic and foundations (03-XX) 6 Biology and other natural sciences (92-XX) 2 Combinatorics (05-XX) 2 Information and communication theory, circuits (94-XX) 1 General and overarching topics; collections (00-XX) 1 Statistics (62-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 98 Publications have been cited 952 times in 522 Documents Cited by ▼ Year ▼ GRASP: a search algorithm for propositional satisfiability. Zbl 1392.68388 Marques-Silva, João P.; Sakallah, Karem A. 144 1999 Expansion-based QBF solving versus Q-resolution. Zbl 1309.68168 Janota, Mikoláš; Marques-Silva, Joao 43 2015 Iterative and core-guided maxsat solving: a survey and assessment. Zbl 1317.90199 Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao 39 2013 PySAT: a Python toolkit for prototyping with SAT oracles. Zbl 1484.68215 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 35 2018 Solving QBF with counterexample guided refinement. Zbl 1273.68178 Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund 32 2012 Fast, flexible MUS enumeration. Zbl 1334.90080 Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao 31 2016 Algorithms for weighted Boolean optimization. Zbl 1247.68258 Manquinho, Vasco; Marques-Silva, Joao; Planes, Jordi 28 2009 Solving QBF with counterexample guided refinement. Zbl 1351.68254 Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund 26 2016 Boolean lexicographic optimization: algorithms & applications. Zbl 1242.90199 Marques-Silva, Joao; Argelich, Josep; Graça, Ana; Lynce, Inês 22 2011 Towards efficient MUS extraction. Zbl 1248.68450 Belov, Anton; Lynce, Inês; Marques-Silva, Joao 21 2012 MUSer2: an efficient MUS extractor. Zbl 1322.68178 Belov, Anton; Marques-Silva, Joao 20 2014 A SAT-based approach to learn explainable decision sets. Zbl 1511.68249 Ignatiev, Alexey; Pereira, Filipe; Narodytska, Nina; Marques-Silva, Joao 20 2018 Abstraction-based algorithm for 2QBF. Zbl 1330.68115 Janota, Mikoláš; Marques-Silva, Joao 16 2011 RC2: an efficient MaxSAT solver. Zbl 1484.68216 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 16 2019 Algorithms for computing backbones of propositional formulae. Zbl 1373.68379 Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao 15 2015 Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. Zbl 1187.68552 Kullmann, Oliver; Lynce, Inês; Marques-Silva, João 14 2006 On the query complexity of selecting minimal sets for monotone predicates. Zbl 1351.68117 Janota, Mikoláš; Marques-Silva, Joao 13 2016 On improving MUS extraction algorithms. Zbl 1330.68273 Marques-Silva, Joao; Lynce, Ines 12 2011 Improvements to core-guided binary search for MaxSAT. Zbl 1273.68357 Morgado, Antonio; Heras, Federico; Marques-Silva, Joao 12 2012 Using randomization and learning to solve hard real-world instances of satisfiability. Zbl 1044.68736 Baptista, Luís; Marques-Silva, João 12 2000 Minimal sets on propositional formulae. Problems and reductions. Zbl 1419.68098 Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos 12 2017 A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Zbl 1181.90291 Liffiton, Mark; Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem 12 2009 Towards robust CNF encodings of cardinality constraints. Zbl 1145.68525 Marques-Silva, Joao; Lynce, Inês 11 2007 Knowledge compilation with empowerment. Zbl 1302.68248 Bordeaux, Lucas; Marques-Silva, Joao 11 2012 On propositional QBF expansions and Q-resolution. Zbl 1390.03017 Janota, Mikoláš; Marques-Silva, Joao 11 2013 Optimum stable model search: algorithms and implementation. Zbl 1487.68206 Alviano, Mario; Dodaro, Carmine; Marques-Silva, Joao; Ricca, Francesco 10 2020 Propositional SAT solving. Zbl 1392.68380 Marques-Silva, Joao; Malik, Sharad 9 2018 A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. Zbl 1128.68477 Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem 9 2005 Towards more effective unsatisfiability-based maximum satisfiability algorithms. Zbl 1138.68548 Marques-Silva, Joao; Manquinho, Vasco 9 2008 On tackling explanation redundancy in decision trees. Zbl 07603113 Izza, Yacine; Ignatiev, Alexey; Marques-Silva, Joao 9 2022 Assessing heuristic machine learning explanations with model counting. Zbl 1441.68211 Narodytska, Nina; Shrotri, Aditya; Meel, Kuldeep S.; Ignatiev, Alexey; Marques-Silva, Joao 9 2019 Empirical study of the anatomy of modern SAT solvers. Zbl 1330.68271 Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, João P. 8 2011 Algebraic simplification techniques for propositional satisfiability. Zbl 1044.68781 Marques-Silva, João 8 2000 Progression in maximum satisfiability. Zbl 1366.68266 Ignatiev, A.; Morgado, A.; Manquinho, V.; Lynce, I.; Marques-Silva, J. 8 2014 Computing minimally unsatisfiable subformulas: state of the art and future directions. Zbl 1394.68359 Marques-Silva, Joao 8 2012 Efficient haplotype inference with pseudo-Boolean optimization. Zbl 1126.92035 Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L. 8 2007 MUS extraction using clausal proofs. Zbl 1423.68436 Belov, Anton; Heule, Marijn J. H.; Marques-Silva, Joao 7 2014 On computing preferred MUSes and MCSes. Zbl 1423.68460 Marques-Silva, Joao; Previti, Alessandro 7 2014 BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies. Zbl 1475.68368 Arif, M. Fareed; Mencía, Carlos; Ignatiev, Alexey; Manthey, Norbert; Peñaloza, Rafael; Marques-Silva, Joao 7 2016 Quantified maximum satisfiability. Zbl 1334.90075 Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao 7 2016 On tackling the limits of resolution in SAT solving. Zbl 1496.68368 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 7 2017 SAT-based rigorous explanations for decision lists. Zbl 07495578 Ignatiev, Alexey; Marques-Silva, Joao 7 2021 On computing backbones of propositional theories. Zbl 1211.68389 Marques-Silva, Joao; Janota, Mikoláš; Lynce, Inês 6 2010 Counterexample guided abstraction refinement algorithm for propositional circumscription. Zbl 1306.68190 Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao 6 2010 Interpolant learning and reuse in SAT-based model checking. Zbl 1277.68140 Marques-Silva, Joao 6 2007 Algorithms for computing minimal equivalent subformulas. Zbl 1405.68340 Belov, Anton; Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao 6 2014 An overview of backtrack search satisfiability algorithms. Zbl 1010.68069 Lynce, Inês; Marques-Silva, João P. 6 2003 Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. Zbl 1471.68173 Arif, M. Fareed; Mencía, Carlos; Marques-Silva, Joao 6 2015 MCS extraction with sublinear oracle queries. Zbl 1475.68220 Mencía, Carlos; Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao 6 2016 Enumerating prime implicants of propositional formulae in conjunctive normal form. Zbl 1432.68327 Jabbour, Said; Marques-Silva, Joao; Sais, Lakhdar; Salhi, Yakoub 6 2014 On computing the union of MUSes. Zbl 1441.68230 Mencía, Carlos; Kullmann, Oliver; Ignatiev, Alexey; Marques-Silva, Joao 6 2019 Efficient and accurate haplotype inference by combining parsimony and pedigree information. Zbl 1256.92037 Graça, Ana; Lynce, Inês; Marques-Silva, João; Oliveira, Arlindo L. 5 2012 On QBF proofs and preprocessing. Zbl 1407.68454 Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao 5 2013 Quantified maximum satisfiability: a core-guided approach. Zbl 1390.68598 Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao 5 2013 SAT-based preprocessing for MaxSAT. Zbl 1406.68108 Belov, Anton; Morgado, António; Marques-Silva, Joao 5 2013 Formula preprocessing in MUS extraction. Zbl 1381.68146 Belov, Anton; Järvisalo, Matti; Marques-Silva, Joao 5 2013 Satisfiability-based algorithms for Boolean optimization. Zbl 1068.90081 Manquinho, Vasco M.; Marques-Silva, João P. 5 2004 Computing maximal autarkies with few and simple oracle queries. Zbl 1471.68250 Kullmann, Oliver; Marques-Silva, Joao 5 2015 Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 1468.68318 Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter 5 2019 Boosting haplotype inference with local search. Zbl 1142.92030 Lynce, Inês; Marques-Silva, João; Prestwich, Steve 4 2008 Improvements to the implementation of interpolant-based model checking. Zbl 1159.68330 Marques-Silva, João 4 2005 On efficient computation of variable MUSes. Zbl 1273.03047 Belov, Anton; Ivrii, Alexander; Matsliah, Arie; Marques-Silva, Joao 4 2012 On reducing maximum independent set to minimum satisfiability. Zbl 1423.68452 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 4 2014 Efficient reasoning for inconsistent Horn formulae. Zbl 1483.68381 Marques-Silva, Joao; Ignatiev, Alexey; Mencía, Carlos; Peñaloza, Rafael 4 2016 Efficient data structures for backtrack search SAT solvers. Zbl 1099.68025 Lynce, Inês; Marques-Silva, João 4 2005 Random backtracking in backtrack search algorithms for satisfiability. Zbl 1121.68109 Lynce, I.; Marques-Silva, J. 4 2007 DRMaxSAT with MaxHS: first contact. Zbl 1441.68232 Morgado, Antonio; Ignatiev, Alexey; Bonet, Maria Luisa; Marques-Silva, Joao; Buss, Sam 4 2019 Haplotype inference with pseudo-Boolean optimization. Zbl 1215.92043 Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L. 3 2011 Heuristic-based backtracking for propositional satisfiability. Zbl 1205.68370 Bhalla, A.; Lynce, I.; de Sousa, J. T.; Marques-Silva, J. 3 2003 Stochastic systematic search algorithms for satisfiability. Zbl 0990.90554 Lynce, Inês; Baptista, Luís; Marques-Silva, João 3 2001 Towards provably complete stochastic search algorithms for satisfiability. Zbl 1053.68684 Lynce, Ines; Baptista, Luís; Marques-Silva, João 3 2001 On using cutting planes in pseudo-Boolean optimization. Zbl 1177.90297 Manquinho, Vasco M.; Marques-Silva, João 3 2006 PackUp: tools for package upgradability solving. Zbl 1348.68228 Janota, Mikoláš; Lynce, Inês; Manquinho, Vasco; Marques-Silva, Joao 3 2012 MaxSAT-based encodings for Group MaxSAT. Zbl 1373.68377 Heras, Federico; Morgado, Antonio; Marques-Silva, Joao 3 2015 Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Zbl 1120.68007 3 2007 Reasoning about strong inconsistency in ASP. Zbl 07331031 Mencía, Carlos; Marques-Silva, Joao 3 2020 Minimally unsatisfiable Boolean circuits. Zbl 1330.68268 Belov, Anton; Marques-Silva, Joao 2 2011 Combinatorial optimization solutions for the maximum quartet consistency problem. Zbl 1214.68364 Morgado, António; Marques-Silva, Joao 2 2010 Model checking with Boolean satisfiability. Zbl 1151.68031 Marques-Silva, Joao 2 2008 Maximal falsifiability. Definitions, algorithms, and applications. Zbl 1407.68453 Ignatiev, Alexey; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao 2 2013 Anatomy and empirical evaluation of modern SAT solvers. Zbl 1258.68137 Sakallah, Karem A.; Marques-Silva, Joao 2 2011 SAT-based formula simplification. Zbl 1471.68245 Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao 2 2015 TG-Pro: A SAT-based ATPG system. Zbl 1331.68204 Chen, Huan; Marques-Silva, Joao 2 2012 Improving MCS enumeration via caching. Zbl 1496.68258 Previti, Alessandro; Mencía, Carlos; Järvisalo, Matti; Marques-Silva, Joao 2 2017 Efficient symmetry breaking for SAT-based minimum DFA inference. Zbl 1425.68240 Zakirzyanov, Ilya; Morgado, Antonio; Ignatiev, Alexey; Ulyantsev, Vladimir; Marques-Silva, Joao 2 2019 Computing with SAT oracles: past, present and future. Zbl 1509.68103 Marques-Silva, Joao 2 2018 Propositional proof systems based on maximum satisfiability. Zbl 1520.68103 Bonet, Maria Luisa; Buss, Sam; Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 2 2021 On computing probabilistic abductive explanations. Zbl 07713736 Izza, Yacine; Huang, Xuanxiang; Ignatiev, Alexey; Narodytska, Nina; Cooper, Martin; Marques-Silva, Joao 2 2023 Symmetry breaking for maximum satisfiability. Zbl 1182.68257 Marques-Silva, Joao; Lynce, Inês; Manquinho, Vasco 1 2008 Improving SAT algorithms by using search pruning techniques. Zbl 1067.68650 Lynce, Inês; Marques-Silva, João 1 2001 On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization. Zbl 1128.68474 Manquinho, Vasco; Marques-Silva, João 1 2005 Improvements to hybrid incremental SAT algorithms. Zbl 1138.68544 Letombe, Florian; Marques-Silva, Joao 1 2008 Counting models in integer domains. Zbl 1187.90202 Morgado, António; Matos, Paulo; Manquinho, Vasco; Marques-Silva, João 1 2006 Certified logic-based explainable AI – the case of monotonic classifiers. Zbl 1541.68219 Hurault, Aurélie; Marques-Silva, Joao 1 2023 Feature necessity & relevancy in ML classifier explanations. Zbl 07777304 Huang, Xuanxiang; Cooper, Martin C.; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao 1 2023 Assessing progress in SAT solvers through the Lens of incremental SAT. Zbl 07495580 Kochemazov, Stepan; Ignatiev, Alexey; Marques-Silva, Joao 1 2021 On the failings of Shapley values for explainability. Zbl 07885914 Huang, Xuanxiang; Marques-Silva, Joao 1 2024 Tractability of explaining classifier decisions. Zbl 07697281 Cooper, Martin C.; Marques-Silva, João 1 2023 On the failings of Shapley values for explainability. Zbl 07885914 Huang, Xuanxiang; Marques-Silva, Joao 1 2024 On computing probabilistic abductive explanations. Zbl 07713736 Izza, Yacine; Huang, Xuanxiang; Ignatiev, Alexey; Narodytska, Nina; Cooper, Martin; Marques-Silva, Joao 2 2023 Certified logic-based explainable AI – the case of monotonic classifiers. Zbl 1541.68219 Hurault, Aurélie; Marques-Silva, Joao 1 2023 Feature necessity & relevancy in ML classifier explanations. Zbl 07777304 Huang, Xuanxiang; Cooper, Martin C.; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao 1 2023 Tractability of explaining classifier decisions. Zbl 07697281 Cooper, Martin C.; Marques-Silva, João 1 2023 On tackling explanation redundancy in decision trees. Zbl 07603113 Izza, Yacine; Ignatiev, Alexey; Marques-Silva, Joao 9 2022 SAT-based rigorous explanations for decision lists. Zbl 07495578 Ignatiev, Alexey; Marques-Silva, Joao 7 2021 Propositional proof systems based on maximum satisfiability. Zbl 1520.68103 Bonet, Maria Luisa; Buss, Sam; Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 2 2021 Assessing progress in SAT solvers through the Lens of incremental SAT. Zbl 07495580 Kochemazov, Stepan; Ignatiev, Alexey; Marques-Silva, Joao 1 2021 Optimum stable model search: algorithms and implementation. Zbl 1487.68206 Alviano, Mario; Dodaro, Carmine; Marques-Silva, Joao; Ricca, Francesco 10 2020 Reasoning about strong inconsistency in ASP. Zbl 07331031 Mencía, Carlos; Marques-Silva, Joao 3 2020 RC2: an efficient MaxSAT solver. Zbl 1484.68216 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 16 2019 Assessing heuristic machine learning explanations with model counting. Zbl 1441.68211 Narodytska, Nina; Shrotri, Aditya; Meel, Kuldeep S.; Ignatiev, Alexey; Marques-Silva, Joao 9 2019 On computing the union of MUSes. Zbl 1441.68230 Mencía, Carlos; Kullmann, Oliver; Ignatiev, Alexey; Marques-Silva, Joao 6 2019 Formally verifying the solution to the Boolean Pythagorean triples problem. Zbl 1468.68318 Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter 5 2019 DRMaxSAT with MaxHS: first contact. Zbl 1441.68232 Morgado, Antonio; Ignatiev, Alexey; Bonet, Maria Luisa; Marques-Silva, Joao; Buss, Sam 4 2019 Efficient symmetry breaking for SAT-based minimum DFA inference. Zbl 1425.68240 Zakirzyanov, Ilya; Morgado, Antonio; Ignatiev, Alexey; Ulyantsev, Vladimir; Marques-Silva, Joao 2 2019 PySAT: a Python toolkit for prototyping with SAT oracles. Zbl 1484.68215 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 35 2018 A SAT-based approach to learn explainable decision sets. Zbl 1511.68249 Ignatiev, Alexey; Pereira, Filipe; Narodytska, Nina; Marques-Silva, Joao 20 2018 Propositional SAT solving. Zbl 1392.68380 Marques-Silva, Joao; Malik, Sharad 9 2018 Computing with SAT oracles: past, present and future. Zbl 1509.68103 Marques-Silva, Joao 2 2018 Minimal sets on propositional formulae. Problems and reductions. Zbl 1419.68098 Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos 12 2017 On tackling the limits of resolution in SAT solving. Zbl 1496.68368 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 7 2017 Improving MCS enumeration via caching. Zbl 1496.68258 Previti, Alessandro; Mencía, Carlos; Järvisalo, Matti; Marques-Silva, Joao 2 2017 Fast, flexible MUS enumeration. Zbl 1334.90080 Liffiton, Mark H.; Previti, Alessandro; Malik, Ammar; Marques-Silva, Joao 31 2016 Solving QBF with counterexample guided refinement. Zbl 1351.68254 Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund 26 2016 On the query complexity of selecting minimal sets for monotone predicates. Zbl 1351.68117 Janota, Mikoláš; Marques-Silva, Joao 13 2016 BEACON: an efficient SAT-based tool for debugging \(\mathcal {EL}^+\) ontologies. Zbl 1475.68368 Arif, M. Fareed; Mencía, Carlos; Ignatiev, Alexey; Manthey, Norbert; Peñaloza, Rafael; Marques-Silva, Joao 7 2016 Quantified maximum satisfiability. Zbl 1334.90075 Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao 7 2016 MCS extraction with sublinear oracle queries. Zbl 1475.68220 Mencía, Carlos; Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao 6 2016 Efficient reasoning for inconsistent Horn formulae. Zbl 1483.68381 Marques-Silva, Joao; Ignatiev, Alexey; Mencía, Carlos; Peñaloza, Rafael 4 2016 Expansion-based QBF solving versus Q-resolution. Zbl 1309.68168 Janota, Mikoláš; Marques-Silva, Joao 43 2015 Algorithms for computing backbones of propositional formulae. Zbl 1373.68379 Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao 15 2015 Efficient MUS enumeration of Horn formulae with applications to axiom pinpointing. Zbl 1471.68173 Arif, M. Fareed; Mencía, Carlos; Marques-Silva, Joao 6 2015 Computing maximal autarkies with few and simple oracle queries. Zbl 1471.68250 Kullmann, Oliver; Marques-Silva, Joao 5 2015 MaxSAT-based encodings for Group MaxSAT. Zbl 1373.68377 Heras, Federico; Morgado, Antonio; Marques-Silva, Joao 3 2015 SAT-based formula simplification. Zbl 1471.68245 Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao 2 2015 MUSer2: an efficient MUS extractor. Zbl 1322.68178 Belov, Anton; Marques-Silva, Joao 20 2014 Progression in maximum satisfiability. Zbl 1366.68266 Ignatiev, A.; Morgado, A.; Manquinho, V.; Lynce, I.; Marques-Silva, J. 8 2014 MUS extraction using clausal proofs. Zbl 1423.68436 Belov, Anton; Heule, Marijn J. H.; Marques-Silva, Joao 7 2014 On computing preferred MUSes and MCSes. Zbl 1423.68460 Marques-Silva, Joao; Previti, Alessandro 7 2014 Algorithms for computing minimal equivalent subformulas. Zbl 1405.68340 Belov, Anton; Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao 6 2014 Enumerating prime implicants of propositional formulae in conjunctive normal form. Zbl 1432.68327 Jabbour, Said; Marques-Silva, Joao; Sais, Lakhdar; Salhi, Yakoub 6 2014 On reducing maximum independent set to minimum satisfiability. Zbl 1423.68452 Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao 4 2014 Iterative and core-guided maxsat solving: a survey and assessment. Zbl 1317.90199 Morgado, Antonio; Heras, Federico; Liffiton, Mark; Planes, Jordi; Marques-Silva, Joao 39 2013 On propositional QBF expansions and Q-resolution. Zbl 1390.03017 Janota, Mikoláš; Marques-Silva, Joao 11 2013 On QBF proofs and preprocessing. Zbl 1407.68454 Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao 5 2013 Quantified maximum satisfiability: a core-guided approach. Zbl 1390.68598 Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao 5 2013 SAT-based preprocessing for MaxSAT. Zbl 1406.68108 Belov, Anton; Morgado, António; Marques-Silva, Joao 5 2013 Formula preprocessing in MUS extraction. Zbl 1381.68146 Belov, Anton; Järvisalo, Matti; Marques-Silva, Joao 5 2013 Maximal falsifiability. Definitions, algorithms, and applications. Zbl 1407.68453 Ignatiev, Alexey; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao 2 2013 Solving QBF with counterexample guided refinement. Zbl 1273.68178 Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund 32 2012 Towards efficient MUS extraction. Zbl 1248.68450 Belov, Anton; Lynce, Inês; Marques-Silva, Joao 21 2012 Improvements to core-guided binary search for MaxSAT. Zbl 1273.68357 Morgado, Antonio; Heras, Federico; Marques-Silva, Joao 12 2012 Knowledge compilation with empowerment. Zbl 1302.68248 Bordeaux, Lucas; Marques-Silva, Joao 11 2012 Computing minimally unsatisfiable subformulas: state of the art and future directions. Zbl 1394.68359 Marques-Silva, Joao 8 2012 Efficient and accurate haplotype inference by combining parsimony and pedigree information. Zbl 1256.92037 Graça, Ana; Lynce, Inês; Marques-Silva, João; Oliveira, Arlindo L. 5 2012 On efficient computation of variable MUSes. Zbl 1273.03047 Belov, Anton; Ivrii, Alexander; Matsliah, Arie; Marques-Silva, Joao 4 2012 PackUp: tools for package upgradability solving. Zbl 1348.68228 Janota, Mikoláš; Lynce, Inês; Manquinho, Vasco; Marques-Silva, Joao 3 2012 TG-Pro: A SAT-based ATPG system. Zbl 1331.68204 Chen, Huan; Marques-Silva, Joao 2 2012 Boolean lexicographic optimization: algorithms & applications. Zbl 1242.90199 Marques-Silva, Joao; Argelich, Josep; Graça, Ana; Lynce, Inês 22 2011 Abstraction-based algorithm for 2QBF. Zbl 1330.68115 Janota, Mikoláš; Marques-Silva, Joao 16 2011 On improving MUS extraction algorithms. Zbl 1330.68273 Marques-Silva, Joao; Lynce, Ines 12 2011 Empirical study of the anatomy of modern SAT solvers. Zbl 1330.68271 Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, João P. 8 2011 Haplotype inference with pseudo-Boolean optimization. Zbl 1215.92043 Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L. 3 2011 Minimally unsatisfiable Boolean circuits. Zbl 1330.68268 Belov, Anton; Marques-Silva, Joao 2 2011 Anatomy and empirical evaluation of modern SAT solvers. Zbl 1258.68137 Sakallah, Karem A.; Marques-Silva, Joao 2 2011 On computing backbones of propositional theories. Zbl 1211.68389 Marques-Silva, Joao; Janota, Mikoláš; Lynce, Inês 6 2010 Counterexample guided abstraction refinement algorithm for propositional circumscription. Zbl 1306.68190 Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao 6 2010 Combinatorial optimization solutions for the maximum quartet consistency problem. Zbl 1214.68364 Morgado, António; Marques-Silva, Joao 2 2010 Algorithms for weighted Boolean optimization. Zbl 1247.68258 Manquinho, Vasco; Marques-Silva, Joao; Planes, Jordi 28 2009 A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Zbl 1181.90291 Liffiton, Mark; Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem 12 2009 Towards more effective unsatisfiability-based maximum satisfiability algorithms. Zbl 1138.68548 Marques-Silva, Joao; Manquinho, Vasco 9 2008 Boosting haplotype inference with local search. Zbl 1142.92030 Lynce, Inês; Marques-Silva, João; Prestwich, Steve 4 2008 Model checking with Boolean satisfiability. Zbl 1151.68031 Marques-Silva, Joao 2 2008 Symmetry breaking for maximum satisfiability. Zbl 1182.68257 Marques-Silva, Joao; Lynce, Inês; Manquinho, Vasco 1 2008 Improvements to hybrid incremental SAT algorithms. Zbl 1138.68544 Letombe, Florian; Marques-Silva, Joao 1 2008 Towards robust CNF encodings of cardinality constraints. Zbl 1145.68525 Marques-Silva, Joao; Lynce, Inês 11 2007 Efficient haplotype inference with pseudo-Boolean optimization. Zbl 1126.92035 Graça, Ana; Marques-Silva, João; Lynce, Inês; Oliveira, Arlindo L. 8 2007 Interpolant learning and reuse in SAT-based model checking. Zbl 1277.68140 Marques-Silva, Joao 6 2007 Random backtracking in backtrack search algorithms for satisfiability. Zbl 1121.68109 Lynce, I.; Marques-Silva, J. 4 2007 Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Zbl 1120.68007 3 2007 Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. Zbl 1187.68552 Kullmann, Oliver; Lynce, Inês; Marques-Silva, João 14 2006 On using cutting planes in pseudo-Boolean optimization. Zbl 1177.90297 Manquinho, Vasco M.; Marques-Silva, João 3 2006 Counting models in integer domains. Zbl 1187.90202 Morgado, António; Matos, Paulo; Manquinho, Vasco; Marques-Silva, João 1 2006 A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. Zbl 1128.68477 Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem 9 2005 Improvements to the implementation of interpolant-based model checking. Zbl 1159.68330 Marques-Silva, João 4 2005 Efficient data structures for backtrack search SAT solvers. Zbl 1099.68025 Lynce, Inês; Marques-Silva, João 4 2005 On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization. Zbl 1128.68474 Manquinho, Vasco; Marques-Silva, João 1 2005 Satisfiability-based algorithms for Boolean optimization. Zbl 1068.90081 Manquinho, Vasco M.; Marques-Silva, João P. 5 2004 An overview of backtrack search satisfiability algorithms. Zbl 1010.68069 Lynce, Inês; Marques-Silva, João P. 6 2003 Heuristic-based backtracking for propositional satisfiability. Zbl 1205.68370 Bhalla, A.; Lynce, I.; de Sousa, J. T.; Marques-Silva, J. 3 2003 Stochastic systematic search algorithms for satisfiability. Zbl 0990.90554 Lynce, Inês; Baptista, Luís; Marques-Silva, João 3 2001 Towards provably complete stochastic search algorithms for satisfiability. Zbl 1053.68684 Lynce, Ines; Baptista, Luís; Marques-Silva, João 3 2001 Improving SAT algorithms by using search pruning techniques. Zbl 1067.68650 Lynce, Inês; Marques-Silva, João 1 2001 Using randomization and learning to solve hard real-world instances of satisfiability. Zbl 1044.68736 Baptista, Luís; Marques-Silva, João 12 2000 Algebraic simplification techniques for propositional satisfiability. Zbl 1044.68781 Marques-Silva, João 8 2000 GRASP: a search algorithm for propositional satisfiability. Zbl 1392.68388 Marques-Silva, João P.; Sakallah, Karem A. 144 1999 all cited Publications top 5 cited Publications all top 5 Cited by 899 Authors 39 Marques-Silva, João P. 25 Beyersdorff, Olaf 14 Heule, Marijn J. H. 14 Ignatyev, Alexey A. 14 Janota, Mikoláš 13 Dodaro, Carmine 13 Lynce, Inês 12 Järvisalo, Matti 12 Szeider, Stefan 11 Biere, Armin 11 Nordström, Jakob 11 Seidl, Martina 10 Blinkhorn, Joshua 10 Mahajan, Meena 10 Ricca, Francesco 9 Chew, Leroy 8 Alviano, Mario 7 Ansótegui, Carlos 7 Lauria, Massimo 7 Lonsing, Florian 7 Manquinho, Vasco M. 7 Maratea, Marco 7 Mencía, Carlos 7 Previti, Alessandro 6 Gebser, Martin 6 Habet, Djamal 6 Morgado, António 6 Nieuwenhuis, Robert 6 Peñaloza, Rafael 6 Ryvchin, Vadim 6 Schaub, Torsten H. 6 Slivovsky, Friedrich 5 Bendík, Jaroslav 5 Berg, Jeremias 5 Bogaerts, Bart 5 Bonacina, Ilario 5 Bryant, Randal E. 5 Eiter, Thomas 5 Kullmann, Oliver 5 Liffiton, Mark H. 5 Meel, Kuldeep S. 5 Nadel, Alexander 5 Oliveras, Albert 5 Peitl, Tomáš 5 Rodríguez-Carbonell, Enric 5 Scholl, Christoph 5 Semenov, Aleksandr Anatol’evich 5 Strichman, Ofer 5 Vardi, Moshe Ya’akov 4 Amendola, Giovanni 4 Becker, Bernd 4 Böhm, Benjamin 4 Bonet, Maria Luisa 4 Cai, Shaowei 4 Egly, Uwe 4 Giunchiglia, Enrico 4 Grégoire, Éric 4 Hinde, Luke 4 Ivrii, Alexander 4 Janhunen, Tomi 4 Kaufmann, Benjamin 4 Kučera, Petr 4 Lagniez, Jean-Marie 4 Levy, Jordi 4 Li, Chumin 4 Martins, Ruben 4 Mazure, Bertrand 4 Piette, Cédric 4 Planes, Jordi 4 Shankar, Natarajan 4 Stuckey, Peter James 4 Suda, Martin 4 Tentrup, Leander 4 Vinyals, Marc 4 Wallner, Johannes Peter 4 Wimmer, Ralf D. 3 Ábrahám, Erika 3 Abramé, André 3 Achterberg, Tobias 3 Atserias, Albert 3 Banbara, Mutsunori 3 Barrett, Clark W. 3 Belov, Anton 3 Berthold, Timo 3 Buss, Samuel R. 3 Černá, Ivana 3 Cherif, Mohamed Sami 3 Cooper, Martin C. 3 de Rezende, Susanna F. 3 Fichte, Johannes Klaus 3 Finkbeiner, Bernd 3 Gabàs, Joel 3 Giráldez-Cru, Jesús 3 Goldberg, Eugene L. 3 Griggio, Alberto 3 Huang, Xuanxiang 3 Kiesl, Benjamin 3 Lierler, Yuliya 3 Manyà, Felip 3 Marquis, Pierre ...and 799 more Authors all top 5 Cited in 79 Serials 52 Artificial Intelligence 25 Journal of Automated Reasoning 25 Constraints 17 Formal Methods in System Design 15 Theory and Practice of Logic Programming 14 Theoretical Computer Science 13 Discrete Applied Mathematics 12 The Journal of Artificial Intelligence Research (JAIR) 12 Annals of Mathematics and Artificial Intelligence 12 Journal of Satisfiability, Boolean Modeling and Computation 9 Computers & Operations Research 8 ACM Transactions on Computational Logic 8 Logical Methods in Computer Science 7 International Journal of Approximate Reasoning 6 Information Processing Letters 6 European Journal of Operational Research 5 Journal of Symbolic Computation 5 Annals of Operations Research 4 Journal of Computer and System Sciences 4 SIAM Journal on Computing 3 ACM Journal of Experimental Algorithmics 3 Journal of Discrete Algorithms 2 Acta Informatica 2 Algorithmica 2 Information and Computation 2 AI Communications 2 The Electronic Journal of Combinatorics 2 The Bulletin of Symbolic Logic 2 Journal of Heuristics 2 INFORMS Journal on Computing 2 Theory of Computing Systems 2 Communications in Nonlinear Science and Numerical Simulation 2 Journal of Machine Learning Research (JMLR) 2 Natural Computing 2 Discrete Optimization 2 Journal of Logical and Algebraic Methods in Programming 2 Prikladnaya Diskretnaya Matematika 1 American Mathematical Monthly 1 Journal of the Franklin Institute 1 Mathematical Biosciences 1 Applied Mathematics and Computation 1 Computing 1 Fuzzy Sets and Systems 1 Information Sciences 1 Journal of Computational and Applied Mathematics 1 Journal of Economic Theory 1 Journal of Optimization Theory and Applications 1 Studia Logica 1 Tsukuba Journal of Mathematics 1 Mathematical Social Sciences 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 Discrete & Computational Geometry 1 Automation and Remote Control 1 Applicable Algebra in Engineering, Communication and Computing 1 Computational Complexity 1 Journal of Logic, Language and Information 1 Journal of the Egyptian Mathematical Society 1 Top 1 International Transactions in Operational Research 1 Mathematical Problems in Engineering 1 Journal of Combinatorial Optimization 1 International Journal of Applied Mathematics and Computer Science 1 Fundamenta Informaticae 1 International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems 1 Journal of Applied Mathematics 1 OR Spectrum 1 JMMA. Journal of Mathematical Modelling and Algorithms 1 Computational Management Science 1 Electronic Notes in Theoretical Computer Science 1 Mathematics in Computer Science 1 Optimization Letters 1 Acta Universitatis Sapientiae. Informatica 1 Mathematical Programming Computation 1 Statistics Surveys 1 Theory of Computing 1 Statistics and Computing 1 Palestine Journal of Mathematics 1 ACM Transactions on Computation Theory all top 5 Cited in 21 Fields 440 Computer science (68-XX) 112 Mathematical logic and foundations (03-XX) 88 Operations research, mathematical programming (90-XX) 14 Combinatorics (05-XX) 13 Biology and other natural sciences (92-XX) 10 Information and communication theory, circuits (94-XX) 9 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 7 Statistics (62-XX) 4 General and overarching topics; collections (00-XX) 3 Order, lattices, ordered algebraic structures (06-XX) 3 Number theory (11-XX) 2 Quantum theory (81-XX) 2 Systems theory; control (93-XX) 1 Commutative algebra (13-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Group theory and generalizations (20-XX) 1 Dynamical systems and ergodic theory (37-XX) 1 Geometry (51-XX) 1 Convex and discrete geometry (52-XX) 1 Probability theory and stochastic processes (60-XX) 1 Numerical analysis (65-XX) Citations by Year