🥮 mooncakes.io

moonsatkit

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

sat
cnf
dimacs
constraint
solver
moon add yf666888/moonsatkit@0.2.0
Download zip
Author
Version
0.2.0
License
Apache-2.0
Repository
Last updated
last month
Downloads
13
README

#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 issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io