LP-Based Weighted Model Integration over Non-Linear Real Arithmetic
Authors: S. Akshay, Supratik Chakraborty, Soroush Farokhnia, Amir Goharshady, Harshit Jitendra Motwani, Đorđe Žikelić
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, we present extensive experimental results, demonstrating the superior performance of our method on a range of WMI tasks for rational and radical functions when compared to state-of-the-art tools for WMI, in terms of both applicability and tightness. |
| Researcher Affiliation | Academia | 1Indian Institute of Technology Bombay, 2Hong Kong University of Science and Technology, 3University of Oxford, 4Max Planck Institute for Software Systems, 5Singapore Management University EMAIL, EMAIL, EMAIL, EMAIL, EMAIL |
| Pseudocode | Yes | The pseudocode of our algorithm is shown in Algorithm 1. Algorithm 1 Volume Approximation of Semi-algebraic Sets |
| Open Source Code | Yes | Both versions of the tool [Akshay et al., 2025b], i.e. standalone or integrated with [Spallitta et al., 2024], are free and open-source software and publicly available at Git Hub1. 1Our tool is available at: https://github.com/destrat18/wmilp, 2025. |
| Open Datasets | No | To showcase the merits and limitations of each approach, we considered two families of functions as our benchmarks: (A) Randomly-generated Rational Functions. To ensure unbiased evaluation and demonstrate the robustness of our method across diverse and arbitrary cases, we generated a set of 60 rational functions, half with one variable and the other half with two variables. The polynomials used in these rational functions are of degree two or three and their coefficients were picked randomly. (B) Randomly-generated Radical Functions. This benchmark family is similar to the previous case, except that we consider radical functions instead of mere rational functions. This set also contains 60 benchmarks, half of which are square roots of polynomials. As in the previous case, the coefficients are chosen randomly. The paper describes how the benchmark functions were generated but does not provide concrete access information (link, DOI, repository) to these generated datasets. |
| Dataset Splits | No | The paper defines two families of randomly-generated functions as benchmarks: 60 rational functions and 60 radical functions. It does not mention any training, validation, or test splits for these benchmarks, which is typical for experiments involving model training. This paper focuses on an integration method, and the concept of dataset splits in the machine learning sense is not applicable or discussed. |
| Hardware Specification | Yes | All experiments were performed on an Intel Xeon Gold 5115 CPU (2.40GHz, 16 cores) running Ubuntu 20.04 with 64 GB of RAM. |
| Software Dependencies | Yes | We implemented our approach in Python 3 and used Sym Py [Meurer et al., 2017] and Num Py [Harris et al., 2020] for symbolic computations. We also employed Gurobi [Gurobi Optimization, LLC, 2023] to solve the resulting LP instances. |
| Experiment Setup | Yes | In all experiments, we set ϵ = 0.1 and enforce a time limit of 1 hour per instance for all baselines. |