Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Dataset . 2021
License: CC BY
Data sources: Datacite
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Dataset . 2021
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Dataset . 2021
License: CC BY
Data sources: Datacite
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Dataset . 2021
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Dataset . 2021
License: CC BY
Data sources: Datacite
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
Smithsonian figshare
Dataset . 2021
License: CC BY
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
versions View all 4 versions
addClaim

SAT-Inspired Eliminations for Superposition

Authors: Vukmirovic, Petar; Blanchette, Jasmin; Heule, Marijn J.H.;

SAT-Inspired Eliminations for Superposition

Abstract

This archive contains the problems, raw evaluation results and scripts for running the experiments described in the paper "SAT-Inspired Inprocessing for Superposition" by Petar Vukmirovic, Jasmin Blanchette, and Marijn J.H. Heule available at https://matryoshka-project.github.io/pubs/satelimsup_paper.pdf The problems we used are stored in the "problems/" subdirectory, together with the required axioms (directory "Axioms"). They are separated in two groups, "Theorems" and "Satisfiable", as in the paper. In the "results/" directory, there are 6 files with names of the form "fD.csv", where D is a digit from 1 to 6. The digit corresponds to the figure from the paper, and the corresponding file contains experiment results for the figure labeled D. The columns give information about the results of the experiment run for a given prover configuration (e.g., CPU time, reported status, memory usage). Each row corresponds to one problem file, whose name is given in the "prob_name" column. The "i_solver" column corresponds to a prover. The "i_configuration" column corresponds to a configuration, where i is a natural number identifying a prover-configuration combination. Files named "fDsummary.csv" contain concise summaries of evaluation runs for a corresponding "fD.csv" file. Their columns are of the form "{solver}_{configuration}", and rows contain different statistics described in the "summary" column. The names of the configurations are self-explanatory and correspond to the ones used in the paper. For BCE, SPE, and PPE, if the configuration has no "inprocessing" in the name, the corresponding technique is used as preprocessing. The "zipperposition/" directory contains the scripts that execute the provided Zipperposition binary (compiled only for Linux) on a given problem using a given configuration. To run Zipperposition on a single problem using some configuration, you can use scripts with the name "run_*.sh", where * stands for the configuration used in the evaluation. The configuration names match the ones described in the files "fD.csv". The scripts take two arguments: (1) the path to the TPTP problem and (2) the CPU timeout. For example, to run problem with the path "~/puzzling.p" using the configuration "bce", execute ./run_bce.sh ~/puzzling.p 240 A working installation of python3 and bash is required. The source code for Zipperposition can be obtained from the "wip-hlbe-unit-eqs-checkpoint" branch of the Zipperposition git repository: git@github.com:sneeuwballen/zipperposition.git. The binary stored in "zipperposition/" corresponds to compiled sources tagged with the commit hash 41b3398647e243c8bf6911b3ee4ed4928b4e445d. Compilation instructions are as in the "README.md" file contained in the git repository.

Country
Netherlands
Keywords

TPTP problem, source code, Science Policy, 5 files, hash c 21457e Compilation instructions, Marijn J.H, CADE submission deadline, experiment results, evaluation results, Space Science, Environmental Sciences not elsewhere classified, quot, problems HLBE, python 3, BCE, Jasmin Blanchette, SAT-Inspired Eliminations, 22194 f 27327568fc, memory usage, prover configuration, CPU timeout, configuration names, Petar Vukmirovic, Medicine, PPE, SPE, HLBE implementation, prover-configuration combination, Biological Sciences not elsewhere classified, HLBE-enabled modes, unsatisfiable problems

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
    OpenAIRE UsageCounts
    Usage byUsageCounts
    visibility views 30
    download downloads 1
  • 30
    views
    1
    downloads
    Powered byOpenAIRE UsageCounts
Powered by OpenAIRE graph
Found an issue? Give us feedback
visibility
download
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
views
OpenAIRE UsageCountsViews provided by UsageCounts
downloads
OpenAIRE UsageCountsDownloads provided by UsageCounts
0
Average
Average
Average
30
1
Related to Research communities
Science and Innovation Policy Studies