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

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

Constraint solving vs Abstract interpretation

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

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

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

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

Recover ARM64 returns and bounded state transitions, compare edits, and export portable C in a local workbench.

Generic search, optimization, and constraint-solving building blocks for Rust

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.

SAT-based Sudoku solver using CNF encoding and Z3 theorem prover. Supports 9×9 and 16×16 puzzles.

Générateur procédural local de plans de principe 2D sous contraintes.