Auditable Algorithms for Approximate Model Counting
Authors: Kuldeep S. Meel, Supratik Chakraborty, S. Akshay
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | The design of algorithms has traditionally focused on optimizing resources like time, space, or communication without necessarily considering how hard it is to independently certify correctness of results. ... Our proofs involve reasoning about specially constructed formulas with qantifier alternations, with incomplete information about parts of the formula. This is quite challenging in general, and one of our technical novelties lies in our application of the probabilistic method in the proofs. |
| Researcher Affiliation | Academia | Kuldeep S. Meel1 r Supratik Chakraborty2 r S. Akshay2 1 University of Toronto, Canada 2 Indian Institute of Technology Bombay, Mumbai, India |
| Pseudocode | Yes | Algorithm 1: Stock(F) ... Algorithm 2: Stock Audit(F, Stock(F)) ... Algorithm 3: Equal Cells Counter(F) ... Algorithm 4: Equal Cells Audit(F, Equal Cells Counter(F)) ... Algorithm 5: AFCounter(F) ... Algorithm 6: Count Auditor(F, AFCounter(F)) |
| Open Source Code | No | The paper does not provide an explicit statement about releasing the source code for the methodology described, nor does it provide a direct link to a code repository for their implementation. |
| Open Datasets | No | The paper is theoretical and primarily deals with Boolean formulas in a general sense, without specifying any particular dataset or providing access information for one. |
| Dataset Splits | No | This paper is theoretical and does not involve empirical validation on datasets, therefore, it does not specify training, validation, or test dataset splits. |
| Hardware Specification | No | The paper is theoretical and does not describe any experimental setup that would require hardware specifications. |
| Software Dependencies | No | The paper discusses the theoretical use of SAT/QBF solvers as proxies for oracles but does not specify any particular software, libraries, or their version numbers necessary for reproducing results. |
| Experiment Setup | No | The paper is theoretical and focuses on algorithm design and complexity analysis, not empirical experiments. Therefore, it does not include details on experimental setup, hyperparameters, or training configurations. |