Weighted Model Integration with Orthogonal Transformations
Authors: David Merrell, Aws Albarghouthi, Loris D'Antoni
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our evaluation demonstrates our technique s ability to improve the time required to achieve exact probability bounds. |
| Researcher Affiliation | Academia | David Merrell, Aws Albarghouthi and Loris D Antoni University of Wisconsin Madison Department of Computer Sciences {dmerrell, aws, loris}@cs.wisc.edu |
| Pseudocode | No | The paper describes algorithms and methods but does not provide structured pseudocode blocks or algorithms labeled as such. |
| Open Source Code | No | The paper does not provide explicit statements or links for the open-sourcing of its own implementation code. It mentions using third-party tools like Z3 SMT solver and Redlog. |
| Open Datasets | No | The paper mentions generating 'random benchmarks' and adapting 'random-walk benchmarks from the programming languages literature [Chatterjee et al., 2016]'. While a citation is provided, there is no direct link, DOI, or specific repository name for accessing the exact datasets used. |
| Dataset Splits | No | The paper does not specify training, validation, or test dataset splits with percentages, counts, or references to predefined splits. |
| Hardware Specification | No | The paper does not specify any hardware components (e.g., CPU, GPU models, memory, or specific cloud instances) used for running the experiments. |
| Software Dependencies | Yes | We implemented our orthogonal transformations technique atop an implementation of the algorithm proposed in [Albarghouthi et al., 2017a], which uses the Z3 SMT solver [De Moura and Bjørner, 2008] to perform hyperrectangular decomposition. ... after using Redlog 2 to eliminate quantifiers from the formula. |
| Experiment Setup | Yes | We let each formula ϕ run for 100 seconds, where we, in parallel, ran WMI(ϕ) and WMI( ϕ). |