A Clause Tableau Calculus for MaxSAT
Authors: Chu-Min Li, Felip Manyà, Joan Ramon Soler
IJCAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We define a clause tableau calculus for Max SAT, prove its soundness and completeness, and describe a tableau-based algorithm for Max SAT. Given a multiset of clauses φ, the algorithm computes both the minimum number of clauses that can be falsified in φ, and an optimal assignment. We also describe how the algorithm can be extended to solve weighted Max SAT and weighted partial Max SAT. It is the first time, to the best of our knowledge, that a tableau calculus has been employed in combinatorial optimization and, in particular, to solve Boolean optimization problems. |
| Researcher Affiliation | Academia | Chu-Min Li Huazhong Univ. of Science and Technology MIS, Universit e de Picardie Jules Verne Felip Many a and Joan Ramon Soler Artificial Intelligence Research Inst. (IIIA) Spanish National Research Council (CSIC) |
| Pseudocode | Yes | Figure 3: An exact clause tableau algorithm for Max SAT. |
| Open Source Code | No | The paper does not mention releasing source code for the described methodology. |
| Open Datasets | No | The paper describes a theoretical calculus and algorithm; it does not perform experiments on a dataset and therefore does not mention public dataset availability. |
| Dataset Splits | No | The paper focuses on theoretical development and algorithm description, not empirical evaluation. Thus, it does not specify any dataset splits (train/validation/test). |
| Hardware Specification | No | The paper describes a theoretical calculus and algorithm; it does not report on empirical experiments, and thus does not specify hardware used. |
| Software Dependencies | No | The paper describes a theoretical calculus and algorithm. It does not mention specific software dependencies with version numbers for implementation or experimentation. |
| Experiment Setup | No | The paper presents a theoretical calculus and algorithm, not an experimental setup. Therefore, it does not include details on hyperparameters or training settings. |