Iterative and core-guided MaxSAT solving: A survey and assessment

Maximum Satisfiability (MaxSAT) is an optimization version of SAT, and many real world applications can be naturally encoded as such. Solving MaxSAT is an important problem from both a theoretical and a practical point of view. In recent years, there has been considerable interest in developing efficient algorithms and several families of algorithms have been proposed. This paper overviews recent approaches to handle MaxSAT and presents a survey of MaxSAT algorithms based on iteratively calling a SAT solver which are particularly effective to solve problems arising in industrial settings. First, classic algorithms based on iteratively calling a SAT solver and updating a bound are overviewed. Such algorithms are referred to as iterative MaxSAT algorithms. Then, more sophisticated algorithms that additionally take advantage of unsatisfiable cores are described, which are referred to as core-guided MaxSAT algorithms. Core-guided MaxSAT algorithms use the information provided by unsatisfiable cores to relax clauses on demand and to create simpler constraints. Finally, a comprehensive empirical study on non-random benchmarks is conducted, including not only the surveyed algorithms, but also other state-of-the-art MaxSAT solvers. The results indicate that (i) core-guided MaxSAT algorithms in general abort in less instances than classic solvers based on iteratively calling a SAT solver and that (ii) core-guided MaxSAT algorithms are fairly competitive compared to other approaches.     

Boolean lexicographic optimization: algorithms & applications

Multi-Objective Combinatorial Optimization (MOCO) problems find a wide range of practical application problems, some of which involving Boolean variables and constraints. This paper develops and evaluates algorithms for solving MOCO problems, defined on Boolean domains, and where the optimality criterion is lexicographic. The proposed algorithms build on existing algorithms for either Maximum Satisfiability (MaxSAT), Pseudo-Boolean Optimization (PBO), or Integer Linear Programming (ILP). Experimental results, obtained on problem instances from haplotyping with pedigrees and software package dependencies, show that the proposed algorithms can provide significant performance gains over state of the art MaxSAT, PBO and ILP algorithms. Finally, the paper also shows that lexicographic optimization conditions are observed in the majority of the problem instances from the MaxSAT evaluations, motivating the development of dedicated algorithms that can exploit lexicographic optimization conditions in general MaxSAT problem instances.     

Algorithm portfolios for noisy optimization

Noisy optimization is the optimization of objective functions corrupted by noise. A portfolio of solvers is a set of solvers equipped with an algorithm selection tool for distributing the computational power among them. Portfolios are widely and successfully used in combinatorial optimization. In this work, we study portfolios of noisy optimization solvers. We obtain mathematically proved performance (in the sense that the portfolio performs nearly as well as the best of its solvers) by an ad hoc portfolio algorithm dedicated to noisy optimization. A somehow surprising result is that it is better to compare solvers with some lag, i.e., propose the current recommendation of best solver based on their performance earlier in the run. An additional finding is a principled method for distributing the computational power among solvers in the portfolio.     

On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes

We analyze and compare two solvers for Boolean optimization problems: WMaxSatz, a solver for Partial MaxSAT, and MinSatz, a solver for Partial MinSAT. Both MaxSAT and MinSAT are similar, but previous results indicate that when solving optimization problems using both solvers, the performance is quite different on some cases. For getting insights about the differences in the performance of the two solvers, we analyze their behaviour when solving 2SAT-MaxOnes problem instances, given that 2SAT-MaxOnes is probably the most simple, but NP-hard, optimization problem we can solve with them. The analysis is based first on the study of the bounds computed by both algorithms on some particular 2SAT-MaxOnes instances, characterized by the presence of certain particular structures. We find that the fraction of positive literals in the clauses is an important factor regarding the quality of the bounds computed by the algorithms. Then, we also study the importance of this factor on the typical case complexity of Random-p 2SAT-MaxOnes, a variant of the problem where instances are randomly generated with a probability p of having positive literals in the clauses. For the case p=0, the performance results indicate a clear advantage of MinSatz with respect to WMaxSatz, but as we consider positive values of p WMaxSatz starts to show a better performance, although at the same time the typical complexity of Random-p 2SAT-MaxOnes decreases as p increases. We also study the typical value of the bound computed by the two algorithms on these sets of instances, showing that the behaviour is consistent with our analysis of the bounds computed on the particular instances we studied first.     

Infra-chromatic bound for exact maximum clique search

Many efficient exact branch and bound maximum clique solvers use approximate coloring to compute an upper bound on the clique number for every subproblem. This technique reasonably promises tight bounds on average, but never tighter than the chromatic number of the graph.Li and Quan, 2010, AAAI Conference, p. 128–133 describe a way to compute even tighter bounds by reducing each colored subproblem to maximum satisfiability problem (MaxSAT). Moreover they show empirically that the new bounds obtained may be lower than the chromatic number.Based on this idea this paper shows an efficient way to compute related “infra-chromatic” upper bounds without an explicit MaxSAT encoding. The reported results show some of the best times for a stand-alone computer over a number of instances from standard benchmarks.     

基于不可满足原因的最小纠正集求解

布尔公式的最小纠正集MCS是子句的集合。对于一个不可满足公式,移除MCS后,所得到的新公式可满足。任一MCS中的子句保留在公式中,所得到的新公式不可满足。通过求解MCS 并调整约束集合,能够求解最小不可满足核心、MaxSAT 问题和最大（小）可满足解问题;还能够应用于故障定位、模型检查配置优化等实际问题中。 提出了一种基于不可满足原因的MCS求解算法,实现了相应的CUC工具。通过与目前最好的MCS求解工具LBX进行比较,得到了CUC性能优于LBX的结论。CUC比LBX平均多解出5%（65个）的公式。对于CUC和LBX均可解出的公式,CUC的平均求解时间比LBX快2.5倍。     

Intelligent forecasting models-selection system for the portfolio internal structure change

In this study, an intelligent forecasting models-selection system for refining portfolio structural estimation is proposed selecting different forecasts time series models, as well as the contents’ trend with refining the risk-return matrices of components. Based on the four inference rules in intelligent selection mechanism, the support system seeks to find the appropriate model solutions satisfying the tracking for the behavior of indices prices in portfolio optimization. The feasibility of the system is verified with a practical simulation experiment. The experimental results show that, for all examined investment assets, the presented system is an efficient way of solving the portfolio internal structure change problem. In addition, we also find that the presented system can also be used as an alternative method for evaluating various forecasting models. By means of global major market as the empirical evidences of portfolio contents, it will show that the proposed system can serve as improving efficient frontier of a portfolio.     

Resolution-based lower bounds in MaxSAT

The lower bound (LB) implemented in branch and bound MaxSAT solvers is decisive for obtaining a competitive solver. In modern solvers like MaxSatz and MiniMaxSat, the LB relies on the cooperation of the underestimation and inference components. Actually, the underestimation component of some solvers guides the application of the inference component when a conflict is reached and certain structures are found. In this paper we analyze algorithmic and logical aspects of the underestimation components that have been implemented in MaxSatz during its evolution. From an algorithmic point of view, we define novel strategies for selecting unit clauses in UP (the underestimation of LB in UP is the number of independent inconsistent subformulas detected using unit propagation), the extension of UP with failed literal detection, and a clever heuristic for guiding the application of MaxSAT resolution when UP augmented with failed literal detection is applied in the presence of cycles structures. From a logical point of view, we prove that the inconsistent subformulas detected by UP are minimally unsatisfiable, but this property does not hold if failed literal detection is added. In the presence of cycle structures in conflicts detected by UP augmented with failed literal detection, we prove that the application of MaxSAT resolution produces smaller inconsistent subformulas and, besides, generates additional clauses that may be used to improve the LB. The conducted empirical investigation indicates that the LB techniques described in this paper lead to better quality LBs.     

Weighted heuristic anytime search: new schemes for optimization over graphical models

Weighted heuristic search (best-first or depth-first) refers to search with a heuristic function multiplied by a constant w [31]. The paper shows, for the first time, that for optimization queries in graphical models the weighted heuristic best-first and weighted heuristic depth-first branch and bound search schemes are competitive energy-minimization anytime optimization algorithms. Weighted heuristic best-first schemes were investigated for path-finding tasks. However, their potential for graphical models was ignored, possibly because of their memory costs and because the alternative depth-first branch and bound seemed very appropriate for bounded depth. The weighted heuristic depth-first search has not been studied for graphical models. We report on a significant empirical evaluation, demonstrating the potential of both weighted heuristic best-first search and weighted heuristic depth-first branch and bound algorithms as approximation anytime schemes (that have sub-optimality bounds) and compare against one of the best depth-first branch and bound solvers to date.     

Strategic Particle Swarm Inertia Selection for Electricity Markets Participation Portfolio Optimization

ABSTRACT

The portfolio optimization is a well-known problem in the areas of economy and finance. This problem has also become increasingly important in electrical power systems, particularly in the area of electricity markets, mostly due to the growing number of alternative/complementary market types that are being introduced to deal with important issues, such as the massive integration of renewable energy sources in power systems. The optimization of electricity market players’ participation portfolio comprises significant time constraints, which cannot be satisfied by the use of deterministic techniques. For this reason, meta-heuristic solutions are used, such as particle swarm optimization. The inertia is one of the most important parameter in this method, and it is the main focus of this paper. This paper studies 18 popular inertia calculation strategies, by comparing their performance in the portfolio optimization problem. A strategic methodology for the automatic selection of the best inertia calculation method for the needs of each optimization is also proposed. Results show that the proposed approach is able to automatically adapt the inertia parameter according to the needs in each execution.     

Computing all roots of the likelihood equations of seemingly unrelated regressions

Seemingly unrelated regressions are statistical regression models based on the Gaussian distribution. They are popular in econometrics but also arise in graphical modeling of multivariate dependencies. In maximum likelihood estimation, the parameters of the model are estimated by maximizing the likelihood function, which maps the parameters to the likelihood of observing the given data. By transforming this optimization problem into a polynomial optimization problem, it was recently shown that the likelihood function of a simple bivariate seemingly unrelated regressions model may have several stationary points. Thus local maxima may complicate maximum likelihood estimation. In this paper, we study several more complicated seemingly unrelated regression models, and show how all stationary points of the likelihood function can be computed using algebraic geometry.     

Accelerating iterative linear solvers using multiple graphical processing units

In this paper, we develop, study and implement iterative linear solvers and preconditioners using multiple graphical processing units (GPUs). Techniques for accelerating sparse matrix–vector (SpMV) multiplication, linear solvers and preconditioners are presented. Four Krylov subspace solvers, a Neumann polynomial preconditioner and a domain decomposition preconditioner are implemented. Our numerical tests with NVIDIA C2050 GPUs show that the SpMV kernel can be sped over 40 times faster using four GPUs. Our linear solvers and preconditioners have similar speedup.     

Triangle-based consistencies for cost function networks

Cost Function Networks (aka Weighted CSP) allow to model a variety of problems, such as optimization of deterministic and stochastic graphical models including Markov random Fields and Bayesian Networks. Solving cost function networks is thus an important problem for deterministic and probabilistic reasoning. This paper focuses on local consistencies which define essential tools to simplify Cost Function Networks, and provide lower bounds on their optimal solution cost. To strengthen arc consistency bounds, we follow the idea of triangle-based domain consistencies for hard constraint networks (path inverse consistency, restricted or max-restricted path consistencies), describe their systematic extension to cost function networks, study their relative strengths, define enforcing algorithms, and experiment with them on a large set of benchmark problems. On some of these problems, our improved lower bounds seem necessary to solve them.     

Multi-period portfolio optimization with linear control policies

This paper is concerned with multi-period sequential decision problems for financial asset allocation. A model is proposed in which periodic optimal portfolio adjustments are determined with the objective of minimizing a cumulative risk measure over the investment horizon, while satisfying portfolio diversity constraints at each period and achieving or exceeding a desired terminal expected wealth target. The proposed solution approach is based on a specific affine parameterization of the recourse policy, which allows us to obtain a sub-optimal but exact and explicit problem formulation in terms of a convex quadratic program.In contrast to the mainstream stochastic programming approach to multi-period optimization, which has the drawback of being computationally intractable, the proposed setup leads to optimization problems that can be solved efficiently with currently available convex quadratic programming solvers, enabling the user to effectively attack multi-stage decision problems with many securities and periods.     

Robust optimal decisions with imprecise forecasts

A robust minimax approach for optimal investment decisions with imprecise return forecasts and risk estimations in financial portfolio management is considered. Single-period and multi-period mean-variance optimization models are extended to worst-case design with multiple rival risk estimations and return forecasts. In multi-period stochastic formulation of classical mean-variance portfolio optimization problem, an investor makes an investment decision based on expectations and/or scenarios up to some intermediate times prior to the horizon and, consequently, rebalances or restructures the portfolio. Multi-period portfolio optimization entails the construction of a scenario tree representing a discretized estimate of uncertainties and associated probabilities in future stages. It is well known that return forecasts and risk estimations are inherently inaccurate and there are different rival estimates, or scenario trees. Robust optimization models are presented and imprecise nature of moment forecasts to reduce the risk of making a decision based on the wrong scenario is addressed. The worst-case performance is guaranteed in view of all rival risk and return scenarios and will only improve when any scenario other than the worst-case is realized. The ex-ante performance of minimax models is tested using historical data and backtesting results are presented.     

Asset portfolio optimization using fuzzy mathematical programming

By morphing mean-variance optimization (MVO) portfolio model into semi-absolute deviation (SAD) model, we apply multi criteria decision making (MCDM) via fuzzy mathematical programming to develop comprehensive models of asset portfolio optimization (APO) for the investors’ pursuing either of the aggressive or conservative strategies.     

Monte Carlo linear solvers with non-diagonal splitting

Monte Carlo (MC) linear solvers can be considered stochastic realizations of deterministic stationary iterative processes. That is, they estimate the result of a stationary iterative technique for solving linear systems. There are typically two sources of errors: (i) those from the underlying deterministic iterative process and (ii) those from the MC process that performs the estimation. Much progress has been made in reducing the stochastic errors of the MC process. However, MC linear solvers suffer from the drawback that, due to efficiency considerations, they are usually stochastic realizations of the Jacobi method (a diagonal splitting), which has poor convergence properties. This has limited the application of MC linear solvers. The main goal of this paper is to show that efficient MC implementations of non-diagonal splittings too are feasible, by constructing efficient implementations for one such splitting. As a secondary objective, we also derive conditions under which this scheme can perform better than MC Jacobi, and demonstrate this experimentally. The significance of this work lies in proposing an approach that can lead to efficient MC implementations of a wider variety of deterministic iterative processes.     

Topology optimization of continuum structures under hybrid uncertainties

The aim of this paper is to study the topology optimization for mechanical systems with hybrid material and geometric uncertainties. The random variations are modeled by a memory-less transformation of random fields which ensures their physical admissibility. The stochastic collocation method combined with the proposed material and geometry uncertainty models provides robust designs by utilizing already developed deterministic solvers. The computational cost is decreased by using of sparse grids and discretization refinement that are proposed and demonstrated as well. The method is utilized in the design of minimum compliance structure. The proposed algorithm provides a computationally cheap alternative to previously introduced stochastic optimization methods based on Monte Carlo sampling by using adaptive sparse grids method.     

Empirical hardness of finding optimal Bayesian network structures: algorithm selection and runtime prediction

Various algorithms have been proposed for finding a Bayesian network structure that is guaranteed to maximize a given scoring function. Implementations of state-of-the-art algorithms, solvers, for this Bayesian network structure learning problem rely on adaptive search strategies, such as branch-and-bound and integer linear programming techniques. Thus, the time requirements of the solvers are not well characterized by simple functions of the instance size. Furthermore, no single solver dominates the others in speed. Given a problem instance, it is thus a priori unclear which solver will perform best and how fast it will solve the instance. We show that for a given solver the hardness of a problem instance can be efficiently predicted based on a collection of non-trivial features which go beyond the basic parameters of instance size. Specifically, we train and test statistical models on empirical data, based on the largest evaluation of state-of-the-art exact solvers to date. We demonstrate that we can predict the runtimes to a reasonable degree of accuracy. These predictions enable effective selection of solvers that perform well in terms of runtimes on a particular instance. Thus, this work contributes a highly efficient portfolio solver that makes use of several individual solvers.     

Reformulation based MaxSAT robustness

The presence of uncertainty in the real world makes robustness a desirable property of solutions to constraint satisfaction problems (CSP). A solution is said to be robust if it can be easily repaired when unexpected events happen. This issue has already been addressed in the frameworks of Boolean satisfiability (SAT) and Constraint Programming (CP). Most existing works on robustness implement search algorithms to look for robust solutions instead of taking the declarative approach of reformulation, since reformulation tends to generate prohibitively large formulas, especially in the CP setting. In this paper we consider the unaddressed problem of robustness in weighted MaxSAT, by showing how robust solutions to weighted MaxSAT instances can be effectively obtained via reformulation into pseudo-Boolean formulae. Our encoding provides a reasonable balance between increase in size and performance, as shown by our experiments in the robust resource allocation framework. We also address the problem of flexible robustness, where some of the breakages may be left unrepaired if a totally robust solution does not exist. In a sense, since the use of SAT and MaxSAT encodings for solving CSP has been gaining wide acceptance in recent years, we provide an easy-to-implement new method for achieving robustness in combinatorial optimization problems.