Efficient Weighted Model Integration via SMT-Based Predicate Abstraction
Authors: Paolo Morettin, Andrea Passerini, Roberto Sebastiani
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results on synthetic and real-world data show drastic computational improvements over the original WMI formulation as well as existing alternatives for hybrid inference. and 7 Experiments Our implementation uses MATHSAT5 [Cimatti et al., 2013] for SMT reasoning and LATTE INTEGRALE [Loera et al., 2012] to compute integrals of polynomials. All experiments were run on a Virtual Machine with 7 cores running at a frequency of 2.2 GHz and 94 GB of RAM. |
| Researcher Affiliation | Academia | Paolo Morettin, Andrea Passerini, Roberto Sebastiani DISI, University of Trento, Italy. paolo.morettin@unitn.it, andrea.passerini@unitn.it, roberto.sebastiani@unitn.it |
| Pseudocode | Yes | Algorithm 1 WMI-PA(ϕ, w, x, A) |
| Open Source Code | No | The paper does not provide explicit concrete access to source code for the methodology described in this paper. |
| Open Datasets | Yes | The data was taken from the Strategic Road Network Dataset 5, which provides average journey times on all the motorways managed by the English Highways Agency. From this dataset we extrapolated polynomial distributions of journey times between all junctions, with a 15 minutes granularity. and 5https://data.gov.uk/dataset/dft-eng-srn-routes-journey-times |
| Dataset Splits | No | The paper describes data extraction and use but does not specify explicit training/validation/test dataset splits, percentages, or absolute sample counts. |
| Hardware Specification | Yes | All experiments were run on a Virtual Machine with 7 cores running at a frequency of 2.2 GHz and 94 GB of RAM. |
| Software Dependencies | Yes | Our implementation uses MATHSAT5 [Cimatti et al., 2013] for SMT reasoning and LATTE INTEGRALE [Loera et al., 2012] to compute integrals of polynomials. |
| Experiment Setup | Yes | Query timeout was set at 10000 seconds. |