An official website of the United States government
While mixed integer linear programming (MILP) solvers are routinely used to solve a wide range of important science and engineering problems, it remains a challenging task for end users to write correct and efficient MILP constraints, especially for problems specified using the inherently non-linear Boolean logic operations. To overcome this challenge, we propose a syntax guided synthesis (SyGuS) method capable of generating high-quality MILP constraints from the specifications expressed using arbitrary combinations of Boolean logic operations. At the center of our method is an extensible domain specification language (DSL) whose expressiveness may be improved by adding new integer variables as decision variables, together with an iterative procedure for synthesizing linear constraints from non-linear Boolean logic operations using these integer variables. To make the synthesis method efficient, we also propose an over-approximation technique for soundly proving the correctness of the synthesized linear constraints, and an under-approximation technique for safely pruning away the incorrect constraints. We have implemented and evaluated the method on a wide range of benchmark specifications from statistics, machine learning, and data science applications. The experimental results show that the method is efficient in handling these benchmarks, and the quality of the synthesized MILP constraints is close to, or higher than, that of manually-written constraints in terms of both compactness and solving time.
more »
« less
This content will become publicly available on August 1, 2026
MiSo: A DSL for Robust and Efficient Solve and MInimize Problems
Many problems in computer graphics can be formulated as finding the global minimum of a function subject to a set of non-linear constraints (Minimize), or finding all solutions of a system of non-linear constraints (Solve). We introduce MiSo, a domain-specific language and compiler for generating efficient C++ code for low-dimensional Minimize and Solve problems, that uses interval methods to guarantee conservative results while using floating point arithmetic. We demonstrate that MiSo-generated code shows competitive performance compared to hand-optimized codes for several computer graphics problems, including high-order collision detection with non-linear trajectories, surface-surface intersection, and geometrical validity checks for finite element simulation.
more »
« less
- Award ID(s):
- 2313156
- PAR ID:
- 10625369
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- ACM Transactions on Graphics
- Volume:
- 44
- Issue:
- 4
- ISSN:
- 0730-0301
- Page Range / eLocation ID:
- 1 to 18
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We introduce a code generator that converts unoptimized C++ code operating on sparse data into vectorized and parallel CPU or GPU kernels. Our approach unrolls the computation into a massive expression graph, performs redundant expression elimination, grouping, and then generates an architecture-specific kernel to solve the same problem, assuming that the sparsity pattern is fixed, which is a common scenario in many applications in computer graphics and scientific computing. We show that our approach scales to large problems and can achieve speedups of two orders of magnitude on CPUs and three orders of magnitude on GPUs, compared to a set of manually optimized CPU baselines. To demonstrate the practical applicability of our approach, we employ it to optimize popular algorithms with applications to physical simulation and interactive mesh deformation.more » « less
-
QuadriFlow is a scalable algorithm for generating quadrilateral surface meshes based on the Instant Field-Aligned Meshes of Jakob et al. (ACM Trans. Graph. 34(6):189, 2015). We modify the original algorithm such that it efficiently produces meshes with many fewer singularities. Singularities in quadrilateral meshes cause problems for many applications, including parametrization and rendering with Catmull-Clark subdivision surfaces. Singularities can rarely be entirely eliminated, but it is possible to keep their number small. Local optimization algorithms usually produce meshes with many singularities, whereas the best algorithms tend to require non-local optimization, and therefore are slow. We propose an efficient method to minimize singularities by combining the Instant Meshes objective with a system of linear and quadratic constraints. These constraints are enforced by solving a global minimum-cost network flow problem and local boolean satisfiability problems. We have verified the robustness and efficiency of our method on a subset of ShapeNet comprising 17,791 3D objects in the wild. Our evaluation shows that the quality of the quadrangulations generated by our method is as good as, if not better than, those from other methods, achieving about four times fewer singularities than Instant Meshes. Other algorithms that produce similarly few singularities are much slower; we take less than ten seconds to process each model. Our source code is publicly available.more » « less
-
Abstract This study develops an integrated delivery assignment and route planning strategy for food banking operations, considering food supply and demand constraints, food item restrictions, and vehicle capacity constraints. A mixed‐integer linear model is formulated to maximize the total demand served and minimize the total travel cost imposed on delivery volunteers. An integrated solution algorithm is developed that includes Lagrangian relaxation and column generation. The algorithm decomposes the problem into assignment and routing components and solves each iteratively. The proposed methodology is applied to a case study in Wake County, NC. A series of sensitivity analyses are conducted to draw insights. The numerical results demonstrate the proposed methodology's capacity to solve complex problems in food delivery operations efficiently.more » « less
-
Abstract The randomized Kaczmarz methods are a popular and effective family of iterative methods for solving large-scale linear systems of equations, which have also been applied to linear feasibility problems. In this work, we propose a new block variant of the randomized Kaczmarz method, B-MRK, for solving linear feasibility problems defined by matrices. We show that B-MRK converges linearly in expectation to the feasible region. Furthermore, we extend the method to solve tensor linear feasibility problems defined under the tensor t-product. A tensor randomized Kaczmarz (TRK) method, TRK-L, is proposed for solving linear feasibility problems that involve mixed equality and inequality constraints. Additionally, we introduce another TRK method, TRK-LB, specifically tailored for cases where the feasible region is defined by linear equality constraints coupled with bound constraints on the variables. We show that both of the TRK methods converge linearly in expectation to the feasible region. Moreover, the effectiveness of our methods is demonstrated through numerical experiments on various Gaussian random data and applications in image deblurring.more » « less
