🥮 mooncakes.io

    moonsatkit

    Backend-neutral SAT modeling with temporary assumptions and explainable minimal conflict cores for MoonBit.

    sat
    cnf
    dimacs
    constraint
    solver
    Download zip
    Author
    Version
    0.2.0
    License
    Apache-2.0
    Repository
    Last updated
    4 months ago
    Downloads
    42

    No dependencies

    #MoonSatKit

    MoonSatKit provides backend-neutral SAT modeling and explainable conflict diagnosis for MoonBit.

    let builder = @sat.CnfBuilder::new()
let local = builder.new_var("local")
let distributed = builder.new_var("distributed")
let strict = builder.new_var("strict")
builder.exactly_one([local, distributed])
builder.implies(strict, distributed)

let report = @sat.minimal_unsat_core(
  builder.cnf(),
  [@sat.Lit::pos(strict), @sat.Lit::pos(local)],
)

    solve_with_assumptions keeps the base CNF unchanged. minimal_unsat_core returns a deterministic deletion-minimal assumption core: each returned literal is necessary, but the result is not claimed to have minimum cardinality.

    The package also includes common CNF encodings, DIMACS import/export, an explainable DPLL solver, tests, runnable demonstrations, and a four-backend CI matrix.

    Clause

    source
    pub(all) struct Clause {
      lits : Array[Lit]
    } derive(
    Debug    )

    Clause::len

    source
    fn Clause::len(self : Clause) -> Int

    Clause::new

    source
    fn Clause::new(lits : Array[Lit]) -> Clause

    Clause::unit

    source
    fn Clause::unit(lit : Lit) -> Clause

    Cnf

    source
    pub(all) struct Cnf {
      var_count : Int
      clauses : Array[Clause]
    } derive(
    Debug    )

    Cnf::clause_count

    source
    fn Cnf::clause_count(self : Cnf) -> Int

    Cnf::is_satisfied

    source
    fn Cnf::is_satisfied(self : Cnf, assignment : Array[Int]) -> Bool

    Cnf::new

    source
    fn Cnf::new(var_count : Int, clauses : Array[Clause]) -> Cnf

    Cnf::stats

    source
    fn Cnf::stats(self : Cnf) -> CnfStats

    Cnf::to_dimacs

    source
    fn Cnf::to_dimacs(self : Cnf) -> String

    CnfBuilder

    source
    pub(all) struct CnfBuilder {
      names : Array[String]
      clauses : Array[Clause]
    } derive(
    Debug    )

    CnfBuilder::add_clause

    source
    fn CnfBuilder::add_clause(self : CnfBuilder, lits : Array[Lit]) -> Unit

    CnfBuilder::and_gate

    source
    fn CnfBuilder::and_gate(self : CnfBuilder, out : Var, inputs : Array[Var]) -> Unit

    CnfBuilder::at_least_one

    source
    fn CnfBuilder::at_least_one(self : CnfBuilder, vars : Array[Var]) -> Unit

    CnfBuilder::at_most_k_sequential

    source
    fn CnfBuilder::at_most_k_sequential(self : CnfBuilder, vars : Array[Var], k : Int, prefix? : String) -> Unit

    CnfBuilder::at_most_one_pairwise

    source
    fn CnfBuilder::at_most_one_pairwise(self : CnfBuilder, vars : Array[Var]) -> Unit

    CnfBuilder::cnf

    source
    fn CnfBuilder::cnf(self : CnfBuilder) -> Cnf

    CnfBuilder::equivalent

    source
    fn CnfBuilder::equivalent(self : CnfBuilder, a : Var, b : Var) -> Unit

    CnfBuilder::exactly_one

    source
    fn CnfBuilder::exactly_one(self : CnfBuilder, vars : Array[Var]) -> Unit

    CnfBuilder::implies

    source
    fn CnfBuilder::implies(self : CnfBuilder, a : Var, b : Var) -> Unit

    CnfBuilder::new

    source
    fn CnfBuilder::new() -> CnfBuilder

    CnfBuilder::new_var

    source
    fn CnfBuilder::new_var(self : CnfBuilder, name : String) -> Var

    CnfBuilder::or_gate

    source
    fn CnfBuilder::or_gate(self : CnfBuilder, out : Var, inputs : Array[Var]) -> Unit

    CnfBuilder::require_literal

    source
    fn CnfBuilder::require_literal(self : CnfBuilder, lit : Lit) -> Unit

    CnfStats

    source
    pub(all) struct CnfStats {
      vars : Int
      clauses : Int
      literals : Int
      max_clause_len : Int
    } derive(Eq, 
    Debug    )

    CnfStats::to_json

    source
    fn CnfStats::to_json(self : CnfStats) -> String

    Lit

    source
    pub(all) struct Lit {
      var_id : Int
      negated : Bool
    } derive(Eq, 
    Debug    )

    Lit::neg

    source
    fn Lit::neg(v : Var) -> Lit

    Lit::not

    source
    fn Lit::not(self : Lit) -> Lit

    Lit::pos

    source
    fn Lit::pos(v : Var) -> Lit

    Lit::to_dimacs

    source
    fn Lit::to_dimacs(self : Lit) -> Int

    SolveResult

    source
    pub(all) struct SolveResult {
      sat : Bool
      decided : Bool
      assignment : Array[Int]
      trace : Array[String]
    } derive(
    Debug    )

    SolveResult::assignment_dimacs

    source
    fn SolveResult::assignment_dimacs(self : SolveResult) -> String

    SolveResult::to_json

    source
    fn SolveResult::to_json(self : SolveResult) -> String

    SolveResult::value_of

    source
    fn SolveResult::value_of(self : SolveResult, v : Var) -> Int

    UnitSearch

    source
    pub(all) struct UnitSearch {
      found : Bool
      conflict : Bool
      lit : Lit
    } derive(Eq, 
    Debug    )

    UnsatCoreReport

    source
    pub(all) struct UnsatCoreReport {
      valid : Bool
      unsat : Bool
      assumptions : Array[Lit]
      core : Array[Lit]
      minimal : Bool
      solver_calls : Int
      message : String
    } derive(
    Debug    )

    UnsatCoreReport::to_json

    source
    fn UnsatCoreReport::to_json(self : UnsatCoreReport) -> String

    Var

    source
    pub(all) struct Var {
      id : Int
      name : String
    } derive(Eq, 
    Debug    )

    Var::new

    source
    fn Var::new(id : Int, name : String) -> Var

    encode_n_queens

    source
    fn encode_n_queens(size : Int) -> Cnf

    minimal_unsat_core

    source
    fn minimal_unsat_core(cnf : Cnf, assumptions : Array[Lit]) -> UnsatCoreReport

    Computes a deterministic deletion-minimal UNSAT core over assumptions.

    "Minimal" means every returned literal is necessary: removing any one makes the formula satisfiable. It does not claim minimum cardinality.

    parse_dimacs

    source
    fn parse_dimacs(input : String) -> Cnf

    solve

    source
    fn solve(cnf : Cnf) -> SolveResult

    solve_with_assumptions

    source
    fn solve_with_assumptions(cnf : Cnf, assumptions : Array[Lit]) -> SolveResult

    Solves a CNF under temporary literal assumptions.

    The original CNF is not modified. Invalid variable identifiers produce an undecided, unsatisfied result with an explanatory trace.

    Source Files

    Powered by MoonBit

    Site sourceReport issueModulesSkillsCLIBuild queueStatistics

    © 2026 mooncakes.io