A Unifying Formal Approach to Importance Values in Boolean Functions
Authors: Hans Harder, Simon Jantsch, Christel Baier, Clemens Dubslaff
IJCAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Exploiting BDD-based symbolic methods and projected model counting, we devise and evaluate practical computation schemes for IVFs. We address computational aspects by devising practical computation schemes for IVFs using projected model counting [Aziz et al., 2015] and BDDs. In this section, we present and evaluate computation schemes for blame, influence, and CGMs. To evaluate our approaches, we conducted experiments on Boolean functions given as CNFs that were either randomly generated or generated from the ISCAS 99 dataset [Davidson, 1999; Compile! Project, 2023]. We always computed importance values w.r.t. the first variable in the input CNF and averaged the timings over 20 runs each. Our experiments were carried out on a Linux system with an i5-10400F CPU at 2.90GHz and 16GB of RAM. To compare our BDD-based and model counting approaches, Figure 1 shows timings for blame computations on random CNFs. Here, the BDD-based approach clearly outperforms the one based on projected model counting. This is also reflected in real-world benchmarks from ISCAS 99 shown in Table 1, where the approach based on model counting runs into timeouts for even small instances. |
| Researcher Affiliation | Academia | Hans Harder1,2 , Simon Jantsch2 , Christel Baier2,4 and Clemens Dubslaff3,4 1University of Paderborn 2Dresden University of Technology 3Eindhoven University of Technology 4Centre for Tactile Internet with Human-in-the-Loop (Ce TI) hans.harder@uni-paderborn.de, {simon.jantsch, christel.baier}@tu-dresden.de, c.dubslaff@tue.nl |
| Pseudocode | No | The paper does not contain any pseudocode or algorithm blocks. It uses mathematical definitions, theorems, and examples in textual form. |
| Open Source Code | Yes | An implementation of the computing schemes for IVFs can be found at https://github.com/graps1/impmeas. |
| Open Datasets | Yes | We conducted experiments on Boolean functions given as CNFs that were either randomly generated or generated from the ISCAS 99 dataset [Davidson, 1999; Compile! Project, 2023]. |
| Dataset Splits | No | The paper evaluates computation times on existing and randomly generated CNF instances. It does not describe a process of training or validating a model, thus no training, validation, or test splits are provided. The instances are used for performance evaluation, not model training/validation. |
| Hardware Specification | Yes | Our experiments were carried out on a Linux system with an i5-10400F CPU at 2.90GHz and 16GB of RAM. |
| Software Dependencies | No | We have implemented Traxler s method and our new computation schemes in Python, using Bu DDy [Lind-Nielsen, 1999] as BDD backend with automatic reordering and GPMC [Suzuki et al., 2015; Suzuki et al., 2017] for (projected) model counting. While specific tools are named, their version numbers are not provided, nor is a specific Python version. |
| Experiment Setup | No | The paper describes the types of instances used (random (n, 3n, 7)-CNFs and ISCAS 99 dataset) and the number of runs (averaged over 20 runs each). However, it does not provide specific experimental setup details such as hyperparameters, model initialization, or specific training configurations typical for machine learning experiments. |