Artifact for the AAAI 2025 paper "Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization"

<p dir="ltr">Artifact for the AAAI 2025 paper "Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization". </p><p dir="ltr">This repository contains the artifact of the tool "QuantiSAT" introduced in the paper titled "Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization". For more information on how to build/run the tool, please refer to the readme file.<br></p><b>quanti-sat</b><p dir="ltr"><i>New Quantifier Elimination Techniques for SMT Solvers</i></p><h2><b>Quick Start</b></h2><h3>1. Install dependencies</h3><p dir="ltr">We recommend using Python <b>3.11</b> in a virtual environment.<br>Install the required packages with:</p><pre><pre>pip install -r requirements.txt<br></pre></pre><h3>2. Install <code>cvc5</code></h3><p dir="ltr">Some baselines (including <code>cvc5</code>) require the command-line tool <code>cvc5</code>.<br>Installation instructions can be found here:<br><a href="https://cvc5.github.io/docs/cvc5-1.0.0/installation/installation.html" rel="noopener" target="_new">https://cvc5.github.io/docs/cvc5-1.0.0/installation/installation.html</a></p><h3>3. Prepare input formulas</h3><p dir="ltr">Add CNF formulas and their negations to the <code>examples/</code> directory.</p><h3>4. Run the solver</h3><p dir="ltr">Example command:</p><pre><pre>python3 main.py \<br> --file_pos examples/polysynth_cnf/archimedes.c.smt2 \<br> --file_neg examples/polysynth_cnf_neg/archimedes.c.smt2 \<br> --solver QUANTISAT \<br> --config configs/farkas-z3.json \<br> --degree 0 \<br> --verbose RESULT_FORMULA_MODEL \<br> --timeout 5<br></pre></pre><h2><b>Run Experiments</b></h2><p dir="ltr">We originally used an HPC cluster to parallelize experiments.<br>To run all experiments locally (sequentially), use:</p><pre><pre>./run_all.sh<br></pre></pre><p></p>