Papers

Ordered Multi-valued Decision Diagram (MDD) is a compact representation used to model various constraints, such as regular constraints and table constraints. It can be particularly useful for representing ad-hoc problem specific constraints. Many algorithms have been proposed to enforce Generalized Arc Consistency (GAC) on MDD constraints. In this paper, we introduce a new compact representation called Binary Constraint Tree (BCT). We propose tree binary encodings to transform any MDD constraint into a BCT constraint. We also present a specialized algorithm enforcing GAC on the BCT constraint resulting from a MDD constraint. Experimental results on a large set of benchmarks show that the BCT GAC algorithm can significantly outperform state-of-the-art MDD as well as table GAC algorithms.

poster session 2 @ blue 4, poster session 9 @ blue 4, poster session 2, poster session 9

The predict+optimize problem combines machine learning and combinatorial optimization by predicting the problem coefficients first and then using these coefficients to solve the optimization problem. While this problem can be solved in two separate stages, recent research shows end to end models can achieve better results. This requires differentiating through a discrete combinatorial function. Models that use differentiable surrogates are prone to approximation errors, while existing exact models are limited to dynamic programming, or they do not generalize well with scarce data. In this work we propose a novel divide and conquer algorithm based on transition points to reason over exact optimization problems and predict the coefficients using the optimization loss. Moreover, our model is not limited to dynamic programming problems. We also introduce a greedy version, which achieves similar results with less computation. In comparison with other predict+optimize frameworks, we show our method outperforms existing exact frameworks and can reason over hard combinatorial problems better than surrogate methods.

poster session 2 @ blue 4, poster session 9 @ blue 4, poster session 2, poster session 9

Combinatorial optimization problems are ubiquitous for decision making in planning social infrastructures. In real-world scenarios, a decision-maker needs to solve his/her problem iteratively until he/she satisfies solutions, but such an iterative process remains challenging. This paper studies a new explainable framework, particularly for finding meeting points, which is a key optimization problem for designing facility locations. Our framework automatically fills the gap between its input instance and instances from which a user could obtain the desired outcome, where computed solutions are judged by the user. The framework also provides users with explanations, representing the difference of instances for deeply understanding the process and its inside. Explanations are clues for users to understand their situation and implement suggested results in practice (e.g., designing a coupon for free travel). We experimentally demonstrate that our search-based framework is promising to solve instances with generating explanations in a sequential decision-making process.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 2 @ blue 4, poster session 2, poster session 9, oral session 2

Column Generation (CG) is an effective method for solving large-scale optimization problems. CG starts by solving a subproblem with a subset of columns (i.e., variables) and gradually includes new columns that can improve the solution of the current subproblem. The new columns are generated as needed by repeatedly solving a pricing problem, which is often NP-hard and is a bottleneck of the CG approach. To tackle this, we propose a Machine-Learning-based Pricing Heuristic (MLPH) that can generate many high-quality columns efficiently. In each iteration of CG, our MLPH leverages an ML model to predict the optimal solution of the pricing problem, which is then used to guide a sampling method to efficiently generate multiple high-quality columns. Using the graph coloring problem, we empirically show that MLPH significantly enhances CG as compared to six state-of-the-art methods, and the improvement in CG can lead to substantially better performance of the branch-and-price exact method.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 2 @ blue 4, poster session 2, poster session 9, oral session 2

The k-undercover Boolean Matrix Factorization problem aims at approximating an (m×n) Boolean matrix X as the Boolean product of an (m×k) and a (k×n) matrices A ◦ B such that X is a cover of A ◦ B, i.e., no representation error is allowed on the 0’s entries of the matrix X. In this paper, we propose two exact methods based on MaxSAT encodings to infer optimal and “block-optimal” k-undercover. From a theoretical standpoint, we prove that our method of inferring “block-optimal” k-undercover is a (1−1/e)-approximation for the optimal k-undercover problem, and from a practical standpoint, experimental results show that our “block-optimal” k-undercover algorithm outperforms the state of the art even when compared with algorithms for the more general k-undercover Boolean Matrix Factorization problem for which only minimizing reconstruction error is required.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 9 @ blue 4, poster session 2, poster session 9, oral session 9

A weak backdoor, or simply a backdoor, for a Boolean SAT formula F into a class of SAT formulae C is a partial truth assignment T such that F[T] is in C and satisfiability is preserved. The problem of finding a backdoor from class C1 into class C2, or WB(C1,C2), can be stated as follows: Given a formula F in C1, and a natural number k, determine whether there exists a backdoor for F into C2 assigning at most k variables. The class 0-Val contains all Boolean formulae with at least one negative literal in each clause. We design a new algorithm for WB(3CNF, 0-Val) by reducing it to a local search variant of 3-SAT. We show that our algorithm runs in time O*(2.562^k), improving on the previous state-of-the-art of O*(2.85^k). Here, the O* notation is a variant of the big-O notation that allows to omit polynomial factors in the input size. Next, we look at WB(3CNF, Null), where Null is the class consisting of the empty formula. This problem was known to have a trivial running time upper bound of O*(6^k) and can easily be solved in O*(3^k) time. We use a reduction to Conflict-Free-d-Hitting-Set to prove an upper bound of O*(2.2738^k), and also prove a lower bound of 2^o(k) assuming the Exponential Time Hypothesis. Finally, Horn is the class of formulae with at most one positive literal per clause. We improve the previous O*(4.54^k) running time for WB(3CNF, Horn) problem to O*(4.17^k), by exploiting the structure of the SAT instance to give a novel proof of the non-existence of the slowest cases after a slight restructuring of the branching priorities.

poster session 2 @ blue 4, poster session 9 @ blue 4, poster session 2, poster session 9

The Maximum $k$-Defective Clique Problem (MDCP), as a clique relaxation model, has been used to solve various problems. Because it is a computational hard task, previous works can hardly solve the MDCP for massive sparse graphs derived from real-world applications. In this work, we propose a novel branch-and-bound algorithm to solve the MDCP based on several new techniques. First, we propose two new upper bounds of the MDCP as well as corresponding reduction rules to remove redundant vertices and edges. The proposed reduction rules are particularly useful for massive graphs. Second, we present another new upper bound by counting missing edges between fixed vertices and an unfixed vertex for cutting branches. We perform extensive computational experiments to evaluate our algorithm. Experimental results show that our reduction rules are very effective for removing redundant vertices and edges so that graphs are reduced greatly. Also, our algorithm can solve benchmark instances efficiently, and it has significantly better performance than state-of-the-art algorithms.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 2 @ blue 4, poster session 2, poster session 9, oral session 2

We introduce novel methods for encoding acyclicity and s-t-reachability constraints for propositional formulas with underlying directed graphs. They are based on \emph{vertex elimination graphs}, which makes them suitable for cases where the underlying graph has a low \emph{directed elimination width}. In contrast to solvers with ad hoc constraint propagators for acyclicity and reachability constraints such as GraphSAT, our methods encode these constraints as standard propositional clauses, making them directly applicable with any SAT solver. An empirical study demonstrates that our methods together with an efficient SAT solver do often outperform both earlier encodings of these constraints as well as GraphSAT, particularly when underlying graphs have low directed elimination width.

poster session 2 @ blue 4, poster session 9 @ blue 4, poster session 2, poster session 9

The diversified top-k weight clique (DTKWC) search problem is an important generalization of the diversified top-k clique search problem, which extends the DTKC search problem by taking into account the weight of vertices. This problem involves finding at most k maximal weighted cliques that cover maximum weight of vertices with low overlapping in a given graph. In this study, a mixed integer linear program constraint formulation is proposed to model DTKWC search problem and an efficient hybrid evolutionary algorithm (HEA-D) based on some heuristic strategies is proposed to tackle it. Experiments on two sets of 110 graphs show that HEA-D outperforms the state-of-art methods.

poster session 2 @ blue 4, poster session 9 @ blue 4, poster session 2, poster session 9

Tree ensembles (TEs) denote a prevalent machine learning model that do not offer guarantees of interpretability, that represent a challenge from the perspective of explainable artificial intelligence. Besides model agnostic approaches, recent work proposed to explain TEs with formally-defined explanations, which are computed with oracles for propositional satisfiability (SAT) and satisfiability modulo theories. The computation of explanations for TEs involves linear constraints to express the prediction. In practice, this deteriorates scalability of the underlying reasoners. Motivated by the inherent propositional nature of TEs, this paper proposes to circumvent the need for linear constraints and instead employ an optimization engine for pure propositional logic to efficiently handle the prediction. Concretely, the paper proposes to use a MaxSAT solver and exploit the objective function to determine a winning class. This is achieved by devising a propositional encoding for computing explanations of TEs. Furthermore, the paper proposes additional heuristics to improve the underlying MaxSAT solving procedure. Experimental results obtained on a wide range of publicly available datasets demonstrate that the proposed MaxSAT-based approach is either on par or outperforms the existing reasoning-based explainers, thus representing a robust and efficient alternative for computing formal explanations for TEs.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 9 @ blue 4, poster session 2, poster session 9, oral session 9

MAX k-SAT is one of canonical NP-hard problems. Its variation called random MAX k-SAT problem was suggested in order to understand how hard it is to solve instances of the problem on average. The most common random model from which random instances get sampled is the uniform model. However, the uniform model, while useful for studying properties of the space of all k-CNF formulas as a whole, cannot capture all the structural properties we observe in the real-world instances. Therefore, we propose to use another random model called configuration model, which is able to produce instances with an arbitrary variable's degree distribution. Thus, we may focus and ``probe'' different regions of the space of all k-CNF formulas. There are many questions one may ask about the instances from configuration model, and in this paper we study how effective the pure literal elimination rule (or heuristic) performs when solving random MAX k-SAT instances having an arbitrary but fixed variable's degree distribution. We provide an equality that depends on the distribution of degrees, solving which one obtains the number of clauses the pure literal elimination rule satisfies. We also show how the distribution of variable degrees changes over time as the heuristic progresses.

poster session 2 @ blue 4, poster session 9 @ blue 4, oral session 9 @ blue 4, poster session 2, poster session 9, oral session 9

The non-dominated sorting genetic algorithm II (NSGA-II) is the most intensively used multi-objective evolutionary algorithm (MOEA) in real-world applications. However, in contrast to several simple MOEAs analyzed also via mathematical means, no such study exists for the NSGA-II so far. In this work, we show that mathematical runtime analyses are feasible also for the NSGA-II. As particular results, we prove that with a population size larger than the Pareto front size by a constant factor, the NSGA-II with two classic mutation operators and three different ways to select the parents satisfies the same asymptotic runtime guarantees as the SEMO and GSEMO algorithms on the basic OneMinMax and LOTZ benchmark functions. However, if the population size is only equal to the size of the Pareto front, then the NSGA-II cannot efficiently compute the full Pareto front (for an exponential number of iterations, the population will always miss a constant fraction of the Pareto front). Our experiments confirm the above findings.

poster session 2 @ blue 4, poster session 9 @ blue 4, poster session 2, poster session 9