Counting Maximal Satisfiable Subsets

Authors: Jaroslav Bendík, Kuldeep S. Meel3651-3660

AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental Our empirical evaluation demonstrates that our approach can scale to instances clearly beyond the reach of enumeration-based techniques. To demonstrate the empirical effectiveness of our approach, we implemented a Python-based prototype and performed a detailed empirical analysis.
Researcher Affiliation Academia 1 Masaryk University, Brno, Czech Republic 2 National University of Singapore, Singapore
Pseudocode No The paper describes its algorithmic framework and components using propositional logic formulas and descriptions, but it does not include any explicitly labeled 'Pseudocode' or 'Algorithm' blocks.
Open Source Code Yes Our tool is publicly available at: https://github.com/jar-ben/MSSCounting
Open Datasets Yes We used a collection of 1200 Boolean CNF formulas that were recently used in prior MUS literature (Liu and Luo 2018; Luo and Liu 2019)3. ... 3https://github.com/luojie-sklsde/MUS Random Benchmarks
Dataset Splits No The paper describes using a collection of 1200 Boolean CNF formulas as 'benchmarks' for evaluation but does not specify any training, validation, or test dataset splits.
Hardware Specification Yes All experiments were run using a time limit of 3600 seconds (1 hour) and computed on an AMD EPYC 7371 16Core Processor, 1 TB memory machine running Debian Linux 4.19.67-2.
Software Dependencies No The paper mentions software like GANAK, UWr Max Sat, FLINT, RIME, and Python, but it does not provide specific version numbers for these components.
Experiment Setup No The paper specifies a time limit of 3600 seconds for experiments and mentions the backend tools used, but it does not provide specific hyperparameters, model initialization details, or training configurations typical of a machine learning experimental setup.