Backdoor DNFs
Authors: Sebastian Ordyniak, Andre Schidler, Stefan Szeider
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We complement our theoretical findings by an empirical study. Our experiments show that backdoor DNFs provide a significant improvement over their predecessors. |
| Researcher Affiliation | Academia | 1University of Leeds, Leeds, UK 2TU Wien, Vienna, Austria |
| Pseudocode | Yes | Algorithm 1 Main method for finding a smallest BDNF. |
| Open Source Code | No | The paper mentions using third-party tools like PySAT and Cadical for SAT encoding and solving, but does not provide a link or statement for the open-sourcing of their own implementation of the methodology described in the paper. |
| Open Datasets | Yes | We compute BDNFs and BTs on a large number of CNF formulas, stemming from various applications like logistics, planning, and combinatorics. The instances form ten groups: (i) all interval series (ais)1, (ii iii) graph coloring (flat, pret)1, (iv) logistics car configuration (daimler) [Sinz et al., 2003], (v) parity function learning (parity)1, (vi) inductive inference (inductive)1, (vii) planning (blocksworld)1, (viii) pigeon hole (pigeon)1, and (ix x) vertex cover and treewidth for named graphs (vc and tw). 1https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html |
| Dataset Splits | No | The paper mentions using various SAT instances but does not specify training, validation, or test dataset splits (e.g., percentages or counts). |
| Hardware Specification | Yes | We run the experiments on servers with two Intel Xeon E5540 CPUs, each running at 2.53 GHz per core, use Ubuntu 18.04. Each run is limited to six hours and 12 GB RAM. |
| Software Dependencies | Yes | We compute the SAT encodings using Python 3.8.0 and Py SAT 1.6.02. |
| Experiment Setup | Yes | The algorithm for BDNFs is based on incremental SAT solving. It finds one potential term of a BDNF in each solver call. Once a term is found, it is added to the encoding and so excluded in future calls. We use a cardinality constraint on the size of the term to obtain only subset-minimal terms. When all the found terms together form a tautological DNF, the algorithm terminates. Termination is checked using a second incremental SAT solver instance, which checks, in increments of 1000 added terms, whether the DNF s negation is an unsatisfiable CNF. Finally, we minimize the DNF by computing a minimal unsatisfiable core [Belov et al., 2014] for its negation. The found DNF is then inclusion-minimal but not necessarily of smallest cardinality. We compute BTs using a recursive algorithm. The algorithm computes one branch of the tree at a time using a SAT solver call. The algorithm then calls itself for each sub-branch. |