Klause

Kotlin solver for Boolean and integer constraint problems. Finds and samples satisfying solutions, picks the best under a weighted objective, and exports to CNF for external SAT engines. Nominal variables are encoded as Boolean indicators; floats are bucketed onto bounded integers.

Schema

class CampaignSchema : VariableSchema() {
    val type    by nominal("a", "b", "c")
    val budget  by intVar(min = 1000, max = 4000)
    val bonus   by intVar(min = 0, max = 500)
    val rate    by floatVar(min = 0.0, max = 1.0)

    val capWhenA   by constraint { (type eq "a") implies (budget + bonus le 2000) }
    val proportion by constraint { 2 * bonus le budget }
    val highRate   by constraint { rate ge 0.5 }
}

The DSL covers:

• Boolean: and, or, implies, iff, not, xor.
• Nominal: eq and ne against label literals.
• Integer arithmetic: signed +, -, unary -, *, /, %, with Java-truncated division and modulo and variable-by-variable multiplication.
• Comparisons: le, lt, ge, gt, eq, ne over arbitrary integer expressions.
• Counting: atMost, atLeast, cardinality, pseudoBoolean and friends.
• Global: gcc, allDifferent.
• Tabular: table, notTable.
• Integer expressions: min, max, abs, element, ifThenElse.
• Linking: channel, lexLeq, lexLt.

Solving

val schema = CampaignSchema()
val compiled = schema.compile()
val solver = LocalSearchSolver(compiled.problem)

solver.enumerate(LocalSearchParams(maxFlips = 100_000)).take(20).forEach { s ->
    println("type=${compiled.decode(schema.type, s)} budget=${compiled.decode(schema.budget, s)}")
}

val weights = LinearObjective(boolWeights = doubleArrayOf(/* ... */))
val best = solver.minimize(weights, LocalSearchParams(maxFlips = 100_000))

LocalSearchSolver is the default engine. Adapters in :klause-logicng (via bit-blasting to CNF) and :klause-z3 (direct SMT translation) implement the same Sampler and Optimizer interfaces. A BruteForceSolver in core walks the assignment space exhaustively as a ground-truth oracle for small problems. :klause-bench cross-checks all four against a hard-coded portfolio plus pre-made problem instances loaded from DIMACS, OPB, and JSON-SchemaDef files. Run ./gradlew :klause-bench:downloadSatlib once to fetch the SATLIB uf20-91 (sat) and uuf50-218 (unsat) sets — :klause-bench:run will include them automatically (sample size capped via -Dklause.bench.satlib.max=N, default 10 per set).

Bit-blasting

val cnf = BitBlaster.compile(compiled.problem)
val text = cnf.toDimacs()

TODO

• Maven Central publishing, CI.