HabrJun 9

Не квантовый компьютер, но уже полезно: обзор AGIQ Solver Enterprise как GPU‑решателя для тяжёлых задач оптимизации

На рынке софта для оптимизации есть две крайности. С одной стороны — академические и промышленные решатели, которые невероятно мощны, но часто требуют либо очень аккуратной постановки, либо серьёзной экспертизы, либо терпения. С другой — бесконечный поток «революционных» продуктов, которые обещают всё, а в реальности оказываются очередной метаэвристикой с красивым лендингом. На этом фоне AGIQ Solver Enterprise оказывается любопытным кейсом. Не потому, что это «магия на видеокарте» или «квантовый компьютер для бедных», а потому что продукт пытается занять вполне конкретную нишу: быстрый поиск хороших решений в сложных булевых и оптимизационных задачах за счёт GPU и квантово-вдохновлённой логики поиска . Ниже — разбор, что это вообще такое, где оно действительно может пригодиться, почему здесь вообще всплывает слово «квантовый», и как с этим работать на практике.

https://habr.com/ru/articles/1045440/

#AGIQ_Solver_Enterprise #GPUвычисления #квантововдохновлённые_алгоритмы #оптимизация #MaxSAT #SAT_solver #GPGPU #параллельные_вычисления #булева_оптимизация #комбинаторные_задачи

Не квантовый компьютер, но уже полезно: обзор AGIQ Solver Enterprise как GPU‑решателя для тяжёлых задач оптимизации

На рынке софта для оптимизации есть две крайности. С одной стороны — академические и промышленные решатели, которые невероятно мощны, но часто требуют либо очень аккуратной постановки, либо серьёзной...

Хабр
José A. AlonsoMay 11, 2024
Lecturas compartidas el 10 de mayo de 2024. https://jalonso.substack.com/lecturas-compartidas-el-10-de-mayo #ITP #Lean4 #IsabelleHOL #SAT_solver #FunctionalProgramming #Haskell #Python #Math
Lecturas compartidas el 10 de mayo de 2024

#ITP #Lean4 #IsabelleHOL #SAT_solver #FunctionalProgramming #Haskell #Python #Math

J.A. Alonso - Newsletter
José A. AlonsoMay 10, 2024
Verifying a SAT solver from ground up. ~ Mathias Fleury. https://youtu.be/-NTodQdAjgQ #ITP #IsabelleHOL #SAT_solver
Mathias Fleury: Verifying a SAT solver from ground up

YouTube
José A. AlonsoFeb 5, 2024
SATurn: SAT Solver-prover in lean 4. ~ Siddhartha Gadgil. https://github.com/siddhartha-gadgil/Saturn #ITP #LeanProver #Lean4 #SAT_Solver
GitHub - siddhartha-gadgil/Saturn: Experiments with SAT solvers with proofs in Lean 4

Experiments with SAT solvers with proofs in Lean 4 - GitHub - siddhartha-gadgil/Saturn: Experiments with SAT solvers with proofs in Lean 4

GitHub
José A. AlonsoAug 20, 2023
No order-10 projective planes via SAT. ~ David Michael Roberts (@highergeometer). https://thehighergeometer.wordpress.com/2023/08/09/no-order-10-projective-planes-via-sat/ #SAT_solver #Math
No order-10 projective planes via SAT

The proof that there is no finite projective plane of “order 10” (namely, one with 9 points per line) was a gory and large multi-part computation. The last phase, on a CRAY supercompute…

theHigherGeometer
José A. AlonsoAug 16, 2023
EduSAT: A pedagogical tool for theory and applications of boolean satisfiability. ~ Yiqi Zhao, Ziyan An, Meiyi Ma, Taylor Johnson. https://arxiv.org/abs/2308.07890 #Logic #SAT_Solver #SMT
EduSAT: A Pedagogical Tool for Theory and Applications of Boolean Satisfiability

Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) are widely used in automated verification, but there is a lack of interactive tools designed for educational purposes in this field. To address this gap, we present EduSAT, a pedagogical tool specifically developed to support learning and understanding of SAT and SMT solving. EduSAT offers implementations of key algorithms such as the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and the Reduced Order Binary Decision Diagram (ROBDD) for SAT solving. Additionally, EduSAT provides solver abstractions for five NP-complete problems beyond SAT and SMT. Users can benefit from EduSAT by experimenting, analyzing, and validating their understanding of SAT and SMT solving techniques. Our tool is accompanied by comprehensive documentation and tutorials, extensive testing, and practical features such as a natural language interface and SAT and SMT formula generators, which also serve as a valuable opportunity for learners to deepen their understanding. Our evaluation of EduSAT demonstrates its high accuracy, achieving 100% correctness across all the implemented SAT and SMT solvers. We release EduSAT as a python package in .whl file, and the source can be identified at https://github.com/zhaoy37/SAT_Solver.

arXiv.org
José A. AlonsoMay 17, 2023
Satisfiability-aided language models using declarative prompting. ~ Xi Ye, Qiaochu Chen, Isil Dillig, Greg Durrett. https://arxiv.org/abs/2305.09656 #LLMs #SAT_Solver
SatLM: Satisfiability-Aided Language Models Using Declarative Prompting

Prior work has combined chain-of-thought prompting in large language models (LLMs) with programmatic representations to perform effective and transparent reasoning. While such an approach works well for tasks that only require forward reasoning (e.g., straightforward arithmetic), it is less effective for constraint solving problems that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of LLMs. We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. This approach has two key advantages. The declarative specification is closer to the problem description than the reasoning steps are, so the LLM can parse it out of the description more accurately. Furthermore, by offloading the actual reasoning task to an automated theorem prover, our approach can guarantee the correctness of the answer with respect to the parsed specification and avoid planning errors in the solving process. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm. In particular, SATLM outperforms program-aided LMs by 23% on a challenging subset of the GSM arithmetic reasoning dataset; SATLM also achieves a new SoTA on LSAT and BoardgameQA, surpassing previous models that are trained on the respective training sets.

arXiv.org
José A. AlonsoMar 29, 2023
Generating extended resolution proofs with a BDD-based SAT solver. ~ Randal E. Bryant, Marijn J. H. Heule. https://arxiv.org/abs/2105.00885 #Logic #ATP #SAT_Solver
Generating Extended Resolution Proofs with a BDD-Based SAT Solver

In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability for a set of clauses. Such a proof indicates that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a BDD-based solver, implemented by modifying an existing BDD package, to several challenging Boolean satisfiability problems. Our resultsdemonstrate scaling for parity formulas, as well as the Urquhart, mutilated chessboard, and pigeonhole problems far beyond that of other proof-generating SAT solvers.

arXiv.org