Elamur Research⌕
☰
home / papers / 2026 / SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs

SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs

Paper · 2026 · Yanxiao Zhao, Yaqian Li, Zihao Bo et al.

Summary

Existing logic benchmarks for LLMs offer limited control over experimental variables. Many vary only puzzle difficulty, depend on human difficulty labels, or risk training-data leakage. SATQuest addresses this with a verifier that builds reasoning tasks directly from randomly generated CNF formulas and grades answers automatically with PySAT. Tasks vary along three independent axes:

  • Instance: scale, plus solver-measured difficulty via decisions, conflicts and propagations.
  • Problem type: five SAT-derived tasks.
  • Presentation format: four logically equivalent formats.

Models answer with binary strings, which avoids JSON parsing and multiple-choice shortcuts and accepts any valid solution.

The authors evaluated open- and closed-weight LLMs in a zero-shot setting. Accuracy falls as solver-measured complexity grows, and models perform worse once problems leave familiar math notation. On hard items, models increasingly hallucinate, for example fabricating execution steps. Reinforcement fine-tuning with GRPO on the binary verifier reward improved the targeted tasks, lengthened reasoning, and carried over to larger instances. Cross-task transfer was uneven, and robustness across formats stayed weak.

The work matters because it gives a reproducible, leakage-resistant testbed for studying both LLM logical reasoning and training on it.

Key points

  • Five problem types:
    • SATDP: decision; counted correct only if both the satisfiable and unsatisfiable instances are answered correctly.
    • SATSP: finding a satisfying assignment.
    • MaxSAT.
    • MCS (minimal correction subset).
    • MUS (minimal unsatisfiable subset).
  • Four formats: Math, DIMACS, Story (OR semantics) and DualStory (AND semantics). Story and DualStory use a cookie-day narrative. Accuracy ordering is roughly Math ≥ DIMACS > Story ≈ DualStory.
  • Evaluation set sdpkjc/SATQuest: n from 3 to 16 variables, m = 4n clauses, 140 satisfiable/unsatisfiable CNF pairs.
  • Training set sdpkjc/SATQuest-RFT-3k: n from 3 to 8, clause-to-variable ratio from 2.1 to 4.0, 3,000 CNF pairs.
  • Limitations:
    • English-only synthetic narratives.
    • Only GRPO with a 0/1 reward is explored.
    • Long binary outputs can trip up smaller models' format compliance.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🏛️Chinese Academy of SciencesBeijing · China246 works · 24,951 citations🎓University of Chinese Academy of SciencesBeijing · China188 works · 8,743 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksArts and Humanities · 17,450 worksLanguage and Linguistics · 17,296 works

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 3,894 worksReasoning · 1,685 works

Cite

Cite as Yanxiao Zhao, Yaqian Li, Zihao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Lei Ren, Xiaolin Qin and Kaiwen Long. 2026. SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.acl-long.96

@inproceedings{zhao2026satquest,
  title = {{SATQuest: A Verifier for Logical Reasoning Evaluation and Reinforcement Fine-Tuning of LLMs}},
  author = {Yanxiao Zhao, Yaqian Li, Zihao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Lei Ren, Xiaolin Qin and Kaiwen Long},
  booktitle = {Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2026},
  doi = {10.18653/v1/2026.acl-long.96},
  url = {https://doi.org/10.18653/v1/2026.acl-long.96}
}

References

33 references, 17 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Gilles Audemard and Laurent Simon. 2018. On the glucose sat solver. International Journal on Artificial Intelligence Tools, 27(01):1840001. find
  2. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, and… find
  3. DeepSeek-AI, Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, and 181 others. 2025. Deepseek-r1: Incentivizing reasoning capability in ll…
  4. Aryo Pradipta Gema, Joshua Ong Jun Leang, Giwon Hong, Alessio Devoto, Alberto Carlo Maria Mancino, Rohit Saxena, Xuanli He, Yu Zhao, Xiaotang Du, Mohammad Reza Ghasemi Madani, Claire Barale, Robert McHardy, Joshua Harris, Jean Kaddour, Emile Van Krieken, and Pasquale Minervini. 2025. Are we done wit… find
  5. Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Caroline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, Olli Järviniemi, Matthew Barnett, Robert Sandler, Matej Vrzala, Jaime Sevilla, Qiuyu Ren, Elizabeth Pratt, Lionel Levine, Grant Bar… — FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI
  6. Rishi Hazra, Gabriele Venturato, Pedro Zuidberg Dos Martires, and Luc De Raedt. 2025. Have large language models learned to reason? a characterization via 3-sat phase transition. Preprint, arXiv:2504.03930. — [arXiv:2504.03930](https://arxiv.org/abs/2504.03930) find
  7. Yun He, Di Jin, Chaoqi Wang, Chloe Bi, Karishma Mandyam, Hejia Zhang, Chen Zhu, Ning Li, Tengyu Xu, Hongjiang Lv, Shruti Bhosale, Chenguang Zhu, Karthik Abinav Sankararaman, Eryk Helenowski, Melanie Kambadur, Aditya Tayade, Hao Ma, Han Fang, and Sinong Wang. 2024. Multi-if: Benchmarking llms on mult… — [arXiv:2410.15553](https://arxiv.org/abs/2410.15553) find
  8. Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. 2021a. Measuring massive multitask language understanding. In International Conference on Learning Representations.
  9. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021b. Measuring mathematical problem solving with the MATH dataset. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 2).
  10. Shulin Huang, Linyi Yang, Yan Song, Shuang Chen, Leyang Cui, Ziyu Wan, Qingcheng Zeng, Ying Wen, Kun Shao, Weinan Zhang, Jun Wang, and Yue Zhang. 2025. Thinkbench: Dynamic out-of-distribution evaluation for robust llm reasoning. Preprint, arXiv:2502.16268. — [arXiv:2502.16268](https://arxiv.org/abs/2502.16268) find
  11. Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. 2019. Rc2: an efficient maxsat solver. Journal on Satisfiability, Boolean Modelling and Computation, 11(1):53–64. find
  12. Mehran Kazemi, Bahare Fatemi, Hritik Bansal, John Palowitch, Chrysovalantis Anastasiou, Sanket Vaibhav Mehta, Lalit K. Jain, Virginia Aglietti, Disha Jindal, Peter Chen, Nishanth Dikkala, Gladys Tyen, Xin Liu, Uri Shalit, Silvia Chiappa, Kate Olszewska, Yi Tay, Vinh Q. Tran, Quoc V. Le, and Orhan Fi… — BIG-Bench Extra Hard
  13. Bill Yuchen Lin, Ronan Le Bras, Kyle Richardson, Ashish Sabharwal, Radha Poovendran, Peter Clark, and Yejin Choi. 2025. Zebralogic: On the scaling limits of llms for logical reasoning. Preprint, arXiv:2502.01100.
  14. Joao Marques-Silva. 2010. Minimal unsatisfiability: Models, algorithms and applications (invited paper). In Proceedings of the 2010 40th IEEE International Symposium on Multiple-Valued Logic, ISMVL ’10, page 9–14, USA. IEEE Computer Society. find
  15. Carlos Mencía, Alessandro Previti, and Joao Marques-Silva. 2015. Literal-based mcs extraction. In Proceedings of the 24th International Conference on Artificial Intelligence, IJCAI’15, page 1973–1979. AAAI Press. find
  16. Philipp Mondorf and Barbara Plank. 2024. Liar, liar, logical mire: A benchmark for suppositional reasoning in large language models. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 7114–7137, Miami, Florida, USA. Association for Computational Linguist… find
  17. OpenAI. 2025. OpenAI o3-mini System Card. https://cdn.openai.com/ Accessed: o3-mini-system-card-feb10.pdf. 2025-04-22. ↗
  18. OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, and 262 others.… — GPT-4 Technical Report
  19. David Rein, Betty Li Hou, Asa Cooper Stickland, Jackson Petty, Richard Yuanzhe Pang, Julien Dirani, Julian Michael, and Samuel R. Bowman. 2024. GPQA: A graduate-level google-proof q&a benchmark. In First Conference on Language Modeling.
  20. Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. 2019. Learning a SAT solver from single-bit supervision. In International Conference on Learning Representations.
  21. Zhihong Shao and et al. 2024. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300.
  22. Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowycz, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexander W. Kocurek, Ali Safaya, Ali Tazarv, an… — Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models
  23. Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung, Aakanksha Chowdhery, Quoc Le, Ed Chi, Denny Zhou, and Jason Wei. 2023. Challenging BIG-bench tasks and whether chain-of-thought can solve them. In Findings of the Association for Computational Linguistics: A…
  24. Neel Jain, Khalid Saifullah, Sreemanti Dey, Shubh-Agrawal, Sandeep Singh Sandha, Siddartha Venkat Naidu, Chinmay Hegde, Yann LeCun, Tom Goldstein, Willie Neiswanger, and Micah Goldblum. 2025. Livebench: A challenging, contamination-limited LLM benchmark. In The Thirteenth International Conference on… find
  25. Chulin Xie, Yangsibo Huang, Chiyuan Zhang, Da Yu, Xinyun Chen, Bill Yuchen Lin, Bo Li, Badih Ghazi, and Ravi Kumar. 2024. On memorization of large language models in logical reasoning. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24.
  26. Tian Xie, Zitian Gao, Qingnan Ren, Haoming Luo, Yuqian Hong, Bryan Dai, Joey Zhou, Kai Qiu, Zhirong Wu, and Chong Luo. 2025. Logic-rl: Unleashing llm reasoning with rule-based reinforcement learning. Preprint, arXiv:2502.14768.
  27. Tong Yu, Yongcheng Jing, Xikun Zhang, Wentao Jiang, Wenjie Wu, Yingjie Wang, Wenbin Hu, Bo Du, and Dacheng Tao. 2025. Benchmarking reasoning robustness in large language models. Preprint, arXiv:2503.04550. — [arXiv:2503.04550](https://arxiv.org/abs/2503.04550) find
  28. P Team, Xinrun Du, Yifan Yao, Kaijing Ma, Bingli Wang, Tianyu Zheng, King Zhu, Minghao Liu, Yiming Liang, Xiaolong Jin, Zhenlin Wei, Chujie Zheng, Kaixin Deng, Shawn Gavin, Shian Jia, Sichao Jiang, Yiyan Liao, Rui Li, Qinrui Li, and 78 others. 2025. Supergpqa: Scaling llm evaluation across 285 gradu…
  29. Qwen Team. 2024. Qwq: Reflect deeply on the boundaries of the unknown. find
  30. Leandro von Werra, Younes Belkada, Lewis Tunstall, Edward Beeching, Tristan Thrush, Nathan Lambert, Shengyi Huang, Kashif Rasul, and Quentin Gallouédec. 2020. Trl: Transformer reinforcement learning. https://github.com/huggingface/trl. ↗
  31. Yubo Wang, Xueguang Ma, Ge Zhang, Yuansheng Ni, Abhranil Chandra, Shiguang Guo, Weiming Ren, Aaran Arulraj, Xuan He, Ziyan Jiang, Tianle Li, Max Ku, Kai Wang, Alex Zhuang, Rongqi Fan, Xiang Yue, and Wenhu Chen. 2024. MMLU-pro: A more robust and challenging multi-task language understanding benchmark…
  32. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed H. Chi, Quoc V Le, and Denny Zhou. 2022. Chain of thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems.
  33. Colin White, Samuel Dooley, Manley Roberts, Arka Pal, Benjamin Feuer, Siddhartha Jain, Ravid Shwartz-Ziv, find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhao-2026-satquest-verifier-logical-reasoning-evaluation/