Research

Main  |  Teaching  |  Contact


Publications

Here you can find my publications. You can also check my profile at Google Scholar, Research Gate, Microsoft Academic Search and Researcher ID.

Book Chapters

  • O. Roussel, V. Manquinho, Pseudo-Boolean and Cardinality Constraints, in Handbook of Satisfiability, February 2009.

  • I. Lynce, V. Manquinho, J. Marques-Silva, Backtracking, Encyclopedia of Computer Science and Engineering, vol. 1, pp. 283-289, Wiley, January 2009.

Journals

  • R. Martins, S. Joshi, V. Manquinho, I. Lynce: On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving, Journal on Satisfiability, Boolean Modeling and Computation, accepted for publication

  • R. Martins, V. Manquinho, I. Lynce: Improving linear search algorithms with model-based approaches for MaxSAT solving, Journal of Experimental & Theoretical Artificial Intelligence, accepted for publication

  • R. Martins, V. Manquinho, I. Lynce: Deterministic Parallel MaxSAT Solving. International Journal on Artificial Intelligence Tools 24(3), 2015

  • M. Miranda, I. Lynce, V. Manquinho: Inferring phylogenetic trees using pseudo-Boolean optimization. AI Communications 27(3): 229-243, 2014

  • R. Martins, V. Manquinho, I. Lynce: Parallel search for maximum satisfiability. AI Communications 25(2): 75-95, 2012

  • R. Martins, V. Manquinho, I. Lynce: An overview of parallel SAT solving. Constraints 17(3): 304-347, 2012

  • M. Janota, I. Lynce, V. Manquinho, J. Marques-Silva: PackUp: Tools for Package Upgradability Solving. JSAT 8(1/2): 89-94, 2012

  • J. Delgado, I. Lynce, V. Manquinho, Computing the Summed Adjacency Disruption Number between Two Genomes with Duplicate Genes, in Journal of Computational Biology, 17(9): 1243-1265, September 2010

  • Wei-Chung Kao, Wei-Shun Chuang, Hsiu-Ting Lin, James C.-M. Li, V. Manquinho, DFT and Minimum Leakage Pattern Generation for Static Power Reduction During Test and Burn-in, in IEEE Transactions on VLSI Systems, vol. 18(3), pp. 392-400, 2010

  • V. Manquinho, J. Marques-Silva, On Using Cutting Planes in Pseudo-Boolean Optimization, in Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, pp. 209-219, research note, 2006.

  • V. Manquinho, O. Roussel, The First Evaluation of Pseudo-Boolean Solvers (PB'05), in Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, pp. 103-143, 2006.

  • V. Manquinho, J. Marques-Silva, Satisfiability-based Algorithms for Boolean Optimization,, in Annals of Mathematics and Artificial Intelligence, vol. 40, n. 3-4, pp. 353-372, 2004.

  • V. Manquinho, J. Marques-Silva, Search Pruning Techniques in SAT-based Branch-and-Bound Algorithms for the Binate Covering Problem,, in IEEE Transactions on Computer Aidded Design (TCAD), vol. 31, n. 5, pp. 505-516, May 2002.

Conferences

  • S. Joshi, R. Martins, V. Manquinho: Generalized Totalizer Encoding for Pseudo-Boolean Constraints. CP: 200-209, 2015

  • M. Neves, R. Martins, M. Janota, I. Lynce, V. Manquinho: Exploiting Resolution-Based Representations for MaxSAT Solving. SAT: 272-286, 2015

  • R. Martins, S. Joshi, V. Manquinho, I. Lynce: Incremental Cardinality Constraints for MaxSAT. CP: 531-548, 2014

  • A. Ignatiev, A. Morgado, V. Manquinho, I. Lynce, J. Marques-Silva: Progression in Maximum Satisfiability. ECAI: 453-458, 2014

  • J. Marques-Silva, A. Ignatiev, A. Morgado, V. Manquinho, I. Lynce: Efficient Autarkies. ECAI: 603-608, 2014

  • R. Martins, V. Manquinho, I. Lynce: Open-WBO: A Modular MaxSAT Solver. SAT: 438-445, 2014

  • R. Martins, V. Manquinho, I. Lynce: Community-Based Partitioning for MaxSAT Solving. SAT: 182-191, 2013

  • R. Martins, V. Manquinho, I. Lynce: On Partitioning for Maximum Satisfiability. ECAI: 913-914, 2012

  • R. Martins, V. Manquinho, I. Lynce: Clause Sharing in Parallel MaxSAT. LION: 455-460, 2012

  • R. Martins, V. Manquinho, I. Lynce: Exploiting Cardinality Encodings in Parallel Maximum Satisfiability. ICTAI: 313-320, 2011

  • R. Martins, V. Manquinho, I. Lynce: Improving Search Space Splitting for Parallel SAT Solving. ICTAI: 336-343, 2010

  • V. Manquinho, R. Martins, I. Lynce, Improving Unsatisfiability-based Algorithms for Boolean Optimization, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2010.

  • J. Delgado, I. Lynce, V. Manquinho, Computing the Summed Adjacency Disruption Number between Two Genomes with Duplicate Genes using Pseudo-Boolean Optimization, in Proceedings of the Seventh Annual RECOMB Satellite Workshop on Comparative Genomics (RECOMB-CG), September 2009.

  • V. Manquinho, J. Marques-Silva, J. Planes, Algorithms for Weighted Boolean Optimization, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), June 2009.

  • J. Marques-Silva, I. Lynce, V. Manquinho, Symmetry Breaking for MaxSAT, in Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), November 2008.

  • J. Marques-Silva, V. Manquinho, Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), May 2008.

  • F. Heras, V. Manquinho, J. Marques-Silva, On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization, in Proceedings of the AAAI Conference of the Florida Artificial Intelligence Research Society (FLAIRS), May 2008.

  • A. Morgado, P. Matos, V. Manquinho, J. Marques-Silva, Counting Models in Integer Domains, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), August 2006.

  • V. Manquinho, J. Marques-Silva, Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts,in Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI), November 2005.

  • V. Manquinho, J. Marques-Silva, On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), June 2005.

  • V. Manquinho, J. Marques-Silva, Effective Lower Bounding Techniques for Pseudo-Boolean Optimization, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 2005.

  • V. Manquinho, J. Marques-Silva, Integration of Lower Bound Estimates in Pseudo-Boolean Optimization, in Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI), November 2004.

  • V. Manquinho, J. Marques-Silva, Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization,, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), May 2004.

  • V. Manquinho, J. Marques-Silva, Search Pruning Conditions for Boolean Optimization , in Proceedings of the 14th European Conference on Artificial Intelligence (ECAI), August 2000.

  • V. Manquinho, J. Marques-Silva, On Using Satisfiability-Based Pruning Techniques in Covering Algorithms, in Proceedings of the IEEE/ACM Design, Automation and Test in Europe Conference (DATE), March 2000.

  • V. Manquinho, J. Marques-Silva, On Solving Boolean Optimization with Satisfiability-Based Algorithms , in Sixth International Symposium on Artificial Intelligence and Mathematics, January 2000.

  • V. Manquinho, Paulo Flores, J. Marques-Silva, A. Oliveira, Prime Implicant Computation Using Satisfiability Algorithms, in Proceedings of the IEEE International Conference on Tools with Artificial Intelligence (ICTAI), November 1997.

Workshops with peer review

Software

WBO Solver

An Unsatisfiability-based solver for Weighted Boolean Optimization. It can also solve Pseudo-Boolean Solving (PBS) and Optimization (PBO) problem instances, as well as Maximum Satisfiability (MaxSAT) instances or any of its partial and weighted variants. Current version of the solver allows for different search strategies. Please visit the wbo homepage for details on the tool and associated publications.

PWBO Solver

Multicore parallel generalization of the wbo solver. pwbo can run several strategies (portfolio or splitting on the optimization function value) for solving Boolean optimization problems (PBO, MaxSAT). One of the key features is that all threads collaborate by sharing information. Please visit the pwbo homepage for details on the tool and associated publications.

BSOLO Solver

Initially, BSOLO was designed to solve instances of the Unate and Binate Covering Problems (UCP/BCP). It has been updated to also deal with Pseudo-Boolean constraints. Although new developments on BSOLO have stopped, if you wish to try it, please send me an email.

Important note: The software packages are made available solely for research and educational purposes. If you wish to use it for other purposes, you must contacts the authors for permission.

For results of bsolo, wbo and pwbo on several types of instances, please check the results of the Pseudo-Boolean Solver Evaluation and MaxSAT Evaluation.


Last Modified: October 2015