Research

Main  |  Teaching  |  Contact

Publications

Book Chapters

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


• Inês Lynce, Vasco Manquinho and João Marques-Silva, Backtracking, Encyclopedia of Computer Science and Engineering, vol. 1, pp. 283-289, Wiley, January 2009.

Journals

• João Delgado, Inês Lynce and Vasco Manquinho, Computing the Summed Adjacency Disruption Number between Two Genomes with Duplicate Genes, in Journal of Computational Biology, In Press.


• Wei-Chung Kao, Wei-Shun Chuang, Hsiu-Ting Lin, James C.-M. Li and Vasco 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


• Vasco Manquinho and João 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.


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


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


• Vasco Manquinho and João 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

• Vasco Manquinho, Ruben Martins and Inês Lynce, Improving Unsatisfiability-based Algorithms for Boolean Optimization, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), July 2010.


• João Delgado, Inês Lynce, and Vasco 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.


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


• João Marques-Silva, Inês Lynce and Vasco Manquinho, Symmetry Breaking for MaxSAT, in Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), November 2008.


• João Marques-Silva and Vasco 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.


• Federico Heras, Vasco Manquinho and João 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.


• António Morgado, Paulo Matos, Vasco Manquinho and João Marques-Silva, Counting Models in Integer Domains, in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), August 2006.


• Vasco Manquinho and João 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.


• Vasco Manquinho and João 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.


• Vasco Manquinho and João 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.


• Vasco Manquinho and João 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.


• Vasco Manquinho and João 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.


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


• Vasco Manquinho and João 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.


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


• Vasco Manquinho, Paulo Flores, João Marques-Silva and Arlindo 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

• Ruben Martins, Inês Lynce, Vasco Manquinho, Preprocessing in Pseudo-Boolean Optimization: An Experimental Evaluation, in Eighth International Workshop on Constraint Modelling and Reformulation, September 2009.


• José Santos and Vasco Manquinho, Learning Techniques for Pseudo-Boolean Solving, in 7th International Workshop on Implementation of Logics, November 2008.


• Vasco Manquinho and João Marques-Silva, Lower Bounding Techniques for SAT-Based Boolean Optimization , in 3rd International Workshop on Integration of AI and OR Techniques (CP-AI-OR), April 2001.


• Vasco Manquinho and João Marques-Silva, Conditions for Non-Chronological Backtracking in Boolean Optimization , in AAAI Workshop on the Integration of AI and OR Techniques for Combinatorial Optimization, July 2000.


• Vasco Manquinho, Arlindo Oliveira and João Marques-Silva, Models and Algorithms for Computing Minimum-Size Prime Implicants, in International Workshop on Boolean Problems (IWBP), September 1998.


• Vasco Manquinho, João Marques-Silva, Arlindo Oliveira and Karem Sakallah, Satisfiability-Based Algorithms for 0-1 Integer Programming, in IEEE/ACM International Workshop on Logic Synthesis, June 1998.

Software

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.

WBO Solver

An Unsatisfiability-based solver for Weighted Boolean Optimization. It can also solve Pseudo-Boolean Solving and Optimization problem instances, as well as Maximum Satisfiability (MaxSAT) instances or any of its partial and weighted variants.

If you wish to try any of our solvers, 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 and wbo on several types of instances, please check the results of the last Pseudo-Boolean Solver Evaluation (PB'10) and MaxSAT Evaluation 2010.

Benchmarks and description of solver input files are also available at the PB'10 and MaxSAT Evaluation webpages