Publications


2016


Automatic Generation of Propagation Complete SAT Encodings
Martin Brain, Liana Hadarean, Daniel Kroening, Ruben Martins,
Verification, Model Checking, and Abstract Interpretation (VMCAI'16), LNCS, 2016.


2015


On Using Incremental Encodings in Unsatisfiability-based MaxSAT Solving
Ruben Martins, Saurabh Joshi, Vasco Manquinho, Inês Lynce,
Journal on Satisfiability, Boolean Modeling and Computation (JSAT'15), 2015.

Generalized Totalizer Encoding for Pseudo-Boolean Constraints
Saurabh Joshi, Ruben Martins, Vasco Manquinho,
International Conference on Principles and Practice of Constraint Programming (CP'15), LNCS, 2015.

Exploiting Resolution-Based Representations for MaxSAT Solving
Miguel Neves, Ruben Martins, Mikoláš Janota, Inês Lynce, Vasco Manquinho,
International Conference on Theory and Applications of Satisfiability Testing (SAT'15), LNCS, 2015.

From AgentSpeak to C for Safety Considerations in Unmanned Aerial Vehicles
Samuel Bucheli, Daniel Kroening, Ruben Martins, Ashutosh Natraj,
Towards Autonomous Robotic Systems (TAROS'15), LNCS, 2015.

Successful Use of Incremental BMC in the Automotive Industry [pdf] [bib]
Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, Tom Bienmuller
Formal Methods for Industrial Critical Systems (FMICS'15), LNCS, 2015.

Deterministic Parallel MaxSAT Solving [doi] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
International Journal on Artificial Intelligence Tools (IJAIT'15), World Scientific, 2015.

Improving Linear Search Algorithms with Model-based Approaches for MaxSAT Solving [doi] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
Journal of Experimental & Theoretical Artificial Intelligence (JETAI'15), Taylor and Francis, 2015.

2014


Incremental Cardinality Constraints for MaxSAT [pdf] [bib]
Ruben Martins, Saurabh Joshi, Vasco Manquinho, Inês Lynce,
International Conference on Principles and Practice of Constraint Programming (CP'14), LNCS, 2014.

Open-WBO: a Modular MaxSAT Solver [pdf] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
International Conference on Theory and Applications of Satisfiability Testing (SAT'14), LNCS, 2014.

2013


Community-based Partitioning for MaxSAT Solving [doi] [pdf] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
International Conference on Theory and Applications of Satisfiability Testing (SAT'13), LNCS, 2013.

Model-based Partitioning for MaxSAT Solving [pdf] [bib] [benchmarks]
Ruben Martins, Vasco Manquinho, Inês Lynce,
RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA'13), 2013.

2012


Satisfação e Optimização Booleanas: Jogos, Puzzles e Genética [pdf] [bib]
Ruben Martins, Ana Graça
Números, Cirugias e Nós de Gravata, 252-270, IST Press, 2012.

Parallel Search for Maximum Satisfiability [doi] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
AI Communications 25(2): 75-95, IOS Press, 2012.

An Overview of Parallel SAT Solving [doi] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
Constraints 17(3): 304-347, Springer, 2012 .

On Partitioning for Maximum Satisfiability [doi] [pdf] [poster] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
European Conference on Artificial Intelligence (ECAI'12), Short Paper, IOS Press, 2012.

Clause Sharing in Parallel MaxSAT [doi] [pdf] [slides] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
Learning and Intelligent Optimization Conference (LION'12), Short Paper, LNCS, 2012.

Clause Sharing in Deterministic Parallel Maximum Satisfiability [pdf] [slides] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA'12), 2012.

2011


Exploiting Cardinality Encodings in Parallel Maximum Satisfiability [doi] [pdf] [slides] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce,
International Conference on Tools with Artificial Intelligence (ICTAI'11), IEEE, 2011.

Parallel Search for Boolean Optimization [pdf] [slides] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce
RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA'11), 2011.


2010


Improving Search Space Splitting for Parallel SAT Solving [doi] [pdf] [slides] [bib]
Ruben Martins, Vasco Manquinho, Inês Lynce
International Conference on Tools with Artificial Intelligence (ICTAI'10), IEEE, 2010.

Improving Unsatisfiability-based Algorithms for Boolean Optimization [doi] [pdf] [slides] [bib]
Vasco Manquinho, Ruben Martins, Inês Lynce

International Conference on Theory and Applications of Satisfiability Testing (SAT'10), LNCS, 2010.

2009


Preprocessing in Pseudo-Boolean Optimization: An Experimental Evaluation [pdf] [slides] [bib]
Ruben Martins, Inês Lynce, Vasco Manquinho
International Workshop on Constraint Modelling and Reformulation (ModRef'09), 2009.

2008


Effective CNF Encodings of the Towers of Hanoi [pdf] [slides] [bib]
Ruben Martins, Inês Lynce
International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'08), Short Paper, 2008.

Effective CNF Encodings of the Towers of Hanoi [pdf] [bib]
Ruben Martins, Inês Lynce
Technical Report: 47, INESC-ID, 2008.

2007


Breaking Local Symmetries in Quasigroup Completion Problems [pdf] [slides] [bib]
Ruben Martins, Inês Lynce
RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA'07), 2007.