This repository contains the artifact for the paper:

Evaluating Satisfiability Solving with LLMs

The artifact is designed to support reproducibility for the paper. It provides implementations for:

• CNF generation
• paired-CNF generation
• LLM API invocation for obtaining model predictions
• traditional evaluation metrics
• the proposed Accurate Differentiation Rate (ADR)
• cross-representation reductions to Vertex Cover and discrete 3D packing
• deterministic witness validation for assignments, covers, and packing outputs

In addition, the artifact contains plotting scripts, aggregated intermediate files, selected prediction-result directories, prompts, and appendix-related supplementary materials needed to reproduce the main findings of the paper. The experiments cover:

• random 3-SAT phase-transition analysis,
• LLM performance on low-(\alpha) UNSAT CNFs,
• paired SAT/UNSAT evaluation with ADR,
• 2-SAT as a controlled baseline,
• cross-representation evaluations on Vertex Cover and discrete 3D packing.

This artifact supports two levels of reproducibility.

Most figures in the paper and appendix can be regenerated directly from prepared intermediate .xlsx files. This is the recommended path for artifact evaluation.

For several experiments, we also provide prediction-result directories and solver-result directories that were used to construct the aggregated summaries. This path provides greater provenance and traceability.

The repository also includes scripts for:

• generating SAT / UNSAT instances,
• generating paired instances,
• invoking commercial LLM APIs,
• parsing predictions,
• validating witnesses,
• recomputing metrics.

To regenerate the main figures directly from prepared intermediate files:

python reproduce_all_figures.py

This is the fastest way to verify the main empirical claims of the paper.

Create a Python environment and install dependencies:

pip install pandas numpy matplotlib openpyxl openai anthropic requests python-sat tqdm

If your local environment already includes some of these packages, you may omit them as needed.

The quick path reproduces the paper’s visual results from prepared intermediate artifacts, including:

• the classical 3-SAT phase-transition baseline,
• low-(\alpha) UNSAT detection trends,
• paired-formula evaluation with ADR,
• 2-SAT paired evaluation,
• cross-representation plots for Vertex Cover and 3D packing.

This section describes the repository structure following the experimental flow of the paper.

This directory serves as the experimental baseline, corresponding to Figure 1(a).

• Functionality: invokes a standard CDCL SAT solver on CNF instances.

• Purpose:

  • reproduces the classical 3-SAT phase transition,
  • measures satisfiability probability and search hardness,
  • provides the algorithmic baseline used to contrast LLM behavior.

1. Figure 1(a) generation script
   The workflow for Figure 1(a), including input generation, CDCL conflict-count computation, and phase-transition plotting, is implemented in:

   Code/invoke_traditional_methond/phase_transition/phase_transition_generate_and_draw_Minisat22_only_draw_median.py
   

These directories contain the core LLM evaluation pipelines supporting Figure 1(b), Figure 2, and related appendix materials.

• Functionality:

  • constructs prompts,
  • sends inference requests,
  • parses model outputs,
  • stores prediction results,
  • computes metrics.

• Metrics:

  • Accuracy
  • Precision / Recall / F1
  • MCC
  • ADR

The pipelines for reproducing Figure 1(b) are organized by model provider.

1. Input directories
   Input CNF instances are stored in directories matching:

   ^Code/invoke_openai/unsat_figure_1b/unsat_cnf_low_alpha_N_[0-9]{1,2}$

2. LLM invocation script The script used to query OpenAI models is:

   Code/invoke_openai/unsat_figure_1b/invoke_openai_predict_low_alpha_unsat_openai_1.0.0_multiple_model.py
   

3. Prediction output directories Model predictions are written to directories matching:

   ^Code/invoke_openai/unsat_figure_1b/unsat_cnf_low_alpha_N_[0-9]{1,2}_openai_prediction_{LLM_name}$

4. Accuracy / correct-rate computation The script used to compute the correct rates needed for Figure 1(b) is:

   Code/invoke_openai/unsat_figure_1b/calculate_accuracy.py
   

1. Input directories Input CNF instances are stored in directories matching:

   ^Code/invoke_deepseek/unsat_cnf_low_alpha_N_[0-9]{1,2}$

2. LLM invocation script The script used to query DeepSeek models is:

   Code/invoke_deepseek/invoke_deepseek_predict_low_alpha_unsat.py
   

3. Prediction output directories Model predictions are written to directories matching:

   ^Code/invoke_deepseek/unsat_cnf_low_alpha_N_[0-9]{1,2}_deepseek_prediction_{LLM_name}$

4. Accuracy / correct-rate computation The script used to compute the correct rates needed for Figure 1(b) is:

   Code/invoke_deepseek/calculate_accuracy.py
   

1. Input directories Input CNF instances are stored in directories matching:

   ^Code/invoke_anthropic/unsat_cnf_low_alpha_N_[0-9]{1,2}$

2. LLM invocation script The script used to query Anthropic models is:

   Code/invoke_anthropic/invoke_anthropic_predict_low_alpha_unsat.py
   

3. Prediction output directories Model predictions are written to directories matching:

   ^Code/invoke_anthropic/unsat_cnf_low_alpha_N_[0-9]{1,2}_anthropic_prediction_{LLM_name}$

4. Accuracy / correct-rate computation The script used to compute the correct rates needed for Figure 1(b) is:

   Code/invoke_anthropic/calculate_accuracy.py
   

"Code/SAT_Draw_Figure/draw_curve_unsat.py"

The pipeline for reproducing Figure 2 is organized as follows.

1. LLM input data
   The CNF inputs used in this experiment are stored in:

   Code/invoke_openai/cnf_results_openai_o1
   

2. LLM invocation scripts The scripts used to query different model families are:

   • OpenAI models

     Code/invoke_openai/invoke_openai_draw_3_curve_multi_models.py
     

   • DeepSeek models

     Code/invoke_openai/invoke_deepseek_predict.py
     

   • Anthropic models

     Code/invoke_openai/invoke_anthropic_predict.py
     

3. Prediction outputs The prediction results produced by the LLMs are written to directories of the form:

   Code/invoke_openai/cnf_results_openai_o1_input_based_{LLM_name}
   

4. Second-part data collection To collect the results for the second part of the experiment, the corresponding scripts with the same filenames should also be run under:

   invoke_openai/draw_o1_phase_transition_figure
   

5. Metric computation and intermediate summaries The scripts used to compute traditional metrics, ADR, and intermediate summary files are:

   Code/invoke_openai/invoke_openai_draw_3_curve_step4_merger_different_models_3_Multiply_3.py
   

   and

   Code/invoke_openai/merge_two_kinds_of_dataset.py
   

6. Plotting Figure 2 The final script used to generate Figure 2 from the intermediate files is:

   invoke_openai/merge_two_kinds_of_dataset_plot_from_intermediate_file.py
   

This directory implements the 3-SAT paired-evaluation workflow used for Figure 3.

• Functionality:

  • generates hard 3-SAT CNFs,
  • constructs minimally modified SAT/UNSAT counterparts,
  • stores paired inputs,
  • evaluates model discrimination using ADR.

The pipeline for reproducing Figure 3 is organized as follows.

1. Generate paired 3-SAT CNF inputs
   The following script is used to generate paired CNF instances for the 3-SAT experiments:

   Code/fix_cnf/fix_cnf_method_2_remove_mul_minimum_clause.py
   

2. Location of the generated pair inputs The generated paired inputs are stored in:

   Code/fix_cnf/pairs_input
   

   These files correspond to the same paired inputs used in directories of the form:

   Code/fix_cnf/fixed_set_mul_N/unsat_cnf_low_alpha_N_{N}_openai_prediction_o1
   

3. Invoke LLMs to obtain predictions The scripts used to query LLMs and collect prediction results are:

   • DeepSeek models

     Code/fix_cnf/invoke_deepseek_predict_fixed_set_mul_N.py
     

   • OpenAI models

     Code/fix_cnf/invoke_openai_predict_fixed_set_mul_N.py
     

4. Location of prediction results The prediction outputs are stored in directories of the following forms:

   • OpenAI prediction results

     Code/fix_cnf/fixed_set_mul_N/unsat_cnf_low_alpha_N_{N}_openai_prediction_o1_openai_prediction_{model_selected}
     

   • DeepSeek prediction results

     Code/fix_cnf/fixed_set_mul_N/unsat_cnf_low_alpha_N_{N}_openai_prediction_o1_deepseek_prediction_{model_selected}
     

5. Metric computation The following script is used to compute traditional evaluation metrics together with ADR:

   Code/fix_cnf/calculate_3_ways_evaluation.py
   

6. Plotting Figure 3 The following script is used to generate Figure 3:

   Code/SAT_Draw_Figure/draw_curve_pairs.py
   

This directory implements the 2-SAT paired-evaluation workflow used for Figure 4.

• Functionality:

  • generates 2-SAT instances,
  • creates paired SAT/UNSAT variants,
  • evaluates traditional metrics and ADR,
  • compares 2-SAT performance against 3-SAT.

The pipeline for reproducing Figure 4 is organized as follows.

1. Generate UNSAT 2-SAT CNFs
   The following script is used to generate UNSAT 2-SAT instances:

   CNF2/generate/CNF2_generate_and_draw_Minisat22.py
   

2. Minimally repair each UNSAT 2-SAT formula After generating the UNSAT 2-SAT instances, a minimal-repair step is applied to construct the corresponding SAT counterparts, thereby forming paired 2-SAT instances.

   CNF2/generate/fix_cnf_method_2_remove_mul_minimum_clause.py
   

3. Storage location for generated and repaired instances The results of the generation and minimal-repair steps are stored in:

   Code/CNF2/generate/cnf_results_CDCL
   

4. Invoke OpenAI, DeepSeek, and Anthropic models The scripts used to query the three model families are:

   • Anthropic models

     C:\Research\Vulnerability\FSE\Satisfiability_Solvers\Code\CNF2\invoke\invoke_anthropic_predict_2SAT.py
     

   • DeepSeek models

     CNF2/invoke/invoke_deepseek_predict_2SAT.py
     

   • OpenAI models

     CNF2/invoke/invoke_openai_predict_2SAT.py
     

5. Prediction outputs The prediction results produced by the LLMs are stored in:

   CNF2/generate/cnf_results_CDCL/prediction_result
   

6. Metric computation The scripts used to compute the traditional metrics and ADR are:

   CNF2/invoke/calculate_3_ways_evaluation.py
   

   and

   CNF2/invoke/calculate_accuracy.py
   

7. Plotting Figure 4 The script used to generate Figure 4, which shows the values and trends of multiple metrics on paired 2-SAT instances, is:

   SAT_Draw_Figure/draw_curve_2sat.py
   

This directory implements the CNF-to-Vertex-Cover reduction used in the cross-representation experiments.

• Functionality:

  • converts CNF formulas into graph instances,
  • invokes LLMs on the resulting Vertex Cover tasks,
  • validates returned covers with a deterministic checker,
  • compares decisions and correctness across representations.

The pipeline for reproducing Appendix Figure 1 is organized as follows.

1. Input paired CNF instances
   The paired CNF inputs used in this experiment are stored in:

   Code/fix_cnf/pairs_input
   

2. Convert paired CNFs to Vertex Cover instances The following script is used to convert the paired CNF instances into Vertex Cover instances:

   convert_cnf_to_vertex_cover/convert_cnf_to_vertex_cover_method_2.py
   

3. Location of converted Vertex Cover instances The converted results are stored in:

   Code/convert_cnf_to_vertex_cover/vertex_cover_graph
   

4. Invoke LLMs on the converted Vertex Cover instances The following scripts are used to query LLMs on the Vertex Cover representations and collect their predictions on whether the original instance is SAT or UNSAT:

   • OpenAI models

     convert_cnf_to_vertex_cover/convert_cnf_to_vertex_cover_method_1.py
     

   • DeepSeek models

     convert_cnf_to_vertex_cover/convert_cnf_to_vertex_cover_method_1_invoke_deepseek.py
     

   The corresponding prediction results are stored in:

   Code/convert_cnf_to_vertex_cover/vertex_cover_graph
   

5. Metric computation The following script is used to compute traditional evaluation metrics together with ADR:

   convert_cnf_to_vertex_cover/calculate_3_ways_evaluation.py
   

6. Plotting Appendix Figure 1 The following script is used to generate Appendix Figure 1:

   SAT_Draw_Figure/draw_curve_vertex_cover.py
   

This directory implements the CNF-to-discrete-3D-packing reduction used in the cross-representation experiments.

• Functionality:

  • converts CNF formulas into discrete packing instances,
  • invokes LLMs using structured prompts,
  • validates returned packing witnesses,
  • compares decision consistency and correctness across representations.

The pipeline for reproducing Appendix Figure 2 is organized as follows.

1. Input paired CNF instances
   The paired CNF inputs used in this experiment are stored in:

   Code/fix_cnf/pairs_input
   

2. Convert paired CNFs to discrete 3D packing instances The following script is used to convert the paired CNF instances into discrete 3D packing instances:

   Code/convert_cnf_to_3D_packing/convert_cnf_to_3D_packing_method.py
   

3. Location of converted 3D packing instances The converted results are stored in:

   Code/convert_cnf_to_3D_packing/cnf_to_3D_packing
   

4. Invoke LLMs on the converted 3D packing instances The following scripts are used to query LLMs on the 3D packing representations and collect their predictions on whether the original instance is SAT or UNSAT:

   • OpenAI models

     Code/convert_cnf_to_3D_packing/convert_cnf_to_3D_packing_method_gpt_5.py
     

   • DeepSeek models

     Code/convert_cnf_to_3D_packing/convert_cnf_to_3D_packing_method_deepseek.py
     

   • DeepSeek-Reasoner models

     Code/convert_cnf_to_3D_packing/convert_cnf_to_3D_packing_method_deepseek_reasoner.py
     

   The corresponding prediction results are stored in:

   Code/convert_cnf_to_3D_packing/cnf_to_3D_packing
   

5. Metric computation The following script is used to compute traditional evaluation metrics together with ADR:

   Code/convert_cnf_to_3D_packing/calculate_3_ways_evaluation.py
   

6. Plotting Appendix Figure 2 The following script is used to generate Appendix Figure 2:

   Code/SAT_Draw_Figure/draw_3d_packing.py
   

This directory contains the plotting utilities used to generate publication-quality figures.

• Functionality:

  • loads aggregated intermediate results,
  • renders the figures used in the paper and appendix,
  • standardizes fonts, legends, axis ranges, and visual formatting.

The paper includes multiple experimental settings, each with its own instance-construction protocol. This repository supports both direct reuse of prepared data and regeneration from scripts.

This setting corresponds to the initial experiment on traditional metrics.

• Fixed variable count:

  • (N = 75)

• Clause-density values:

  • (\alpha \in {3.5, 4.0, 4.5, 5.0, 5.5})

• For each (\alpha), the experiment uses multiple randomly generated 3-SAT instances verified by a classical SAT solver.

This setting probes whether LLMs can detect UNSAT instances when satisfiable instances usually dominate.

• Variable counts:

  • (N \in {5, 8, 10, 25, 50, 60, 70, 80, 90, 100, 110, 120, 140})

• Clause-density values:

  • (\alpha \in {3.5, 3.6, 3.7, 3.8, 3.9, 4.0})

• All instances in this setting are solver-verified UNSAT formulas.

For each UNSAT formula, the artifact constructs a near-identical SAT counterpart using a minimal edit, such as:

• deleting one clause,
• flipping the polarity of one literal,
• replacing one literal with another.

These pairs are used to evaluate ADR, which requires simultaneous correctness on both members of a pair.

The repository also provides generation and evaluation pipelines for paired 2-SAT instances, enabling comparison between a polynomial-time SAT fragment and the harder 3-SAT case.

The repository includes reduced instances for:

• Vertex Cover
• discrete 3D packing

These are derived from SAT instances and are used to study representation-invariant reasoning.

If you want to rerun generation yourself, please use the corresponding scripts inside:

• invoke_traditional_methond
• fix_cnf
• CNF2
• convert_cnf_to_vertex_cover
• convert_cnf_to_3D_packing

To rerun commercial-model inference, set the required API keys in your shell environment before execution.

Example:

export OPENAI_API_KEY="your_openai_key"
export ANTHROPIC_API_KEY="your_anthropic_key"
export DEEPSEEK_API_KEY="your_deepseek_key"

Depending on your local scripts, you may also choose to place these values in a .env file or in provider-specific configuration files.

The LLMs evaluated in this paper are closed-source commercial models. Reproducing all model calls therefore requires paid API access. For this reason, the default artifact workflow focuses on reproducing results from prepared intermediate files rather than rerunning all LLM calls.

• Python 3.10 or newer
• Linux, macOS, or Windows

The artifact depends on two classes of packages: core packages and API packages.

These are used for data generation, metric computation, validation, and plotting:

• pandas
• numpy
• matplotlib
• openpyxl
• python-sat
• tqdm

These are used for invoking commercial LLM services:

• openai
• anthropic
• requests

Install all required packages with:

pip install scikit-learn, pandas numpy matplotlib openpyxl openai anthropic requests python-sat tqdm

Because the evaluated LLMs are commercial models, the default workflow focuses on reproducing results from the provided intermediate files and processed outputs.

python reproduce_all_figures.py

• Plotting code: Code/invoke_traditional_methond/phase_transition/phase_transition_generate_and_draw_Minisat22_only_draw_median.py
• Prediction / solver results: Code/invoke_traditional_methond/phase_transition/cnf_results_CDCL
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/phase_transition/figures_CDCL_phase_transition/Random_3-SAT_CDCL_N_75_median.png

• Aggregated intermediate data: Code/Analysis_Result_Collection/SAT_figures.xlsx
• Plotting code: Code/SAT_Draw_Figure/draw_curve_unsat.py
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/unsat/unsat_small_alpha_prediction_correct_rate.png

• Aggregated intermediate data: Analysis_Result_Collection/Figure_in_paper/LLMs_phase_transition/combined_metrics/combined_metrics_by_model_alpha.xlsx
• Plotting code: Code/invoke_openai/merge_two_kinds_of_dataset_plot_from_intermediate_file.py
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/LLMs_phase_transition/combined_metrics/combined_metrics_4x3.png

• Aggregated intermediate data: Code/Analysis_Result_Collection/SAT_figures.xlsx
• Plotting code: Code/SAT_Draw_Figure/draw_curve_pairs.py
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/pairs/pairs_small_alpha_prediction_correct_rate_3x3_only.png

• Aggregated intermediate data: Code/Analysis_Result_Collection/SAT_figures.xlsx
• Plotting code: Code/SAT_Draw_Figure/draw_curve_2sat.py
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/2SAT/2SAT_3x3_only.png

• Aggregated intermediate data: Code/Analysis_Result_Collection/SAT_figures.xlsx
• Plotting code: Code/SAT_Draw_Figure/draw_curve_vertex_cover.py
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/Vertex_Cover/Vertex_Cover_legend_in_last_panel.png

• Aggregated intermediate data: Code/Analysis_Result_Collection/SAT_figures.xlsx
• Plotting code: Code/SAT_Draw_Figure/draw_3d_packing.py
• Saved Figure path: Analysis_Result_Collection/Figure_in_paper/3d_packing/packing_pred_llm_yes_3x3.png