An Exact Inference Scheme for MinSAT
Authors: Chu-Min Li, Felip Manyà
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We describe an exact inference-based algorithm for the Min SAT problem. Given a multiset of clauses φ, the algorithm derives as many empty clauses as the maximum number of clauses that can be falsified in φ by applying finitely many times an inference rule, and returns an optimal assignment. We prove the correctness of the algorithm, describe how it can be extended to deal with weighted Min SAT and weighted partial Min SAT instances, analyze the differences between the Max SAT and Min SAT inference schemes, and define and empirically evaluate the Min SAT Pure Literal Rule. |
| Researcher Affiliation | Academia | Chu-Min Li Huazhong Univ. of Science and Technology MIS, Universit e de Picardie Jules Verne Felip Many a Artificial Intelligence Research Inst. (IIIA) Spanish National Research Council (CSIC) |
| Pseudocode | Yes | Figure 1: An exact inference algorithm for Max SAT; Figure 2: An exact inference algorithm for Min SAT |
| Open Source Code | No | The paper does not provide any statement or link indicating that source code for the described methodology is publicly available. |
| Open Datasets | No | The paper mentions 'random Min-2SAT instances' but does not provide concrete access information (link, DOI, specific repository, or formal citation) for this dataset. |
| Dataset Splits | No | The paper does not specify exact percentages, sample counts, or citations to predefined splits for training, validation, or test sets. |
| Hardware Specification | No | The paper does not provide any specific hardware details such as GPU/CPU models, processor types, or memory used for running the experiments. |
| Software Dependencies | No | The paper mentions 'Min Satz' and 'Max Satz' solvers but does not provide specific version numbers for these or any other software dependencies crucial for replication. |
| Experiment Setup | Yes | Figure 3 compares the mean time, in seconds, needed by Min Satz to solve random Min-2SAT instances for different values of the ratio of the number of clauses to the number of variables (r) with a version of Min Satz that applies the Min SAT PLR (W), and a version of Min Satz that does not ap- ply the Min SAT PLR (W/O). A total of 100 instances were solved at each point of the plots. |