klause

klause

Used in: combo.

Klause is a Kotlin constraint programming library. Variables are bounded integers, Booleans, floats bucketed to integers, nominals one-hot encoded as Booleans, and sets over either an int range or a nominal universe. Any variable can be declared optional, with constraints automatically lowered to reified or aggregation-aware forms. The DSL covers arithmetic, logic, comparisons, and a wide catalogue of global constraints: allDifferent, cumulative, circuit, binPacking, table, regular, mdd, network flow, and the rest of the usual CP toolkit. MiniZinc models can target klause as a backend through klause-mzn-lib.

Two native engines back the same Solver and Optimizer surface. A complete CSP backtrack engine is the default, with propagation, configurable variable and value heuristics, branch-and-bound optimisation, and model-blocking enumeration; reach for it when you need proofs of unsat, optimal bounds, or without-replacement enumeration. A local-search engine (adaptive probSAT by default, with WalkSat, DDFW, simulated annealing, and CCA variants available) covers stochastic sampling and large-domain problems where complete search runs out of budget.

Sampling is first-class. Drawing with replacement and enumerating without replacement are core operations rather than afterthoughts, so the same compiled problem serves repeated, diverse, incremental queries against one model. Optional adapter modules send the same problem to external solvers when useful: klause-logicng for bit-blasted SAT, klause-smt for SMT-LIB backends. Klause is not a MILP solver (integer-only objectives), not a full SMT solver (no bitvectors, arrays, strings, or quantifiers), and not a verification framework. Reach for those tools when the model calls for them.

Install

dependencies {
  implementation("com.eignex:klause:LATEST")
}

Where to go next