///|
fn main {
  let builder = @sat.CnfBuilder::new()
  let local_cache = builder.new_var("local_cache")
  let distributed_cache = builder.new_var("distributed_cache")
  let strict_consistency = builder.new_var("strict_consistency")
  let offline_mode = builder.new_var("offline_mode")
  builder.exactly_one([local_cache, distributed_cache])
  builder.implies(strict_consistency, distributed_cache)
  builder.add_clause([
    @sat.Lit::neg(offline_mode),
    @sat.Lit::neg(distributed_cache),
  ])
  let cnf = builder.cnf()
  let choices = [
    @sat.Lit::pos(strict_consistency),
    @sat.Lit::pos(offline_mode),
    @sat.Lit::pos(local_cache),
  ]
  let report = @sat.minimal_unsat_core(cnf, choices)
  println("MoonSatKit configuration conflict demo")
  println(cnf.stats().to_json())
  println(report.to_json())
  println(
    "core literals are necessary; this is inclusion-minimal, not minimum-cardinality",
  )
}