In this paper, we revisit the state-of-the-art of MaxSAT solving. We focus on SAT-based MaxSAT solving algorithms, mainly on Core-guided MaxSAT solvers. We show how to describe Core-guided solvers with Non-CNF MaxSAT rules plus the Extension rule. Equipped with these rules, we show how to apply them alternatively to obtain new Core-guided MaxSAT solvers. Since Core-guided solvers essentially solve a sequence of SAT instances, we also discuss how Core-guided MaxSAT solvers traverse the search space of possible sequences of SAT instances, the existence of exponentially harder sequences, and how to avoid them. The experimental investigation shows comparable and complementary performance to state-of-the-art solvers.

In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach.

Covering arrays have become a key piece in Combinatorial Testing. In particular, we focus on the efficient construction of Covering Arrays with Constraints of high strength. SAT solving technology has been proven to be well suited when solving Covering Arrays with Constraints. However, the size of the SAT reformulations rapidly grows up with higher strengths. To this end, we present a new incomplete algorithm that mitigates substantially memory blow-ups. The experimental results confirm the goodness of the approach, opening avenues for new practical applications.

In the literature, we find reductions from 3SAT to Max2SAT. These reductions are based on the usage of a gadget, i.e., a combinatorial structure that allows translating constraints of one problem to constraints of another. Unfortunately, the generation of these gadgets lacks an intuitive or efficient method. In this paper, we provide an efficient and constructive method for Reducing SAT to Max2SAT and show empirical results of how MaxSAT solvers are more efficient than SAT solvers solving the translation of hard formulas for Resolution.

Modern SAT solvers have experienced a remarkable progress on solving industrial instances. It is believed that most of these successful techniques exploit the underlying structure of industrial instances. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. Representing SAT instances as graphs, we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver, and observe that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. Motivated by this observation, we finally present an application that exploits the community structure to detect relevant learned clauses, and we show that detecting these clauses results in an improvement on the performance of the SAT solver. Empirically, we observe that this improves the performance of several SAT solvers on industrial SAT formulas, especially on satisfiable instances.

Norms constitute regulative mechanisms extensively enacted in groups, organisations, and societies. However, 'choosing the right norms to establish' constitutes an open problem that requires the consideration of a number of constraints (such as norm relations) and preference criteria (e.g over involved moral values). This paper advances the state of the art in the Normative Multiagent Systems literature by formally defining this problem and by proposing its encoding as a linear program so that it can be automatically solved.

Metaheuristics have been developed to provide general purpose approaches for solving hard combinatorial problems. While these frameworks often serve as the starting point for the development of problem-specific search procedures, they very rarely work efficiently in their default state. We combine the ideas of reactive search, which adjusts key parameters during search, and algorithm configuration, which fine-tunes algorithm parameters for a given set of problem instances, for the automatic compilation of a portfolio of highly reactive dialectic search heuristics for MaxSAT. Even though the dialectic search metaheuristic knows nothing more about MaxSAT than how to evaluate the cost of a truth assignment, our automatically generated solver defines a new state of the art for random weighted partial MaxSAT instances. Moreover, when combined with an industrial MaxSAT solver, the self-assembled reactive portfolio was able to win four out of nine gold medals at the recent 2016 MaxSAT Evaluation on random, crafted, and industrial partial and weighted-partial MaxSAT instances.

Our objective is to boost the state-of-the-art performance in MaxSATsolving. To this end, we employ the instance-specific algorithmconfigurator ISAC, and improve it with the latest inportfolio technology. Experimental results on SAT show that thiscombination marks a significant step forward in our ability to tunealgorithms instance-specifically. We then apply the new methodology toa number of MaxSAT problem domains and show that the resulting solversconsistently outperform the best existing solvers on the respectiveproblem families. In fact, the solvers presented here were independentlyevaluated at the 2013 MaxSAT Evaluation where they won six of the elevencategories.

We present and implement a Weighted Partial MaxSAT solver based on successive calls to a SAT solver. We prove the correctness of our algorithm and compare our solver with other Weighted Partial MaxSAT solvers.

This paper introduces new solving strategies for the resolution of Pseudo-Boolean Modularity (PBMod) constraints. In particular, we deal with modular arithmetic constraints on Boolean variables. On the one hand, we analyze translations to Pseudo-Boolean (PB) constraints and apply PB solvers. We also look at those PB solvers that have shown that a transformation to the SAT problem can be an effective solving strategy for PB problems. Among the existing translation techniques we focus on the encoding based on a network of sorters. We extend this encoding technique to generate directly a SAT formula from the PBMod constraints. We compare our approach to other standard techniques such as Satisfiability Modulo Theories (SMT) solvers with support for the Quantifier Free Linear Integer Arithmetic (QF_LIA) theory and the GLPK package for Mixed Integer Programming. In order to conduct our experimental investigation we present a generator of random PBMod constraints and study the impact of the several parameters on the hardness of the instances.