Algorithms for Deciding Counting Quantifiers over Unary Predicates
Authors: Marcelo Finger, Glauber De Bona
AAAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The latter is shown to lead to a viable implementation and experiments shows this algorithm presents a phase transition behavior. |
| Researcher Affiliation | Academia | Marcelo Finger Department of Computer Science University of Sao Paulo, Brazil; Glauber De Bona Department of Computer Science University College London, UK |
| Pseudocode | Yes | Algorithm 3.1 CQUBranch And Bound(ϕ) |
| Open Source Code | Yes | Available at http://cqu.sourceforge.net |
| Open Datasets | No | The paper states: 'We generate uniformly distributed random CQU-SAT instances in normal form...' rather than using a pre-existing public dataset. |
| Dataset Splits | No | The paper describes generating random instances and evaluating the solver's performance, but does not mention specific training/validation/test dataset splits. |
| Hardware Specification | No | The paper does not provide any specific details about the hardware used for running the experiments (e.g., CPU, GPU models, or memory specifications). |
| Software Dependencies | Yes | Column generation implemented using MINISAT 2.22; we implemented the Solve Relaxed Via Col Gen method using the linear solver Clp of the COIN-OR Project |
| Experiment Setup | Yes | For the first experiment, we fixed L = 100, k = 10 and n = 250 and varied the rate m/n from 0.5 to 8 in steps of 0.05. At each step, we generated randomly 100 cqu-instances and computed the percentage of satisfiable instances (%SAT, left axis) and the average time of computation in seconds (right axis). |