Alviano, Mario; Dodaro, Carmine; Marques-Silva, Joao; Ricca, Francesco Optimum stable model search: algorithms and implementation. (English) Zbl 1487.68206 J. Log. Comput. 30, No. 4, 863-897 (2020). MSC: 68T20 68N17 PDFBibTeX XMLCite \textit{M. Alviano} et al., J. Log. Comput. 30, No. 4, 863--897 (2020; Zbl 1487.68206) Full Text: DOI
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao RC2: an efficient MaxSAT solver. (English) Zbl 1484.68216 J. Satisf. Boolean Model. Comput. 11, 53-64 (2019). MSC: 68T20 68V15 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., J. Satisf. Boolean Model. Comput. 11, 53--64 (2019; Zbl 1484.68216) Full Text: DOI
Morgado, Antonio; Ignatiev, Alexey; Bonet, Maria Luisa; Marques-Silva, Joao; Buss, Sam DRMaxSAT with MaxHS: first contact. (English) Zbl 1441.68232 Janota, Mikoláš (ed.) et al., Theory and applications of satisfiability testing – SAT 2019. 22nd international conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11628, 239-249 (2019). MSC: 68T20 68R07 PDFBibTeX XMLCite \textit{A. Morgado} et al., Lect. Notes Comput. Sci. 11628, 239--249 (2019; Zbl 1441.68232) Full Text: DOI
Mencía, Carlos; Kullmann, Oliver; Ignatiev, Alexey; Marques-Silva, Joao On computing the union of MUSes. (English) Zbl 1441.68230 Janota, Mikoláš (ed.) et al., Theory and applications of satisfiability testing – SAT 2019. 22nd international conference, SAT 2019, Lisbon, Portugal, July 9–12, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11628, 211-221 (2019). MSC: 68T20 68R07 PDFBibTeX XMLCite \textit{C. Mencía} et al., Lect. Notes Comput. Sci. 11628, 211--221 (2019; Zbl 1441.68230) Full Text: DOI Link
Ignatiev, Alexey; Pereira, Filipe; Narodytska, Nina; Marques-Silva, Joao A SAT-based approach to learn explainable decision sets. (English) Zbl 1511.68249 Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 627-645 (2018). MSC: 68T20 68T05 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Lect. Notes Comput. Sci. 10900, 627--645 (2018; Zbl 1511.68249) Full Text: DOI
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao PySAT: a Python toolkit for prototyping with SAT oracles. (English) Zbl 1484.68215 Beyersdorff, Olaf (ed.) et al., Theory and applications of satisfiability testing – SAT 2018. 21st international conference, SAT 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10929, 428-437 (2018). MSC: 68T20 68V15 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Lect. Notes Comput. Sci. 10929, 428--437 (2018; Zbl 1484.68215) Full Text: DOI
Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos Minimal sets on propositional formulae. Problems and reductions. (English) Zbl 1419.68098 Artif. Intell. 252, 22-50 (2017). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva} et al., Artif. Intell. 252, 22--50 (2017; Zbl 1419.68098) Full Text: DOI arXiv
Ignatiev, Alexey; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao Maximal falsifiability. Definitions, algorithms and applications. (English) Zbl 1373.68378 AI Commun. 29, No. 2, 351-370 (2016). MSC: 68T20 90C09 90C59 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., AI Commun. 29, No. 2, 351--370 (2016; Zbl 1373.68378) Full Text: DOI
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund Solving QBF with counterexample guided refinement. (English) Zbl 1351.68254 Artif. Intell. 234, 1-25 (2016). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Janota} et al., Artif. Intell. 234, 1--25 (2016; Zbl 1351.68254) Full Text: DOI
Heras, Federico; Morgado, Antonio; Marques-Silva, Joao MaxSAT-based encodings for Group MaxSAT. (English) Zbl 1373.68377 AI Commun. 28, No. 2, 195-214 (2015). MSC: 68T20 90C09 90C59 PDFBibTeX XMLCite \textit{F. Heras} et al., AI Commun. 28, No. 2, 195--214 (2015; Zbl 1373.68377) Full Text: DOI
Janota, Mikoláš; Lynce, Inês; Marques-Silva, Joao Algorithms for computing backbones of propositional formulae. (English) Zbl 1373.68379 AI Commun. 28, No. 2, 161-177 (2015). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Janota} et al., AI Commun. 28, No. 2, 161--177 (2015; Zbl 1373.68379) Full Text: DOI
Mencía, Carlos; Previti, Alessandro; Marques-Silva, Joao SAT-based Horn least upper bounds. (English) Zbl 1471.68256 Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 423-433 (2015). MSC: 68T20 03B05 03B35 68V15 PDFBibTeX XMLCite \textit{C. Mencía} et al., Lect. Notes Comput. Sci. 9340, 423--433 (2015; Zbl 1471.68256) Full Text: DOI
Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao SAT-based formula simplification. (English) Zbl 1471.68245 Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 287-298 (2015). MSC: 68T20 03B05 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Lect. Notes Comput. Sci. 9340, 287--298 (2015; Zbl 1471.68245) Full Text: DOI
Kullmann, Oliver; Marques-Silva, Joao Computing maximal autarkies with few and simple oracle queries. (English) Zbl 1471.68250 Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 138-155 (2015). MSC: 68T20 PDFBibTeX XMLCite \textit{O. Kullmann} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 9340, 138--155 (2015; Zbl 1471.68250) Full Text: DOI arXiv
Ignatiev, A.; Morgado, A.; Manquinho, V.; Lynce, I.; Marques-Silva, J. Progression in maximum satisfiability. (English) Zbl 1366.68266 Schaub, Torsten (ed.) et al., ECAI 2014. 21st European conference on artificial intelligence, Prague, Czech Republic, August 18–22, 2014. Proceedings. Including proceedings of the accompanied concerence on prestigious applications of intelligent systems (PAIS 2014). Amsterdam: IOS Press (ISBN 978-1-61499-418-3/pbk; 978-1-61499-419-0/ebook). Frontiers in Artificial Intelligence and Applications 263, 453-458 (2014). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Front. Artif. Intell. Appl. 263, 453--458 (2014; Zbl 1366.68266) Full Text: Link
Belov, Anton; Marques-Silva, Joao MUSer2: an efficient MUS extractor. (English) Zbl 1322.68178 J. Satisf. Boolean Model. Comput. 8(2012-2014), No. 3-4, 123-128 (2014). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{A. Belov} and \textit{J. Marques-Silva}, J. Satisf. Boolean Model. Comput. 8, No. 3--4, 123--128 (2014; Zbl 1322.68178)
Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao On reducing maximum independent set to minimum satisfiability. (English) Zbl 1423.68452 Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 103-120 (2014). MSC: 68T20 05C69 68Q25 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Lect. Notes Comput. Sci. 8561, 103--120 (2014; Zbl 1423.68452) Full Text: DOI
Marques-Silva, Joao; Previti, Alessandro On computing preferred MUSes and MCSes. (English) Zbl 1423.68460 Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 58-74 (2014). MSC: 68T20 68Q25 68T15 PDFBibTeX XMLCite \textit{J. Marques-Silva} and \textit{A. Previti}, Lect. Notes Comput. Sci. 8561, 58--74 (2014; Zbl 1423.68460) Full Text: DOI
Belov, Anton; Heule, Marijn J. H.; Marques-Silva, Joao MUS extraction using clausal proofs. (English) Zbl 1423.68436 Sinz, Carsten (ed.) et al., Theory and applications of satisfiability testing – SAT 2014. 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8561, 48-57 (2014). MSC: 68T20 68Q25 68T15 PDFBibTeX XMLCite \textit{A. Belov} et al., Lect. Notes Comput. Sci. 8561, 48--57 (2014; Zbl 1423.68436) Full Text: DOI
Janota, Mikoláš; Grigore, Radu; Marques-Silva, Joao On QBF proofs and preprocessing. (English) Zbl 1407.68454 McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8312, 473-489 (2013). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Janota} et al., Lect. Notes Comput. Sci. 8312, 473--489 (2013; Zbl 1407.68454) Full Text: DOI arXiv
Ignatiev, Alexey; Morgado, Antonio; Planes, Jordi; Marques-Silva, Joao Maximal falsifiability. Definitions, algorithms, and applications. (English) Zbl 1407.68453 McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8312, 439-456 (2013). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Lect. Notes Comput. Sci. 8312, 439--456 (2013; Zbl 1407.68453) Full Text: DOI
Belov, Anton; Morgado, António; Marques-Silva, Joao SAT-based preprocessing for MaxSAT. (English) Zbl 1406.68108 McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-45220-8/pbk). Lecture Notes in Computer Science 8312, 96-111 (2013). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Belov} et al., Lect. Notes Comput. Sci. 8312, 96--111 (2013; Zbl 1406.68108) Full Text: DOI arXiv
Ignatiev, Alexey; Janota, Mikoláš; Marques-Silva, Joao Quantified maximum satisfiability: a core-guided approach. (English) Zbl 1390.68598 Järvisalo, Matti (ed.) et al., Theory and applications of satisfiability testing – SAT 2013. 16th international conference, Helsinki, Finland, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39070-8/pbk). Lecture Notes in Computer Science 7962, 250-266 (2013). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Ignatiev} et al., Lect. Notes Comput. Sci. 7962, 250--266 (2013; Zbl 1390.68598) Full Text: DOI
Belov, Anton; Manthey, Norbert; Marques-Silva, Joao Parallel MUS extraction. (English) Zbl 1390.68588 Järvisalo, Matti (ed.) et al., Theory and applications of satisfiability testing – SAT 2013. 16th international conference, Helsinki, Finland, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39070-8/pbk). Lecture Notes in Computer Science 7962, 133-149 (2013). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{A. Belov} et al., Lect. Notes Comput. Sci. 7962, 133--149 (2013; Zbl 1390.68588) Full Text: DOI
Marques-Silva, Joao Computing minimally unsatisfiable subformulas: state of the art and future directions. (English) Zbl 1394.68359 J. Mult.-Val. Log. Soft Comput. 19, No. 1-3, 163-183 (2012). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva}, J. Mult.-Val. Log. Soft Comput. 19, No. 1--3, 163--183 (2012; Zbl 1394.68359) Full Text: Link
Janota, Mikoláš; Lynce, Inês; Manquinho, Vasco; Marques-Silva, Joao PackUp: tools for package upgradability solving. (English) Zbl 1348.68228 J. Satisf. Boolean Model. Comput. 8, No. 1-2, 89-94 (2012). MSC: 68T20 68N25 PDFBibTeX XMLCite \textit{M. Janota} et al., J. Satisf. Boolean Model. Comput. 8, No. 1--2, 89--94 (2012; Zbl 1348.68228)
Chen, Huan; Marques-Silva, Joao TG-Pro: A SAT-based ATPG system. (English) Zbl 1331.68204 J. Satisf. Boolean Model. Comput. 8, No. 1-2, 83-88 (2012). MSC: 68T20 PDFBibTeX XMLCite \textit{H. Chen} and \textit{J. Marques-Silva}, J. Satisf. Boolean Model. Comput. 8, No. 1--2, 83--88 (2012; Zbl 1331.68204)
Morgado, Antonio; Heras, Federico; Marques-Silva, Joao Improvements to core-guided binary search for MaxSAT. (English) Zbl 1273.68357 Cimatti, Alessandro (ed.) et al., Theory and applications of satisfiability testing – SAT 2012. 15th international conference, Trento, Italy, June 17–20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31611-1/pbk). Lecture Notes in Computer Science 7317, 284-297 (2012). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Morgado} et al., Lect. Notes Comput. Sci. 7317, 284--297 (2012; Zbl 1273.68357) Full Text: DOI Link
Belov, Anton; Lynce, Inês; Marques-Silva, Joao Towards efficient MUS extraction. (English) Zbl 1248.68450 AI Commun. 25, No. 2, 97-116 (2012). MSC: 68T20 68W05 PDFBibTeX XMLCite \textit{A. Belov} et al., AI Commun. 25, No. 2, 97--116 (2012; Zbl 1248.68450) Full Text: DOI
Bordeaux, Lucas; Marques-Silva, Joao Knowledge compilation with empowerment. (English) Zbl 1302.68248 Bieliková, Mária (ed.) et al., SOFSEM 2012: Theory and practice of computer science. 38th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 21–27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27659-0/pbk). Lecture Notes in Computer Science 7147, 612-624 (2012). MSC: 68T20 PDFBibTeX XMLCite \textit{L. Bordeaux} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 7147, 612--624 (2012; Zbl 1302.68248) Full Text: DOI Link
Sakallah, Karem A.; Marques-Silva, Joao Anatomy and empirical evaluation of modern SAT solvers. (English) Zbl 1258.68137 Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 103, 95-121 (2011). MSC: 68T20 68Q17 68Q32 PDFBibTeX XMLCite \textit{K. A. Sakallah} and \textit{J. Marques-Silva}, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 103, 95--121 (2011; Zbl 1258.68137)
Lynce, Inês; Marques-Silva, Joao Restoring CSP satisfiability with MaxSAT. (English) Zbl 1230.68181 Fundam. Inform. 107, No. 2-3, 249-266 (2011). MSC: 68T20 PDFBibTeX XMLCite \textit{I. Lynce} and \textit{J. Marques-Silva}, Fundam. Inform. 107, No. 2--3, 249--266 (2011; Zbl 1230.68181) Full Text: DOI
Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, João P. Empirical study of the anatomy of modern SAT solvers. (English) Zbl 1330.68271 Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 343-356 (2011). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{H. Katebi} et al., Lect. Notes Comput. Sci. 6695, 343--356 (2011; Zbl 1330.68271) Full Text: DOI
Marques-Silva, Joao; Lynce, Ines On improving MUS extraction algorithms. (English) Zbl 1330.68273 Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 159-173 (2011). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{J. Marques-Silva} and \textit{I. Lynce}, Lect. Notes Comput. Sci. 6695, 159--173 (2011; Zbl 1330.68273) Full Text: DOI
Belov, Anton; Marques-Silva, Joao Minimally unsatisfiable Boolean circuits. (English) Zbl 1330.68268 Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 145-158 (2011). MSC: 68T20 03B05 68T15 94C10 PDFBibTeX XMLCite \textit{A. Belov} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 6695, 145--158 (2011; Zbl 1330.68268) Full Text: DOI
Morgado, António; Marques-Silva, Joao Combinatorial optimization solutions for the maximum quartet consistency problem. (English) Zbl 1214.68364 Fundam. Inform. 102, No. 3-4, 363-389 (2010). MSC: 68T20 90C27 92D15 PDFBibTeX XMLCite \textit{A. Morgado} and \textit{J. Marques-Silva}, Fundam. Inform. 102, No. 3--4, 363--389 (2010; Zbl 1214.68364) Full Text: Link
Marques-Silva, Joao; Janota, Mikoláš; Lynce, Inês On computing backbones of propositional theories. (English) Zbl 1211.68389 Coelho, Helder (ed.) et al., ECAI 2010. 19th European conference on artificial intelligence, August 16–20, 2010 Lisbon, Portugal. Including proceedings of the 6th prestigious applications of artificial intelligence (PAIS-2010). Amsterdam: IOS Press (ISBN 978-1-60750-605-8/pbk; 978-1-60750-606-5/ebook). Frontiers in Artificial Intelligence and Applications 215, 15-20 (2010). MSC: 68T20 68Q60 PDFBibTeX XMLCite \textit{J. Marques-Silva} et al., Front. Artif. Intell. Appl. 215, 15--20 (2010; Zbl 1211.68389) Full Text: DOI
Manquinho, Vasco; Marques-Silva, Joao; Planes, Jordi Algorithms for weighted Boolean optimization. (English) Zbl 1247.68258 Kullmann, Oliver (ed.), Theory and applications of satisfiability testing – SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30–July 3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02776-5/pbk). Lecture Notes in Computer Science 5584, 495-508 (2009). MSC: 68T20 PDFBibTeX XMLCite \textit{V. Manquinho} et al., Lect. Notes Comput. Sci. 5584, 495--508 (2009; Zbl 1247.68258) Full Text: DOI
Marques-Silva, Joao; Lynce, Inês; Manquinho, Vasco Symmetry breaking for maximum satisfiability. (English) Zbl 1182.68257 Cervesato, Iliano (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 15th international conference, LPAR 2008, Doha, Qatar, November 22–27, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-89438-4/pbk). Lecture Notes in Computer Science 5330. Lecture Notes in Artificial Intelligence, 1-15 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva} et al., Lect. Notes Comput. Sci. 5330, 1--15 (2008; Zbl 1182.68257) Full Text: DOI Link
Marques-Silva, Joao; Manquinho, Vasco Towards more effective unsatisfiability-based maximum satisfiability algorithms. (English) Zbl 1138.68548 Kleine Büning, Hans (ed.) et al., Theory and applications of satisfiability testing – SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12–15, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79718-0/pbk). Lecture Notes in Computer Science 4996, 225-230 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva} and \textit{V. Manquinho}, Lect. Notes Comput. Sci. 4996, 225--230 (2008; Zbl 1138.68548) Full Text: DOI Link
Letombe, Florian; Marques-Silva, Joao Improvements to hybrid incremental SAT algorithms. (English) Zbl 1138.68544 Kleine Büning, Hans (ed.) et al., Theory and applications of satisfiability testing – SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12–15, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79718-0/pbk). Lecture Notes in Computer Science 4996, 168-181 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{F. Letombe} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 4996, 168--181 (2008; Zbl 1138.68544) Full Text: DOI Link
Marques-Silva, Joao; Lynce, Inês Towards robust CNF encodings of cardinality constraints. (English) Zbl 1145.68525 Bessière, Christian (ed.), Principles and practice of constraint programming – CP 2007. 13th international conference, CP 2007, Providence, RI, USA, September 23–27, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74969-1/pbk). Lecture Notes in Computer Science 4741, 483-497 (2007). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva} and \textit{I. Lynce}, Lect. Notes Comput. Sci. 4741, 483--497 (2007; Zbl 1145.68525) Full Text: DOI Link
Lynce, I.; Marques-Silva, J. Random backtracking in backtrack search algorithms for satisfiability. (English) Zbl 1121.68109 Discrete Appl. Math. 155, No. 12, 1604-1612 (2007). MSC: 68T20 68P10 68W20 PDFBibTeX XMLCite \textit{I. Lynce} and \textit{J. Marques-Silva}, Discrete Appl. Math. 155, No. 12, 1604--1612 (2007; Zbl 1121.68109) Full Text: DOI Link
Kullmann, Oliver; Lynce, Inês; Marques-Silva, João Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. (English) Zbl 1187.68552 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 22-35 (2006). MSC: 68T20 PDFBibTeX XMLCite \textit{O. Kullmann} et al., Lect. Notes Comput. Sci. 4121, 22--35 (2006; Zbl 1187.68552) Full Text: DOI Link
Bhalla, Ateet; Lynce, Inês; de Sousa, José T.; Marques-Silva, João Heuristic-based backtracking relaxation for propositional satisfiability. (English) Zbl 1109.68099 J. Autom. Reasoning 35, No. 1-3, 3-24 (2005). MSC: 68T20 68P10 68W05 PDFBibTeX XMLCite \textit{A. Bhalla} et al., J. Autom. Reasoning 35, No. 1--3, 3--24 (2005; Zbl 1109.68099) Full Text: DOI Link
Mneimneh, Maher; Lynce, Inês; Andraus, Zaher; Marques-Silva, João; Sakallah, Karem A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. (English) Zbl 1128.68477 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 467-474 (2005). MSC: 68T20 90C57 90C59 PDFBibTeX XMLCite \textit{M. Mneimneh} et al., Lect. Notes Comput. Sci. 3569, 467--474 (2005; Zbl 1128.68477) Full Text: DOI
Manquinho, Vasco; Marques-Silva, João On applying cutting planes in DLL-based algorithms for pseudo-Boolean optimization. (English) Zbl 1128.68474 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 451-458 (2005). MSC: 68T20 90C09 PDFBibTeX XMLCite \textit{V. Manquinho} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 3569, 451--458 (2005; Zbl 1128.68474) Full Text: DOI
Bhalla, A.; Lynce, I.; de Sousa, J. T.; Marques-Silva, J. Heuristic-based backtracking for propositional satisfiability. (English) Zbl 1205.68370 Moura Pires, Fernando (ed.) et al., Progress in artificial intelligence. 11th Portuguese conference on artificial intelligence, EPIA 2003, Beja, Portugal, December 4–7, 2003. Proceedings. Berlin: Springer (ISBN 3-540-20589-6/pbk). Lect. Notes Comput. Sci. 2902, 116-130 (2003). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Bhalla} et al., Lect. Notes Comput. Sci. 2902, 116--130 (2003; Zbl 1205.68370) Full Text: DOI
Lynce, Inês; Marques-Silva, João The effect of nogood recording in DPLL-CBJ SAT algorithms. (English) Zbl 1023.68669 O’Sullivan, Barry (ed.), Recent advances in constraints. Joint ERCIM/CologNet international workshop on constraint solving and constraint logic programming, Cork, Ireland, June 19-21, 2002. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 2627, 144-158 (2003). MSC: 68T20 PDFBibTeX XMLCite \textit{I. Lynce} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 2627, 144--158 (2003; Zbl 1023.68669) Full Text: Link
Lynce, Ines; Baptista, Luís; Marques-Silva, João Towards provably complete stochastic search algorithms for satisfiability. (English) Zbl 1053.68684 Brazdil, Pavel (ed.) et al., Progress in artificial intelligence. Knowledge extraction, multi-agent systems, logic programming, and constraint solving. 10th Portuguese conference, EPIA 2001, Porto, Portugal, December 17–20, 2001. Proceedings. Berlin: Springer (ISBN 3-540-43030-X). Lect. Notes Comput. Sci. 2258, 363-370 (2001). MSC: 68T20 PDFBibTeX XMLCite \textit{I. Lynce} et al., Lect. Notes Comput. Sci. 2258, 363--370 (2001; Zbl 1053.68684) Full Text: Link
Lynce, Inês; Marques-Silva, João Improving SAT algorithms by using search pruning techniques. (English) Zbl 1067.68650 Walsh, Toby (ed.), Principles and practice of constraint programming - CP 2001. 7th international conference, Paphos, Cyprus, November 26 – December 1, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42863-1). Lect. Notes Comput. Sci. 2239, 770 (2001). MSC: 68T20 PDFBibTeX XMLCite \textit{I. Lynce} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 2239, 770 (2001; Zbl 1067.68650) Full Text: Link
Marques-Silva, João Algebraic simplification techniques for propositional satisfiability. (English) Zbl 1044.68781 Dechter, Rina (ed.), Principles and practice of constraint programming - CP 2000. 6th international conference, Singapore, September 18–21, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41053-8). Lect. Notes Comput. Sci. 1894, 537-542 (2000). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 1894, 537--542 (2000; Zbl 1044.68781) Full Text: Link
Baptista, Luís; Marques-Silva, João Using randomization and learning to solve hard real-world instances of satisfiability. (English) Zbl 1044.68736 Dechter, Rina (ed.), Principles and practice of constraint programming - CP 2000. 6th international conference, Singapore, September 18–21, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41053-8). Lect. Notes Comput. Sci. 1894, 489-494 (2000). MSC: 68T20 68T05 68T27 PDFBibTeX XMLCite \textit{L. Baptista} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 1894, 489--494 (2000; Zbl 1044.68736) Full Text: Link
Marques-Silva, João P.; Sakallah, Karem A. GRASP: a search algorithm for propositional satisfiability. (English) Zbl 1392.68388 IEEE Trans. Comput. 48, No. 5, 506-521 (1999). MSC: 68T20 68T15 90C08 PDFBibTeX XMLCite \textit{J. P. Marques-Silva} and \textit{K. A. Sakallah}, IEEE Trans. Comput. 48, No. 5, 506--521 (1999; Zbl 1392.68388) Full Text: DOI Link