Achterberg, Tobias
Refine
Year of publication
Document Type
- ZIB-Report (23)
- In Proceedings (9)
- Article (8)
- Doctoral Thesis (2)
- Book chapter (1)
- Other (1)
Keywords
- mixed integer programming (8)
- Mixed Integer Programming (7)
- Constraint Programming (3)
- Ganzzahlige Programmierung (3)
- IP (3)
- MIP (3)
- SAT (3)
- branch-and-cut (3)
- chip verification (3)
- constraint programming (3)
- integer programming (3)
- Branch-and-Bound (2)
- Chip-Verifikation (2)
- Constraint Programmierung (2)
- Integer Programming (2)
- MIPLIB (2)
- Mathematical Programming (2)
- ParaSCIP (2)
- Ubiquity Generator Framework (2)
- branch-and-bound (2)
- optimization software (2)
- scip (2)
- Algebraic Modelling Languages (1)
- Branch-And-Cut (1)
- Branching Rules (1)
- CP (1)
- CPAIOR (1)
- Chip Verification (1)
- Chipverifikation (1)
- Constraint Integer Programming (1)
- Distributed Memory (1)
- Eigenschaftsprüfer (1)
- Gurobi (1)
- IST-20 (1)
- Instances (1)
- Late Breaking Abstracts (1)
- MIP-Solver (1)
- MIPLIB2003 (1)
- MOMENTUM (1)
- Mathematische Programmierung (1)
- Mixed Integer Programming, Parallel processing, Node merging, Racing, ParaSCIP, Ubiquity Generator Framework, MIPLIB (1)
- Mixed-integer-programming (1)
- Modelling (1)
- Node merging (1)
- Optimierungssoftware (1)
- Optimization (1)
- Parallel Computing (1)
- Parallel processing (1)
- Problem Instances (1)
- Pseudocost Branching (1)
- Pseudocost-Branching (1)
- Racing ParaSCIP (1)
- Reliability-Branching (1)
- Strong-Branching (1)
- Supercomputer (1)
- Teaching (1)
- UMTS (1)
- Variable selection (1)
- Zählen (1)
- branch and cut (1)
- configuration (1)
- conflict analysis (1)
- constraint integer programming (1)
- counting (1)
- cplex (1)
- cut-based inequalities (1)
- domain propagation (1)
- feasibility pump (1)
- formal chip verification (1)
- formale Chip Verifikation (1)
- ganzzahlige Programme (1)
- massive parallization (1)
- mathematical model (1)
- micro chip (1)
- network detection (1)
- network planning (1)
- perfect power control (1)
- presolving (1)
- primal heuristic (1)
- primal heuristics (1)
- property checking (1)
- radio interface (1)
Institute
This article introduces constraint integer programming (CIP), which is a novel way to combine constraint programming (CP) and mixed integer programming (MIP) methodologies. CIP is a generalization of MIP that supports the notion of general constraints as in CP. This approach is supported by the CIP framework SCIP, which also integrates techniques for solving satisfiability problems. SCIP is available in source code and free for noncommercial use. We demonstrate the usefulness of CIP on three tasks. First, we apply the constraint integer programming approach to pure mixed integer programs. Computational experiments show that SCIP is almost competitive to current state-of-the-art commercial MIP solvers. Second, we demonstrate how to use CIP techniques to compute the number of optimal solutions of integer programs. Third, we employ the CIP framework to solve chip design verification problems, which involve some highly nonlinear constraint types that are very hard to handle by pure MIP solvers. The CIP approach is very effective here: it can apply the full sophisticated MIP machinery to the linear part of the problem, while dealing with the nonlinear constraints by employing constraint programming techniques.
Starting with the description of the Traveling Salesmen Problem formulation as given by van Vyve and Wolsey in the article Approximate extended formulations'', we investigate the effects of small variations onto the performance of contemporary mixed integer programming solvers. We will show that even minor changes in the formulation of the model can result in performance difference of more than a factor of 1000. As the results show it is not obvious which changes will result in performance improvements and which not.
In the recent years there has been tremendous progress in the development of algorithms to find optimal solutions for integer programs. In many applications it is, however, desirable (or even necessary) to generate all feasible solutions. Examples arise in the areas of hardware and software verification and discrete geometry. In this paper, we investigate how to extend branch-and-cut integer programming frameworks to support the generation of all solutions. We propose a method to detect so-called unrestricted subtrees, which allows us to prune the integer program search tree and to collect several solutions simultaneously. We present computational results of this branch-and-count paradigm which show the potential of the unrestricted subtree detection.
This article introduces constraint integer programming (CIP), which is a novel way to combine constraint programming (CP) and mixed integer programming (MIP) methodologies. CIP is a generalization of MIP that supports the notion of general constraints as in CP. This approach is supported by the CIP framework SCIP, which also integrates techniques from SAT solving. SCIP is available in source code and free for non-commercial use. We demonstrate the usefulness of CIP on two tasks. First, we apply the constraint integer programming approach to pure mixed integer programs. Computational experiments show that SCIP is almost competitive to current state-of-the-art commercial MIP solvers. Second, we employ the CIP framework to solve chip design verification problems, which involve some highly non-linear constraint types that are very hard to handle by pure MIP solvers. The CIP approach is very effective here: it can apply the full sophisticated MIP machinery to the linear part of the problem, while dealing with the non-linear constraints by employing constraint programming techniques.
We address the property checking problem for SoC design verification at the register transfer level (RTL) by integrating techniques from integer programming, constraint programming, and SAT solving. Specialized domain propagation and preprocessing algorithms for individual RTL operations extend a general constraint integer programming framework. Conflict clauses are learned by analyzing infeasible LPs and deductions, and by employing reverse propagation. Experimental results show that our approach outperforms SAT techniques for proving the validity of properties on circuits containing arithmetics.
This thesis introduces the novel paradigm of constraint integer programming (CIP), which integrates constraint programming (CP) and mixed integer programming (MIP) modeling and solving techniques. It is supplemented by the software SCIP, which is a solver and framework for constraint integer programming that also features SAT solving techniques. SCIP is freely available in source code for academic and non-commercial purposes. Our constraint integer programming approach is a generalization of MIP that allows for the inclusion of arbitrary constraints, as long as they turn into linear constraints on the continuous variables after all integer variables have been fixed. The constraints, may they be linear or more complex, are treated by any combination of CP and MIP techniques: the propagation of the domains by constraint specific algorithms, the generation of a linear relaxation and its solving by LP methods, and the strengthening of the LP by cutting plane separation. The current version of SCIP comes with all of the necessary components to solve mixed integer programs. In the thesis, we cover most of these ingredients and present extensive computational results to compare different variants for the individual building blocks of a MIP solver. We focus on the algorithms and their impact on the overall performance of the solver. In addition to mixed integer programming, the thesis deals with chip design verification, which is an important topic of electronic design automation. Chip manufacturers have to make sure that the logic design of a circuit conforms to the specification of the chip. Otherwise, the chip would show an erroneous behavior that may cause failures in the device where it is employed. An important subproblem of chip design verification is the property checking problem, which is to verify whether a circuit satisfies a specified property. We show how this problem can be modeled as constraint integer program and provide a number of problem-specific algorithms that exploit the structure of the individual constraints and the circuit as a whole. Another set of extensive computational benchmarks compares our CIP approach to the current state-of-the-art SAT methodology and documents the success of our method.
Modern applications of mathematical programming must take into account a multitude of technical details, business demands, and legal requirements. Teaching the mathematical modeling of such issues and their interrelations requires real-world examples that are well beyond the toy sizes that can be tackled with the student editions of most commercial software packages. We present a new tool, which is freely available for academic use including complete source code. It consists of an algebraic modeling language and a linear mixed integer programming solver. The performance and features of the tool are in the range of current state-of-the-art commercial tools, though not in all aspects as good as the best ones. Our tool does allow the execution and analysis of large real-world instances in the classroom and can therefore enhance the teaching of problem solving issues. Teaching experience has been gathered and practical usability was tested in classes at several universities and a two week intensive block course at TU Berlin. The feedback from students and teachers has been very positive.
The Feasibility Pump of Fischetti, Glover, Lodi, and Bertacco has proved to be a very successful heuristic for finding feasible solutions of mixed integer programs. The quality of the solutions in terms of the objective value, however, tends to be poor. This paper proposes a slight modification of the algorithm in order to find better solutions. Extensive computational results show the success of this variant: in 89 out of 121 MIP instances the modified version produces improved solutions in comparison to the original Feasibility Pump.
MIPLIB 2003
(2005)
This paper reports on the fourth version of the Mixed Integer Programming Library. Since ({\sc miplib}) is to provide a concise set of challenging problems, it became necessary to purge instances that became too easy. We present an overview of the 27 new problems and statistical data for all 60 instances.
Conflict analysis for infeasible subproblems is one of the key ingredients in modern SAT solvers to cope with large real-world instances. In contrast, it is common practice for today's mixed integer programming solvers to just discard infeasible subproblems and the information they reveal. In this paper we try to remedy this situation by generalizing the SAT infeasibility analysis to mixed integer programming. We present heuristics for branch-and-cut solvers to generate valid inequalities from the current infeasible subproblem and the associated branching information. SAT techniques can then be used to strengthen the resulting cuts. We performed computational experiments which show the potential of our method: On feasible MIP instances, the number of required branching nodes was reduced by 50\% in the geometric mean. However, the total solving time increased by 15\%. on infeasible MIPs arising in the context of chip verification, the number of nodes was reduced by 90\%, thereby reducing the solving time by 60\%.