Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
201
datasets available to search
ShareScore release 0.9.0
Dataset results
201 results for “SAT”
On CNF Conversion for SAT and SMT Enumeration: Benchmarks, Results and Plots
<p>Experimental results for the paper:<br><br><a title="Arxiv Link" href="https://arxiv.org/abs/2303.14971" target="_blank" rel="noopener">On CNF encoding for SAT and SMT enumeration</a>, Gabriele Masina, Giuseppe Spallitta and Roberto Sebastiani. ArXiv, 2024.</p> <p>Content:</p> <ul> <li><code>aig-bench.zip</code> <code>iscas85-bench.zip</code> <code>syn-bool-bench.zip</code> contain the inputs and results for the Boolean benchmarks. Each zip contains: <ul> <li><code>data/</code> that contains the input data</li> <li><code>results-<tool>/</code> for each tested tool.</li> </ul> </li> <li><code>syn-lra-bench.zip</code> <code>wmi-bench.zip</code> contain the inputs and results for the Boolean benchmarks. Each zip contains: <ul> <li><code>data/</code> that contains the input data</li> <li><code>results-<tool>/</code> for each tested tool.</li> </ul> </li> <li><code>plot-d4</code>, <code>plot-msat</code>, <code>plot-tabularallsat</code>, <code>plot-tabularallsmt</code> contain the plots for enumeration with different tools. </li> <li><code>plot-msat-sat</code> contains the plot for plain satisfiability using MathSAT.</li> </ul> <p>Results are stored in JSON files, where the field <code>"mode"</code> indicates the CNF transformation used to preprocess the input:</p> <ul> <li><code>LAB</code> for Tseitin CNF</li> <li><code>LABELNEG_POL</code> for Plaisted&Greenbaum CNF, using negative labels for subformulas occurring negatively only.</li> <li><code>NNF_MUTEX_POL</code> for NNF+Plaisted&Greenbaum CNF+mutex clauses, as described in the paper</li> </ul> <p>The source code used to run the experiments is available at <a href="https://doi.org/10.5281/zenodo.14033422" target="_blank" rel="noopener">https://doi.org/10.5281/zenodo.14033422</a>.</p> <p> </p>
DMS-SAT_GLOBAL_MONTHLY_DMS_DMSPt_CLIM_v1.0.0
<p>README file for the global DMS and DMSPt fields derived with DMS-SAT</p> <p>Martí Galí Tàpias, 2019-02-06</p> <p>Questions and requests can be addressed to:<br> marti.gali.tapias@gmail.com</p> <p>Content and data sources<br> ========================<br> This dataset contains gobal fields of dimethylsulfide (DMS) and dimethylsulfoniopropionate in the sea surface layer, estimated with different remote sensing algorithms.<br> It is based on ocean colour data publicly available at https://oceancolor.gsfc.nasa.gov/.<br> Monthly climatological data are provided at 9 km, 1 and 5 degree resolutions on lat-lon grids.<br> Different satellite products have been used for chlorophyll_a and euphotic layer depth, as indicated in the names of the files:</p> <p>{Variable}_{PERIOD}_{algorithm}_{spatial resolution}_{chlorophyll product}_{euphotic layer product}.nc</p> <p>{chlorophyll product}: CHL corresponds to OC4-CI, GSM to Garver-Siegel-Maritorena.<br> {euphotic layer product}: KD490 corresponds to diffuse attenuation coefficient at 490 nm, ZLEE correspond to Lee et al. algorithm.</p> <p>Note that CHL is not used in VS07 although it appears in the file name.</p> <p>Please check Galí et al. 2018 Biogeosciences for details.</p> <p>This dataset is related to <a href="https://doi.org/10.5281/zenodo.2205131">doi.org/10.5281/zenodo.2205131</a></p> <p>References<br> ==========<br> Galí, M., Devred, E., Levasseur, M., Royer, S. J., & Babin, M. (2015). A remote sensing algorithm for planktonic dimethylsulfoniopropionate (DMSP) and an analysis of global patterns. Remote Sensing of Environment, 171, 171-184. https://doi.org/10.1016/j.rse.2015.10.012</p> <p>Galí, M., Levasseur, M., Devred, E., Simó, R., & Babin, M. (2018). Sea-surface dimethylsulfide (DMS) concentration from satellite data at global and regional scales. Biogeosciences, 15(11), 3497-3519. https://doi.org/10.5194/bg-15-3497-2018</p> <p><br> How to cite<br> ===========<br> This dataset can be freely distributed, but please cite it using its DOI. When relevant, cite also the journal articles mentioned above.</p> <p>Acknowledgments<br> ================<br> I acknowledge NASA’s Ocean Biology Processing Group (OBPG) for making data freely available.</p> <p>======<br> Enjoy!<br> Martí Galí Tàpias</p> <p> </p>
A SAT Benchmark Suite for LTL Specification Sketching
<h1>LTL_Sketcher-SAT_Benchmark</h1> <p>This repository contains a set of formulas in Propositional Boolean Logic.<br>These formulas are generated during the execution of our <a href="https://github.com/rajarshi008/LTLSketcher/tree/master" target="_blank" rel="noopener">LTLSketcher tool</a>.<br>Given an LTL sketch (i.e., a partial LTL formula) and a sample (i.e., a set of program executions labeled desired and undesired), the tool solves the LTL sketching problem, i.e., complete the sketch to a specification consistent with the data. (feel freet to check out our <a href="https://link.springer.com/chapter/10.1007/978-3-031-45332-8_2" target="_blank" rel="noopener">paper</a> for more information on this problem)<br>In essence, this is done by reducing the problem to a series of formulas in Propositional Boolean Logic and checking their satisfiability.</p> <h2>Naming convention:</h2> <p>This repository contains each formula both in the DIMACS and SMTLib format.<br>Each file follows the same naming convention:</p> <p><em>type__sample-file__sketch__size__algorithm-configuration__satisifability</em></p> <p><em>type</em>: indicates whether the formula is stored in the DIMACS or SMTLib format<br><em>sample-file</em>: refers to the sample (cf., <a href="https://github.com/rajarshi008/LTLSketcher/tree/master/experiment_results/generated_files/final_benchmark" target="_blank" rel="noopener">here</a>) used by the LTLSketcher tool<br><em>sketch</em>: refers to the sketch (cf., See experimental evaluation of our <a href="https://link.springer.com/chapter/10.1007/978-3-031-45332-8_2" target="_blank" rel="noopener">paper</a>) used by the LTLSketcher tool<br><em>size</em>: refers to the size of the complete solution (i.e., the number of subformulas of the complete specification)<br><em>algorithm-configuration</em>: our algorithm can be extended by two heuristics (BMC and suffix), this indicates which combination of heuristics was used (none, either one of the two, both)<br><em>satisfiability</em>: indicates whether the formula is satisfiable or not</p>
Large Uniform Random SAT Samples
<p>Large Random SAT samples generated with the following <em>samplers</em>:</p> <ul> <li>BDDSampler</li> <li>Spur</li> <li>QuickSampler </li> <li>KUS</li> <li>Unigen2</li> <li>Smarch </li> </ul>
The OPS-SAT case: test dataset
<p><i>The OPS-SAT case: test dataset</i> is the test split of the official dataset of <a href="https://kelvins.esa.int/opssat/home/"><strong>ESA's Kelvins</strong> <strong>"the OPS-SAT case" challenge</strong></a><strong>, </strong>created in collaboration<strong> with ESA's Φ-lab </strong>and <strong>ESA's OPS-SAT spacecraft operations team</strong>. It consists of<strong> 588 raw patches</strong> generated by cropping original acquisitions taken by the OPS-SAT cube-sat using its on-board camera. The patches have a resolution of <strong>200x200</strong> and are provided in <strong>.png</strong> format. Each patch was assigned through manual labeling to one of the following landcover classes: <strong>Agricultural, Cloud, Mountain, Natural, River, Sea_Ice, Snow, </strong>and <strong>Water.</strong></p><p>The competition's goal is, given a model of a neural network (in this case the <strong>EfficientNet-Lite0</strong>), to provide best possible network parameters to perform an <strong>on-board classification</strong> task. To this goal, competitors were free to use any data, including <a href="https://zenodo.org/records/6524750">The OPS-SAT case dataset</a>, which was released before the start of the competition.</p><p>The OPS-SAT case: test dataset was hidden from the competitors during the competition and was used to evaluate and rank their submissions. </p><p>More details about the competition setup and solution evaluation are on the <a href="https://kelvins.esa.int/opssat/home/">Kelvins competition platform</a>.</p>
SAT Competition 2004 Benchmarks and Raw Results
<p>Set of problems used for the SATISFIABILITY (SAT) competition organized in 2004. Problems are given in three categories: Industrial, Handmade (Now called "Crafted") and Random.</p>
Dataset: EchoStar Corporation (SATS) Stock Performance
This dataset provides historical stock market performance data for specific companies. It enables users to analyze and understand the past trends and fluctuations in stock prices over time. This information can be utilized for various purposes such as investment analysis, financial research, and market trend forecasting.
Text-fig. 4. Protothymallus elongatus (KRAMBERGER, 1885): ventral detail of the neurocranium (SMMGD SaT-168). in Revision Of The Cyprinids From The Early Oligocene Of The České Středohoří Mountains, And The Phylogenetic Relationships Of Protothymallus Laube, 1901 (Teleostei, Cyprinidae, Gobioninae)
Text-fig. 4. Protothymallus elongatus (KRAMBERGER, 1885): ventral detail of the neurocranium (SMMGD SaT-168).
Text-fig. 6. Protothymallus elongatus (KRAMBERGER, 1885): maxilla (the arrow marks the maxillary foramen; SMMGD Sat-165: 1). in Revision Of The Cyprinids From The Early Oligocene Of The České Středohoří Mountains, And The Phylogenetic Relationships Of Protothymallus Laube, 1901 (Teleostei, Cyprinidae, Gobioninae)
Text-fig. 6. Protothymallus elongatus (KRAMBERGER, 1885): maxilla (the arrow marks the maxillary foramen; SMMGD Sat-165: 1).
Text-fig. 2: Reconstruction of Protothymallus elongatus (KRAMBERGER, 1885) based on NHMV-1883, SMMGD-SaT 173, and UL-V2. in Revision Of The Cyprinids From The Early Oligocene Of The České Středohoří Mountains, And The Phylogenetic Relationships Of Protothymallus Laube, 1901 (Teleostei, Cyprinidae, Gobioninae)
Text-fig. 2: Reconstruction of Protothymallus elongatus (KRAMBERGER, 1885) based on NHMV-1883, SMMGD-SaT 173, and UL-V2.
Text-fig. 5. Protothymallus elongatus (KRAMBERGER, 1885): partly disarticulated skull (SMMGD SaT-141). in Revision Of The Cyprinids From The Early Oligocene Of The České Středohoří Mountains, And The Phylogenetic Relationships Of Protothymallus Laube, 1901 (Teleostei, Cyprinidae, Gobioninae)
Text-fig. 5. Protothymallus elongatus (KRAMBERGER, 1885): partly disarticulated skull (SMMGD SaT-141).
SAT Instances for Testing SFpC Validity and Reliability
<p>Random SAT samples generated with the following samplers:</p> <ul> <li>BDDSampler</li> <li>KUS</li> <li>QuickSampler </li> <li>Smarch </li> <li>Spur</li> <li>Unigen2</li> </ul> <p>These samples are used to check SFpC Soundness, i.e., to test whether SFpC produces results that are (i) valid and (ii) reliable. In other words, are SFpC results consistent (i) with the results obtained by other uniformity testing methods and (ii) when one sampler is tested repeatedly using different models?</p>
SAT-Inspired Higher-Order Eliminations
<p>This is the package containing the raw evaluation data for the paper "SAT-Inspired Higher-Order Eliminations" by Jasmin Blanchette and Petar Vukmirović.</p> <p>The problems used for the evaluation are located in the "problems" directory. The seven categories are</p> <p> seventeen_th0 (called S0 in Fig. 1 of the paper)<br> seventeen_th1 (called S1 in Fig. 1)<br> tptp_th0 (called TH0 in Fig. 1)<br> tptp_th1 (called TH1 in Fig. 1)<br> tptp_cnffof (called CF in Fig. 1)<br> tptp_tf0 (called TF0 in Fig. 1)<br> tptp_tf1 (called TF1 in Fig. 1)</p> <p>The empirical results are located in the "results" directory, under the following names, corresponding to the category names above:</p> <p> seventeen_th0_results.csv<br> seventeen_th1_results.csv<br> tptp_th0_results.csv<br> tptp_th1_results.csv<br> tptp_cnffof_results.csv<br> tptp_tf0_results.csv<br> tptp_tf1_results.csv</p> <p>The CSV files were produced by StarExec. Each nonheader row gives the prover's performance on one problem. For example, the row</p> <p> 74437543,Problems/AGT/AGT036^1.p,2900058,Zipperposition---2.2pre-hoelim-v2,2410,hlbe-in,92437,complete,2.09374,0.983524,1684480.0,Theorem,Theorem,THM-Ref,Ref,THM</p> <p>in "tptp_th0_results.csv" indicates that the HLBE inprocessing mode of Zipperposition ("hlbe-in") was able to prove the TPTP problem "AGT036^1.p", as indicated by the "THM" result in the last column. "THM" and "UNS" (unsatisfiable) correspond to a successful proof; other outcomes are considered failures.</p> <p>Figure 1 was generated using the script "script/gen_figure.py", which must be run from within the "script" directory.</p> <p>The "binaries" directory contains the StarExec package used to run the evaluation. The package is called "bin" in accordance with StarExec conventions. Inside it, "zipperposition" and "eprover-ho" are the 64-bit Linux binaries for the Zipperposition prover and its E backend, and the other files are scripts used to run various configurations in time slices. When running the scripts locally, set the environment variables "STAREXEC_CPU_LIMIT" and "STAREXEC_WALLCLOCK_LIMIT" to suitable time limits in seconds.</p> <p>Zipperposition was compiled from the repositiory version with the git commit hash 2a66166453ac32c0 on the "wip_ho_elimination_techniques" branch. E was compiled with the "--enable-ho" configuration option from an unspecified repository version. The Zipperposition and E repositories are available online (https://github.com/sneeuwballen/zipperposition and https://github.com/eprover/eprover).</p>
Uniform Random SAT Samples
<p>Random SAT samples generated with the following <em>samplers</em>:</p> <ul> <li>Spur</li> <li>QuickSampler </li> <li>Unigen2</li> <li>Smarch </li> </ul>
Using Resolution Proofs to Analyse CDCL SAT solvers
<p>Data for the article Janne I. Kokkala, Jakob Nordström: Using Resolution Proofs to Analyse CDCL SAT solvers, accepted to the 26th International Conference on Principles and Practice of Constraint Programming.</p> <p>Files:</p> <ul> <li><strong>solver.tgz</strong> – Source code of the modified Glucose 3.0 used in the experiments</li> <li><strong>instances.tar</strong> – All CNF instances used in the experiments (compressed individually using xz). Note that these are the formulas obtained after preprocessing, so they are not the same as used in the SAT races and competitions they are obtained from.</li> <li><strong>data-instances.txt</strong> – List of all benchmark instance filenames and IDs used to refer to them in other data files.</li> <li><strong>data-solvers.txt</strong> – Parameters used for each solver configuration (see the paper for explanation of where they were used).</li> <li><strong>data-solverstats.txt</strong> – For each solver configuration and instance, some data of the run</li> <li><strong>data-proofsizes.txt</strong> – For each solver configuration and instance, sizes of untrimmed proof, the trimmed solver proof, and the proof output by DRAT-trim, measured both in number of learnt clauses and in number of clause usages – note that for the clause usage counts, all unit clauses are considered to be used only once at the end (since that would result to a shorter resolution proof and is more related to the solver performance)</li> <li><strong>data-features.txt</strong> – For the solver used in the clause feature experiments, this file contains for each instance the frequency distribution of each feature (both absolute and percentile rank)</li> <li><strong>plots-features.pdf</strong> – Larger versions of the feature plots in the paper, including plots not shown in the paper.</li> <li><strong>plots-proofsizes.pdf</strong> – Plots of the data for the pairwise solver proof size comparison experiments.</li> </ul> <p> </p>
Dataset for On the Sparsity of XORs in Approximate Model Counting (SAT-20 Paper)
<p>The artifact consists of the necessary data to reproduce the results reported in the SAT-20 Paper titled "On the Sparsity of XORs in Approximate Model Counting". <br> <br> In particular, the artifact consists of the binaries, the log files generated by our computing cluster, and scripts to generate tables and the plots used in the paper. </p>
Benchmark Petri Net Models Used for the Evaluation of B-I-Sat
<p>Collection and documentation of the benchmark Petri net models used for the evaluation of the B-I-Sat algorithm.</p>
LLM-SAT-Eval
<p>Exploring the theme “Do static analysis tools foresee actual bug fixes?," this poster investigates the practical utility of Static Analysis Tools (SATs) in anticipating genuine bug fixes within software code-bases. Leveraging a dataset comprising bug-fix pairs, our study scrutinizes the efficacy of SATs through quantitative analysis, revealing a significant disparity between SAT outputs and actual bug fixes, with nearly 93% of pairs rated at 0. Employing qualitative insights from Gemini-pro Large Language Model, we corroborate these findings, observing prevalent terms such as "buggy line" and "not able" in bug detection. Furthermore, correlation analysis showcases a moderate positive correlation (0.3) between SAT outputs and known bug fixes, emphasizing the importance of alignment for favorable ratings. Our findings underscore the pressing need for enhanced bug detection methodologies, prompting further research in software quality assurance.</p>
CG:Shop 2022 Results: SAT-Based Local Search for Plane Subgraph Partitions
<p>The results for the CG:SHOP 2022 challenge achieved by team tuwien.</p>
Benchmarks used for the SAT 2005 Competition with raw results
<p>Set of benchmarjs used for the SAT 2005 competitions.</p> <p>Some benchmarks are not included because they were only distributed via their author's web site (IBM and Miroslav Velev problems).</p> <p>This set is the set that was distributed after the contest.</p> <p>Note that the benchmarks are distributed as shuffled problems.</p> <p>The competition was organised by the LRI (Orsay, France) and the CRIL (Lens, France) with the help of the university of Cincinnati and Intel. Organizers were Daniel Leberre, Olivier Roussel and Laurent Simon</p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.