Lifted Reasoning for Combinatorial Counting
Authors: Pietro Totis, Jesse Davis, Luc de Raedt, Angelika Kimmig
JAIR 2023 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Finally, we evaluate our contributions on a real-world combinatorics math problems dataset and synthetic benchmarks. |
| Researcher Affiliation | Academia | Pietro Totis EMAIL Jesse Davis EMAIL Luc De Raedt EMAIL Angelika Kimmig EMAIL Department of Computer Science, KU Leuven Celestijnenlaan 200A, 3001 Heverlee, Belgium |
| Pseudocode | Yes | Algorithm 1 COUNT Precondition: P = V,D,C,cf , V,C = {(ϕ,=,s)} Operator: COUNT (P)... Algorithm 2 COUNT Precondition: P = MC(V,D,C,cf) : V,C = {(ϕ,=,s)} C , cf {[| ],{| }} Operator: COUNT (P)... |
| Open Source Code | Yes | Co So2, a solver for the full range of problems expressible in Co La (Section 4). 2. Python implementation: https://github.com/Pietro Totis/Co So |
| Open Datasets | Yes | Finally, we evaluate our contributions on a real-world combinatorics math problems dataset and synthetic benchmarks. |
| Dataset Splits | No | The paper describes how synthetic benchmarks were generated by varying parameters like the number of TVs (P3), workers (P4), and letters/word size (P5) to create problems of increasing size. For example, 'For P3, starting from the original problem with 12 TVs of which 3 are defective (Problem 0 on the x scale), we add at each step i one defective TV and one working TV for i {1,...,10}, thus reaching 32 TVs of which 13 are defective in Problem 10.' This describes data generation strategies for synthetic data, but does not provide specific training/test/validation splits for any dataset, including the 'real-world combinatorics math problems dataset' (Dries et al., 2017) or the generated synthetic benchmarks. |
| Hardware Specification | Yes | We test Co So on the benchmarks on a machine equipped with a 4 cores/4 threads CPU and 32 Gb of RAM. |
| Software Dependencies | Yes | Clingo (Gebser et al., 2012) is one of the widely adopted solvers for ASP programs (version 5.4.0)... The sharp SAT version adopted is 12.08... We use ESSENCE 1.3 along with Conjure 2.3.0. |
| Experiment Setup | No | The paper states, 'We set a timeout of 300 seconds on each problem.' However, it does not provide detailed experimental setup information such as hyperparameters (e.g., learning rate, batch size, number of epochs) or specific training schedules that would typically be associated with a machine learning or model-training experimental setup. The description focuses on problem generation and benchmarking conditions rather than the internal configuration of the solver's methodology beyond the problem definition. |