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.
52
datasets available to search
ShareScore release 0.9.0
Dataset results
52 results for “SMT”
Datset of automated economic reasoning problems for QE / SMT
<p>This dataset is generated by 45 economics theorems "A implies H" where A are assumptions and H a hypothesis. These are taken from textbooks and papers and chosen for their suitability for automatic solution with Quantifier Elimination (QE) or Satisfiability Modulo Theory (SMT) technology. </p> <p>For each theorem three problems are generated: checking the compatibility of the assumptions; checking for the existence of an example of the theorem; and checking for the existence of a counterexample. </p> <p>There are three files:</p> <p>1. EconomicReasoningBenchmarks-Apr18-SMT2.zip</p> <p>This zip file will uncompress into a directory with 45 files, one for each theorem stating the three existence checks within the SMT2 format. Thus these files are suitable for use with any SMT solver supporting the theory.</p> <p> </p> <p>2. EconomicReasoningBenchmarks-Apr20-Redlog.txt</p> <p>This plain text file can be run with the Redlog Package for the Computer Algebra System Reduce. It contains definitions and calls to Redlog's QE command to check for a counterexample for all 45 theorems.</p> <p> </p> <p>3. EconomicReasoningBenchmarks-Apr23-Maple.txt</p> <p>This plain text file is for use with the Maple Computer Algebra System. For each theorem it provides the polynomials used in the Tarski formula to check for a counterexample. The polynomials are given as a list of lists with the outer list representing logical OR between entries and each inner list logical AND. </p> <p> </p>
Dataset for "Phosphorus fractionation of recycled fertilizers reveals inadequacy of the SMT protocol"
<p>Raw dataset used in the manuscript "Phosphorus fractionation of recycled fertilizers reveals inadequacy of the SMT protocol"</p>
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>
TriCera Benchmarks: SMT-LIB Encodings of SV-COMP 2022 Benchmarks by TriCera
<p>This repository contains the SMT-LIB v2.6 encodings of a subset of SV-COMP 2022 benchmarks from the <em>reach-safety</em> and the <em>memsafety</em> categories, encoded by <a href="https://github.com/uuverifiers/tricera">TriCera</a> and <a href="https://github.com/zafer-esen/heap2array">heap2array</a> [1, 2]. The source benchmarks from SV-Comp 2022 (`.c` and `.i` files together with their accompanying `.yml` files) are not provided due to licensing reasons; the files are freely available for download at <a href="https://zenodo.org/record/5831003/export/hx">https://zenodo.org/record/5831003/export/hx</a></p> <p>- `benchmarks/heap` contains all heap benchmarks (encoded by TriCera using the <a href="https://arxiv.org/abs/2104.04224">theory of heaps</a>, used in [1] and [2]).<br> - `benchmarks/heap2array` contains all heap2array encoded benchmarks (encoded from heap benchmarks using heap2array, used in [1] and [2]).<br> - `benchmarks/nonHeapBms` contains all non-heap benchmarks (encoded by TriCera, used in [2]).</p> <p>[1] (to appear) Zafer Esen and Philipp Rümmer, "An SMT-LIB Theory of Heaps", SMT 2022<br> [2] (to appear) Zafer Esen and Philipp Rümmer, "TriCera: Verifying C Programs Using the Theory of Heaps", FMCAD 2022</p>
Dataset supporting the paper 'Integration of SMT-LIB Support into Maple'
<p>This dataset provides a listing of all distinct queries to the Maple commands <strong>is</strong> and <strong>coulditbe </strong>which occurred in the course of a complete run through the Maple library test suite using Maple 2017 on 26 July 2017. The results include:</p> <ul> <li>24085 distinct queries to <strong>is</strong> (which tests if a given proposition holds universally) - see file is_queries.txt</li> <li>5771 distinct queries to <strong>coulditbe</strong> (which tests if given proposition is satisfiable) - see file coulditbe_queries.txt</li> </ul> <p>The files are plaintext and each line corresponds to a distinct query. Queries are in Maple syntax and adhere to one of the following patterns:</p> <ul> <li><strong>coulditbe(</strong><em>X</em><strong>)</strong></li> <li><strong>coulditbe(</strong><em>X</em><strong>) assuming </strong><em>Y</em></li> <li><strong>is(</strong><em>X</em><strong>)</strong></li> <li><strong>is(</strong><em>X</em><strong>) assuming </strong><em>Y</em></li> </ul> <p>Here, <em>X</em> is the expression being tested (in Maple syntax) and <em>Y</em> is an expression sequence of one or more assumptions on symbols appearing in <em>X</em>.</p> <ul> </ul>
IDMT-SMT-Chord-Sequences Dataset
<p>The IDMT-SMT-CHORD-SEQUENCES dataset contains 15,000 4-32 seconds long chord progressions synthesized from MIDI data with 45 different instruments. The files are organized as 5,000 triplets with an anchor, similar and dissimilar chord progression. Metadata like tempo, meter, duration in bars, instrument, and chord progression is provided in JSON format. Also, an overview about all metadata along with the dataset split is stored in a CSV file.</p>
IDMT-SMT-Audio-Effects Dataset
<p>The IDMT-SMT-Audio-Effects database is a large database for automatic detection of audio effects in recordings of electric guitar and bass and related signal processing.</p> <p>The overall duration of the audio material is approx. 30 hours.</p> <p>The dataset consists of 55044 WAV files (44.1 kHz, 16bit, mono) with single recorded notes:</p> <ul> <li>20592 monophonic bass notes</li> <li>20592 monophonic guitar notes</li> <li>13860 polyphonic guitar sounds</li> </ul> <p>Overall, 11 different audio effects are incorporated:</p> <ul> <li>feedback delay</li> <li>slapback delay</li> <li>reverb</li> <li>chorus</li> <li>flanger</li> <li>phaser</li> <li>tremolo</li> <li>vibrato</li> <li>distortion</li> <li>overdrive</li> <li>no effect (unprocessed notes/sounds)</li> </ul> <p>2 different electric guitars and 2 different electric bass guitars, each with two different pick-up settings and up to three different plucking styles (finger plucked - hard, finger plucked - soft, picked) were used for recording.</p> <p>The notes cover the common pitch range of a 4-string bass guitar from E1 (41.2 Hz) to G3 (196.0 Hz) or the common pitch range of a 6-string electric guitar from E2 (82.4 Hz) to E5 (659.3 Hz).</p> <p>Effects processing was performed using a digital audio workstation and a variety of mostly freely available effect plugins.</p> <p>To organize the database, lists in XML format are used, which record all relevant information and are provided with the database as well as a summary of the used effect plugins and parameter settings.</p> <p>In addition, most of this information is also encoded in the first part of the file name of the audio files using a simple alpha-numeric encoding scheme. The second part of the file name contains unique identification numbers. This provides an option for fast and flexible structuring of the data for various purposes.</p>
IDMT-SMT-Bass-Single-Track Dataset
<p>The IDMT-SMT-BASS-SINGLE-TRACK dataset comprises of 17 bass lines from different music styles.</p> <p>It is intended as a public evaluation dataset for:</p> <ul> <li>retrieval of repetitive bass patterns</li> </ul> <p>For each bass line, the pattern length (in seconds) and the begin of the first pattern appearance (in seconds) is annotated.</p> <p>The patterns are in general no exact repetitions but instead contain occasional<br> pitch and rhythm variations.</p> <ul> <li>bass transcription</li> </ul> <p>Each note is annotated with the score-related parameters onset, offset and pitch.</p> <ul> <li>spatial transcription / estimation of the fretboard position</li> </ul> <p><br> Each note is annotated with the instrument-related parameters string number and fret number.</p> <ul> <li>estimation of bass guitar plucking styles</li> </ul> <p>Each note is played and annotated with one of the 5 plucking style classes:</p> <ul> <li>Finger-style (FS) - alternate plucking of the string using the index and<br> middle finger</li> <li>Picked (PK) - plucking of the string using a plastic pick</li> <li>Muted (MU) - plucking of the string using the thumb and index finger while simultaneously damping the string vibration using the palm of the hand</li> <li>Slap-Pluck (SP) - picking of a string using either the index or the middle finger (causing a collision between the string and the upper frets)</li> <li>Slap-Thumb (ST)- striking of the string using the thumb (causing a collision between the string and the upper frets)</li> </ul> <p> </p> <ul> <li>estimation of bass guitar expression styles (6 classes)</li> </ul> <p>Each note is played and annotated with one of the 6 expression style classes:</p> <ul> <li>Normal (NO) - no expression, just “regular” bass note playing</li> <li>Harmonics (HA) - flageolet tones</li> <li>Dead-note (DN) - damped, percussive note</li> <li>Bending (BE) - singular bending of the string during vibration</li> <li>Vibrato (VI) - periodic bending and releasing the string during vibration</li> <li>Slide (SL) - slide up or down after note is plucked</li> </ul>
IDMT-SMT-Drums Dataset
<p>The IDMT-SMT-Drums database is a medium-sized database for automatic drum transcription and source separation.</p> <p>The dataset consists of 608 WAV files (44.1 kHz, Mono, 16bit). The approximate duration is 2:10 hours.</p> <p>There are 104 polyphonic drum set recordings (drum loops) containing only the drum instruments kick drum, snare drum and hi-hat. For each drum loop, there are 3 training files for the involved instruments, yielding 312 training files for drum transcription purposes. The recordings are from three different sources:</p> <ul> <li>Real-world, acoustic drum sets (RealDrum)</li> <li>Drum sample libraries (WaveDrum)</li> <li>Drum synthesizers (TechnoDrum)</li> </ul> <p>For each drum loop, the onsets of kick drum, snare drum and hi-hat have been manually annotated. They are provided as XML and SVL files that can be assigned to the corresponding audio recording by their filename. Appropriate annotation file parsers are provided as MATLAB functions together with an example script showing how to import the complete dataset.</p> <p>The subsets TechnoDrum02 and WaveDrum02 contain 64 drum loops that are delivered together with perfectly isolated single tracks of kick drum, snare drum, and hi-hat in addition to the above-mentioned training files. Mixing the single tracks together yields the mixture drum loops, thus providing 192 reference signals for source separation experiments.</p>
IDMT-SMT-Chords Dataset
<p>The IDMT-SMT-CHORDS comprises of 16 MIDI generated audio files consists of various chord classes. Here we focused on chord voicings, which are commonly used on keyboard instruments and guitars. Based on this we categorized as Guitar and Non-Guitar instruments. We used several software instruments from Ableton Live and Garage Band to synthesize these MIDI files with various instruments such as piano, synthesizer pad, as well as acoustic and electric guitar.</p> <ul> <li>File duration: 4.1 Hours</li> <li># Chord segments: 7398</li> <li># WAV files: 16</li> <li>Chord duration: 2 seconds</li> <li>BPM: 120</li> <li>Time signature: 4/4</li> <li>Sampling rate: 44.1KHz</li> <li>Mono audio</li> </ul> <p>Non-Guitar</p> <p>The Non-Guitar files includes all chord types in all possible root note positions and inversions. For example, C Major triad chord is included with its two possible inversions C/E and C/G.</p> <p>All non-guitar chord classes are listed below:</p> <ul> <li>Major (+ 2 inversions)</li> <li>Minor (+ 2 inversions)</li> <li>Major 7 (+ 3 inversions)</li> <li>Minor 7 (+ 3 inversions)</li> <li>Power Chord - root and fifth note (+ 1 inversion)</li> <li>Dominant 7 (+ 3 inversions)</li> <li>Minor 7 flat 5 (+ 3 inversions)</li> </ul> <p>This gives us 576 non-guitar chord classes.</p> <p>Guitar</p> <p>The guitar files where generated based on barŕe chord voicings with the root note located on the low E, A, and D strings. For example, to modeling major chord and it’s voicings we use open position E maj, A maj and D maj shape and move 12 steps (including octave at 12<sup>th</sup> fret) thereby we get 39 positions (13*3).</p> <p>List of Guitar chord types:</p> <ul> <li>Major (+ 2 voicings)</li> <li>Minor (+ 2 voicings)</li> <li>Major 7 (+ 2 voicings)</li> <li>Minor 7 (+ 2 voicings)</li> <li>Power Chord - root and fifth note (+ 2 voicings)</li> <li>Dominant 7 (+ 2 voicings)</li> <li>Minor 7 flat 5 (+ 2 voicings)</li> </ul> <p>This gives us 273 different guitar chord classes.</p>
IDMT-SMT-Guitar Dataset
<p>The IDMT-SMT-GUITAR database is a large database for automatic guitar transcription. Seven different guitars in standard tuning were used with varying pick-up settings and different string measures to ensure a sufficient diversification in the field of electric and acoustic guitars. The recording setup consisted of appropriate audio interfaces, which were directly connected to the guitar output or in one case to a condenser microphone. The recordings are provided in one channel RIFF WAVE format with 44100 Hz sample rate.<br> <br> The dataset consists of four subsets. The first contains all introduced playing techniques (plucking styles: finger-style, muted, picked; expression styles: normal, bending, slide, vibrato, harmonics, dead-notes) and is provided with a bit depth of 24 Bit. It has been recorded using three different guitars and consists of about 4700 note events with monophonic and polyphonic structure. As a particularity the recorded files contain realistic guitar licks ranging from monophonic to polyphonic instrument tracks.</p> <p>The second subset of data consists of 400 monophonic and polyphonic note events each played with two different guitars. No expression styles were applied here and each note event was recorded and stored in a separate file with a bit depth of 16 Bit. The parameter annotations for the first and second subset are stored in XML format.</p> <p>The third subset is made up of five short monophonic and polyphonic guitar recordings. All five pieces have been recorded with the same instrument and no special expression styles were applied. The files are stored with a bit depth of 16 Bit and each file is accompanied by a parameter annotation in XML format.</p> <p>Additionally, a fourth subset is included, which was created for evaluation purposes in the context of chord recognition and rhythm style estimation tasks. This set contains recordings of 64 short musical pieces grouped by genre. Each piece has been recorded at two different tempi with three different guitars and is provided with a bit depth of 16 Bit. Annotations regarding onset positions, chords, rhythmic pattern length, and texture (monophony/polyphony) are included in various file formats.</p>
SMT-Solving Induction Proofs of Inequalities Benchmarking Repository
<p>This repository contains the full list of files and the benchmarking results that were used in the benchmarking processes described in the paper:<br> A.K. Uncu, J.H. Davenport and M. England. "SMT-Solving Induction Proofs of Inequalities". Proceedings of the 7th International Workshop on Satisfiability Checking and Symbolic Computation (SC^2 2022). </p> <p>The files are split in three branches. The Mathematica and Maple files include the calls that were made to the respective computer algebra systems, and the smt2 files are the ones used by the considered SMT solvers: Z3, CVC5 and Yices.</p> <p>The Benchmarking Results cvc has the results. The columns record the file names, the satisfiability outcome of the calls, then the times (in seconds) of the respective programmes. Any empty box (which the Maple:-RegularChains column has) would mean that the implementation does not accept that sort of input (this is due to rational functions - see the paper for details). Any time over 1200 seconds would mean that the program times out and the outcome of the question was not found in the given time.</p> <p> </p> <p> </p>
SMT-LIB release 2023 (non-incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smtlib.cs.uiowa.edu/">https://smtlib.cs.uiowa.edu/</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>non-incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
SMT-LIB release 2023 (incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smtlib.cs.uiowa.edu/">https://smtlib.cs.uiowa.edu/</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
Benchmarks from the paper titled "An SMT-LIB Theory of Heaps" submtted to SMT 2022
<p>Benchmarks from the paper titled "An SMT-LIB Theory of Heaps" submtted to SMT 2022</p> <p><strong>benchmarks/</strong><br> This directory contains all benchmarks (excluding SV-Comp sources).<br> - <strong>benchmarks/heap</strong> contains all heap benchmarks (smt2). <br> - <strong>benchmarks/heap2array</strong> contains all heap2array encoded benchmarks (smt2).</p> <p>The source benchmarks from SV-Comp 2022 (`.c` and `.i` files together with their accompanying `.yml` files) are not provided in this repository due to licensing reasons, but the files are freely available for download: <a href="https://zenodo.org/record/5831003/export/hx">https://zenodo.org/record/5831003/export/hx</a></p>
SMT-LIB release 2024 (non-incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smt-lib.org">https://smt-lib.org</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>non-incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
SMT-LIB release 2024 (incremental benchmarks)
<p>This is the SMT-LIB benchmark library: a large library of input problems, or benchmarks, written in the SMT-LIB language. More information about the SMT-LIB initiative can be found at <a href="https://smt-lib.org">https://smt-lib.org</a>. The contributor and licence of each benchmark is indicated in the metadata fields of each benchmark file.</p> <p>This collection contains the <strong>incremental benchmarks</strong>.</p> <p>Benchmarks are grouped by logic and compressed with the <code>zstd</code> compression algorithm using the <code>tar --zstd</code>. SMT-LIB benchmarks usually have a very high compression rate, be aware of the required disk space when uncompressing the archives. You can find the size of each archive in compressed and uncompressed form in the following list.</p>
Design of facilitated dissociation enables control over cytokine signaling duration - SMT raw data - ASneo2 - ASneo2 + Effector - intraFRET ASneo2
<p>This dataset contains the raw data for the Single-molecule tracking data of the manuscript: "Design of facilitated dissociation enables control over cytokine signaling duration". Presicely, it contains the imaging data for ASneo2 stimulation before and after effector addition and the smFRET with double labeled ASneo2 (E4C_K211C)</p>
Design of facilitated dissociation enables control over cytokine signaling duration - SMT raw data - neo2 - neo2 + Effector
<p>This dataset contains the raw data for the Single-molecule tracking data of the manuscript: "Design of facilitated dissociation enables control over cytokine signaling duration". Presicely, it contains the imaging data for neo2 stimulation before and after effector addition.</p>
Design of facilitated dissociation enables control over cytokine signaling duration - SMT raw data - unstimulated - calibration beads - long term tracking - labelled ligand
<p>This dataset contains the raw data for the Single-molecule tracking data of the manuscript: "Design of facilitated dissociation enables control over cytokine signaling duration". Presicely, it contains the calibration beads for all imaging experiments, the long term tracking experiments, the experiments with labelled ligand and the unstimulated probes</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.