Playground — inverse calculator

Declare variables over k bits. Write assertions. SAT finds inputs that make every assertion true. Supported ops: +-*//% ^&|~ <<>> (const rhs), and comparisons == != < <= > >=.

Templates

Factor 77 Diophantine 3x+5y=41 Mod-sqrt x² ≡ 42 (mod 101) XOR cipher Collatz antecedent Pythagorean triples c=65

Variables

forbid multiply overflow max solutions

Assertions (one per line)

Example: x * y == 1000001, x > 1, y > 1

Result

(nothing yet — pick a template or write assertions then Solve)

Built on npdollars v8 · /satlib · /dashboard · architecture
Charles Dana · Monce SAS · 2026