Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph
Authors: Vasily Alferov, Ivan Bliznets, Kirill Brilliantov
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We complement our theoretical findings with computational experiments. Note that the goal of the algorithm to be efficient when parameter k is small (such instances can arise during an execution of branching algorithm). If this is not the case then even simple brute-force algorithm outperform our algorithm. We compare performance of our solver with the state-of-the-art open source Max SAT solvers on type of instances for which our algorithm was designed. Experiments In this section, we present the experiments conducted to evaluate the performance of our implemented algorithm in C++. |
| Researcher Affiliation | Academia | Vasily Alferov1, Ivan Bliznets2, Kirill Brilliantov3 1Independent Researcher 2University of Groningen 3St. Petersburg Department of Steklov Mathematical Institute of the RAS |
| Pseudocode | No | The paper describes reduction and branching rules, and an algorithm verbally and through mathematical notation, but does not include any clearly labeled pseudocode or algorithm blocks. |
| Open Source Code | No | The paper mentions that the algorithm was "implemented in C++" and refers to a "full version" for implementation details, but does not provide a concrete link or explicit statement of code release for the methodology. |
| Open Datasets | No | The paper describes a custom test instance generator for evaluation (Generated Tests section), rather than using a publicly available or open dataset with access information. |
| Dataset Splits | No | The paper describes generated test instances but does not specify train/validation/test dataset splits, as the algorithm is exact and not trained on data in a traditional machine learning sense. |
| Hardware Specification | No | The paper does not provide specific details about the hardware (e.g., GPU/CPU models, memory) used for running the experiments. |
| Software Dependencies | No | The paper mentions that the algorithm was implemented in C++ and lists other Max SAT solvers, but it does not provide specific version numbers for compilers, libraries, or other software dependencies required to reproduce the experiment. |
| Experiment Setup | Yes | The generator used to test the capabilities of the algorithm accepts three parameters: a, b, and k. It creates a formula with ν(F) = ab and at most ab + k satisfiable clauses. ... To carry out the comparison, we set the parameters a and k to fixed values and linearly increased the parameter b. |