Prime Compilation of Non-Clausal Formulae
Authors: Alessandro Previti, Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | This section evaluates the two algorithms proposed in this paper. The experiments were performed on an Intel Xeon E5-2630 2.60GHz, with 64GByte of memory, and running Ubuntu Linux. The time limit was set to 3600s and the memory limit to 10GByte. Algorithms 1 and 2 were implemented on top of Mini SAT3 [E en and S orensson, 2003] in a prototype called primer (PRIMe compil ER). [...] Table 3 shows the number of solved instances for each of the considered approaches. [...] As for the comparison between primer-a and primer-b and according to Table 3, one can readily conclude that computing all prime implicants PIn is generally more efficient for the Geffe generator and QG6 benchmarks than computing PIe. This can be explained by |PIn| being significantly smaller than |PIe| for these benchmarks. However, this is not the case for Fm PHPn and Fm GTn instances. Finally and as shown in Figure 1b, primer-b set to compute PIn consistently outperforms primer-a, thus being in general expected to find more prime implicants/implicates within a given time limit. |
| Researcher Affiliation | Academia | A. Previti UCD CASL Dublin, Ireland alessandro.previti@ucdconnect.ie A. Ignatiev INESC-ID, IST Lisbon, Portugal aign@sat.inesc-id.pt A. Morgado INESC-ID, IST Lisbon, Portugal ajrmorgado@gmail.com J. Marques-Silva INESC-ID, IST, Lisbon, Portugal UCD CASL Dublin, Ireland jpms@tecnico.ulisboa.pt |
| Pseudocode | Yes | Algorithm 1: Basic prime compilation" and "Algorithm 2: Alternative prime compilation |
| Open Source Code | No | The paper mentions that Algorithms 1 and 2 were implemented in a prototype called 'primer' but does not provide a link or explicit statement for its open-source availability. The provided link (footnote 3) is for Mini SAT3, which is a third-party tool used by the authors. |
| Open Datasets | Yes | Quasigroup classification problems. This set of benchmarks called QG6 was proposed in [Meier and Sorge, 2005] when encoding classification theorems for quasigroups. ... Cryptanalysis of the Geffe stream generator. Originally proposed in [Geffe, 1973], the Geffe stream generator is a combination of 3 LFSRs ... The corresponding Boolean formulae were constructed with the use of the Transalg system4, which is able to translate algorithms into Boolean formulae [Otpuschennikov et al., 2014]. ... Crafted formulae. This set comprises crafted non-clausal formulae ... a generalization of the construction proposed in [Bordeaux and Marques-Silva, 2012]. ... based on the ordering principle that any partial order on a finite set must have a maximal element [Beame et al., 2004]. |
| Dataset Splits | No | The paper describes the datasets used and how instances were generated (e.g., '200 different output sequences were generated (600 instances in total)'), but it does not provide specific details on training, validation, and test dataset splits (e.g., percentages, counts, or citations to predefined splits). |
| Hardware Specification | Yes | The experiments were performed on an Intel Xeon E5-2630 2.60GHz, with 64GByte of memory, and running Ubuntu Linux. |
| Software Dependencies | No | The paper mentions 'Mini SAT3', 'Transalg system', and 'CUDD BDD-package' as software used, but it does not provide specific version numbers for these components. |
| Experiment Setup | Yes | The time limit was set to 3600s and the memory limit to 10GByte. |