Europe
Improving the Efficiency of Dynamic Programming on Tree Decompositions via Machine Learning
Abseher, Michael (Vienna University of Technology) | Dusberger, Frederico (Vienna University of Technology) | Musliu, Nysret (Vienna University of Technology) | Woltran, Stefan (Vienna University of Technology)
Dynamic Programming (DP) over tree decompositions is a well-established method to solve problems โ that are in general NP-hard โ efficiently for instances of small treewidth. Experience shows that (i) heuristically computing a tree decomposition has negligible runtime compared to the DP step; (ii) DP algorithms exhibit a high variance in runtime when using different tree decompositions; in fact, given an instance of the problem at hand, even decompositions of the same width might yield extremely diverging runtimes. We thus propose here a novel and general method that is based on a selection of the best decomposition from an available pool of heuristically generated ones. For this purpose, we require machine learning techniques based on features of the decomposition rather than on the actual problem instance. We report on extensive experiments in different problem domains which show a significant speedup when choosing the tree decomposition according to this concept over simply using an arbitrary one of the same width.
On the Resiliency of Unit Propagation to Max-Resolution
Abramรฉ, Andrรฉ (Aix Marseille Universitรฉ) | Habet, Djamal (Aix Marseille Universitรฉ)
At each node of the search tree, Branch and Bound solvers for Max-SAT compute the lower bound (LB) by estimating the number of disjoint inconsistent subsets (IS) of the formula. IS are detected thanks to unit propagation (UP) then transformed by max-resolution to ensure that they are counted only once. However, it has been observed experimentally that the max-resolution transformations impact the capability of UP to detect further IS. Consequently, few transformations are learned and the LB computation is redundant. In this paper, we study the effect of the transformations on the UP mechanism. We introduce the notion of UP-resiliency of a transformation, which quantifies its impact on UP. It provides, from a theoretical point of view, an explanation to the empirical efficiency of the learning scheme developed in the last ten years. The experimental results we present give evidences of UP-resiliency relevance and insights on the behavior of the learning mechanism.
Finding Diverse Solutions of High Quality to Constraint Optimization Problems
Petit, Thierry (Worcester Polytechnic Institute and Mines de Nantes / LINA-CNRS / INRIA) | Trapp, Andrew C. (Worcester Polytechnic Institute)
A number of effective techniques for constraint-based optimization can be used to generate either diverse or high-quality solutions independently, but no framework is devoted to accomplish both simultaneously. In this paper, we tackle this issue with a generic paradigm that can be implemented in most existing solvers. We show that our technique can be specialized to produce diverse solutions of high quality in the context of over-constrained problems. Furthermore, our paradigm allows us to consider diversity from a different point of view, based on generic concepts expressed by global constraints.
Maximum Satisfiability Using Cores and Correction Sets
Bjorner, Nikolaj (Microsoft Research) | Narodytska, Nina (Carnegie Mellon University)
Core-guided MAXSAT algorithms dominate other methods in solving industrial MAXSAT problems. In this work, we propose a new efficient algorithm that is guided by correction sets and cores. At every iteration, the algorithm obtains a correction set or a core, which is then used to rewrite the formula using incremental and succinct transformations. We theoretically show that correction sets and cores have complementary strengths and empirically demonstrate that their combination leads to an efficient MAXSAT solver that outperforms state-of-the-art WPMS solvers on the 2014 Evaluation on industrial instances.
Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT
Berg, Jeremias (University of Helsinki) | Saikko, Paul (University of Helsinki) | Jรคrvisalo, Matti (University of Helsinki)
Solvers for the Maximum satisfiability (MaxSAT) problem find an increasing number of applications today. We focus on improving MaxHS โ one of the most successful recent MaxSAT algorithms โ via SAT-based preprocessing. We show that employing SAT-based preprocessing via the so-called labelled CNF (LCNF) framework before calling MaxHS can in some cases greatly degrade the performance of the solver. As a remedy, we propose a lifting of MaxHS that works directly on LCNFs, allowing for a tighter integration of SAT-based preprocessing and MaxHS. Our empirical results on standard crafted and industrial weighted partial MaxSAT Evaluation benchmarks show overall improvements over the original MaxHS algorithm both with and without SAT-based preprocessing.
A Multicore Tool for Constraint Solving
Amadini, Roberto (University of Bologna) | Gabbrielli, Maurizio (University of Bologna) | Mauro, Jacopo (University of Bologna)
In Constraint Programming (CP), a portfolio solver uses a variety of different solvers for solving a given Constraint Satisfaction / Optimization Problem. In this paper we introduce sunny-cp2: the first parallel CP portfolio solver that enables a dynamic, cooperative, and simultaneous execution of its solvers in a multicore setting. It incorporates state-of-the-art solvers, providing also a usable and configurable framework. Empirical results are very promising. sunny-cp2 can even outperform the performance of the oracle solver which always selects the best solver of the portfolio for a given problem.
Maximal Cooperation in Repeated Games on Social Networks
Moon, Catherine (Duke University) | Conitzer, Vincent (Duke University)
Standard results on and algorithms for repeated games assume that defections are instantly observable. In reality, it may take some time for the knowledge that a defection has occurred to propagate through the social network. How does this affect the structure of equilibria and algorithms for computing them? In this paper, we consider games with cooperation and defection. We prove that there exists a unique maximal set of forever-cooperating agents in equilibrium and give an efficient algorithm for computing it. We then evaluate this algorithm on random graphs and find experimentally that there appears to be a phase transition between cooperation everywhere and defection everywhere, based on the value of cooperation and the discount factor. Finally, we provide a condition for when the equilibrium found is credible, in the sense that agents are in fact motivated to punish deviating agents. We find that this condition always holds in our experiments, provided the graphs are sufficiently large.
Mechanism Design and Implementation for Lung Exchange
Luo, Suiqian (Tsinghua University) | Tang, Pingzhong (Tsinghua University)
We explore the mechanism design problem for lung exchange and its implementation in practice. We prove that determining whether there exists a non-trivial solution of the lung exchange problem is NP-complete. We propose a mechanism that is individually rational, strategy-proof and maximizes exchange size. To implement this mechanism in practice, we propose an algorithm based on Integer Linear Program and another based on search. Both of our algorithms for this mechanism yield excellent performances in simulated data sets.
A Deterministic Partition Function Approximation for Exponential Random Graph Models
Pu, Wen (LinkedIn Corporation) | Choi, Jaesik (Ulsan National Institute of Science and Technology) | Hwang, Yunseong (Ulsan National Institute of Science and Technology) | Amir, Eyal (University of Illinois at Urbana-Champaign)
Exponential Random Graphs Models (ERGM) are common, simple statistical models for social network and other network structures. Unfortunately, inference and learning with them is hard even for small networks because their partition functions are intractable for precise computation. In this paper, we introduce a new quadratic time deterministic approximation to these partition functions. Our main insight enabling this advance is that subgraph statistics is sufficient to derive a lower bound for partition functions given that the model is not dominated by a few graphs. The proposed method differs from existing methods in its ways of exploiting asymptotic properties of subgraph statistics. Compared to the current Monte Carlo simulation based methods, the new method is scalable, stable, and precise enough for inference tasks.
Context-Independent Claim Detection for Argument Mining
Lippi, Marco (University of Bologna) | Torroni, Paolo (University of Bologna)
Argumentation mining aims to automatically identify structured argument data from unstructured natural language text. This challenging, multi-faceted task is recently gaining a growing attention, especially due to its many potential applications. One particularly important aspect of argumentation mining is claim identification. Most of the current approaches are engineered to address specific domains. However, argumentative sentences are often characterized by common rhetorical structures, independently of the domain. We thus propose a method that exploits structured parsing information to detect claims without resorting to contextual information, and yet achieve a performance comparable to that of state-of-the-art methods that heavily rely on the context.