constraint-solving

A webassembly wrapper for FreeCAD's 2D geometric solver.

Turns natural-language requirements into executable Python software, tests it in isolation, and packages only independently validated builds.

An implementation of miniKanren which provides support for Constraint Handling Rules (CHR)

A high-performance, custom-rendered FMX component for Delphi that provides a fluid, physics-based list interface. Built entirely on the Skia4Delphi graphics pipeline, it breaks away from traditional UI constraints to deliver a smooth, modern, and highly interactive user experience.

在麦当劳 MCP 真实菜单里做套餐轮次级求解 —— 140 种组合本地枚举，只调 3 次接口。实测热量 -40%，价格经官方接口验证。

三维扫雷迷宫：在三维雷区中寻路，结合约束推理与风险可视化。

An interactive 3D story world where a deterministic engine verifies ways to keep a chosen moment after conditions change.

Universal dependency resolver using SAT solvers - works for software packages, course prerequisites, books, certifications, and any system with logical dependencies

Unique-solution Kakuro puzzle generator with configurable difficulty, deterministic generation, SQLite persistence, multiprocessing and print-ready PDF booklet export.

C³: Calculus of Constrained Constructions. Sovereign alternative to SMT/Haskell from first principles. Menhir · Rascal · Scala 3 · Dex · Aldor · MPL.

A pure-Julia SMT-LIB 2 interface for building constraints, checking satisfiability, retrieving models and working incrementally with solvers such as Z3, CVC5, Yices and MathSAT.

A puzzle game where solutions are cryptographically verified - prove your work, literally.

Interactive symbolic execution plugin for Ghidra, powered by angr + Z3. Solve constraints, crack passwords, reverse algorithms — right from the Ghidra UI.

Constraint solving vs Abstract interpretation

Practical Z3 resources for the mathematics and verification communities.

This repository contains projects and assignments completed for the Constraint Solving course at KU Leuven.

紧箍咒：给大模型套上的状态机与逻辑沙盒。AI 穷举 + 系统剪枝 = 可审计的因果推演树。

SATzillaX is a high-performance CDCL SAT Solver built in C++17 featuring Two-Watched Literals, VSIDS branching heuristic, Phase Saving, Clause Learning, Non-Chronological Backtracking, and Geometric Restarts.

Certified frame-first SAT middleware — decide structured regions (2-SAT · GF(2) parity · counting) before CDCL, and independently verify every verdict (model replay · DRAT). A research harness for where SAT hardness lives.

A CDCL SAT solver written in OCaml. The solver reads standard DIMACS CNF files and applies watched literals, clause learning, and restarts. A Sudoku encoder turns puzzles into CNF as a demo. The test suite checks every reported model with an independ