Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs
Authors: Stephan Gocht, Jakob Nordström3768-3777
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our experimental evaluation of a SAT solver integration shows a dramatic decrease in proof logging and verification time compared to existing DRAT methods. |
| Researcher Affiliation | Academia | 1 Lund University, Lund, Sweden 2 University of Copenhagen, Copenhagen, Denmark |
| Pseudocode | Yes | Algorithm 1 Checking substitution redundancy |
| Open Source Code | Yes | We have implemented our method for representing XOR constraints and performing Gaussian elimination in a library with a simple, clean interface for SAT solvers. ... The used tools, benchmarks, data and evaluation scripts are available at https://doi.org/10.5281/zenodo.4569840. |
| Open Datasets | No | The paper describes using 'SAT competition benchmarks' and 'Tseitin formulas' for evaluation, which are problem instances for SAT solvers, not datasets used for training a model in the traditional machine learning sense. No explicit public access information is provided for a 'training dataset'. |
| Dataset Splits | No | The paper discusses solving SAT problems on benchmark instances but does not define or use training, validation, or test dataset splits in the context of machine learning model development. |
| Hardware Specification | Yes | All running times were measured on an Intel Core i3-7100U CPU @ 2.40GHz 2 with a memory limit of 8GB, disk write speed of 154 MB/s and read speed of 518 MB/s. |
| Software Dependencies | No | The paper mentions software like 'Mini Sat', 'Veri PB', 'Sat4j', 'Rounding Sat', and 'Kissat', and provides citations for some, but it does not specify explicit version numbers for these software dependencies as required for reproducibility. |
| Experiment Setup | No | The paper describes the integration of their library with Mini Sat and mentions the use of a 'lazy reason generation technique', but it does not provide specific numerical hyperparameter values or detailed system-level training settings for experimental reproducibility. |