🥮 mooncakes.io

    Lyhdsba/fusekite/sat does not have a README file

    BoolExpr

    source
    pub(all) enum BoolExpr {
      Constant(Bool)
      Variable(Int)
      Not(BoolExpr)
      And(BoolExpr, BoolExpr)
      Or(BoolExpr, BoolExpr)
      Xor(BoolExpr, BoolExpr)
    }

    A Boolean expression that can be compiled to equisatisfiable CNF with Tseitin variables.

    CnfFormula

    source
    pub struct CnfFormula {
      // private fields
    }

    A validated CNF formula over variables numbered from 1 through variable_count. A positive literal denotes a variable; a negative literal denotes its complement. Empty clauses are allowed and make the formula unsatisfiable. Tautological clauses are removed during construction.

    CnfFormula::accepts

    source
    fn CnfFormula::accepts(self : CnfFormula, model : Array[Bool]) -> Bool

    Check a reported model against the formula's normalized clauses.

    CnfFormula::clauses

    source
    fn CnfFormula::clauses(self : CnfFormula) -> Array[Array[Int]]

    Return defensive copies of the normalized clauses.

    CnfFormula::from_expression

    source
    fn CnfFormula::from_expression(variable_count : Int, expression : BoolExpr) -> CnfFormula?

    Compile an expression and assert that it is true.

    Variables in the expression are numbered 1 through variable_count. The encoder uses Tseitin definitions and structurally shares repeated subexpressions rather than distributing into potentially exponential DNF/CNF. Generated clauses and variables are validated by the same limits as directly constructed formulas. Distinct expression nodes are capped at 100,000 and nesting at 1,024 levels.

    CnfFormula::new

    source
    fn CnfFormula::new(variable_count : Int, clauses : Array[Array[Int]]) -> CnfFormula?

    Validate and normalize a CNF formula.

    variable_count is limited to 4,096. Clause inputs are copied, duplicate literals are removed, literals are sorted, duplicate clauses are removed, and tautological clauses are omitted. A clause containing no literals is preserved as an immediate contradiction.

    CnfFormula::parse_dimacs

    source
    fn CnfFormula::parse_dimacs(text : String) -> Result[CnfFormula, DimacsError]

    Parse a DIMACS CNF text document.

    The parser accepts standard c comment lines, one p cnf V C header, clauses spanning lines, and zero-terminated clauses. It checks the declared variable and clause counts and applies the normal CNF validation rules.

    CnfFormula::solve

    source
    fn CnfFormula::solve(self : CnfFormula, config : SolverConfig) -> SatReport

    Solve a CNF formula using deterministic DPLL with two-watched-literal propagation.

    Branching uses the first unassigned literal in the first unresolved clause. The solver returns a complete Boolean model on SAT and Unknown if the configured search-node budget is exhausted before a proof is found.

    CnfFormula::variable_count

    source
    fn CnfFormula::variable_count(self : CnfFormula) -> Int

    Return the declared number of variables.

    DimacsError

    source
    pub enum DimacsError {
      MissingHeader
      InvalidHeader
      InvalidInteger
      InvalidLiteral
      ClauseCountMismatch
      TrailingClauseData
    }

    Error returned while reading a DIMACS CNF document.

    SatOutcome

    source
    pub enum SatOutcome {
      Satisfiable(Array[Bool])
      Unsatisfiable
      Unknown
    }

    Result of a bounded SAT search. Unknown means the configured search-node budget was reached before satisfiability or unsatisfiability was proved.

    SatReport

    source
    pub struct SatReport {
      outcome : SatOutcome
      stats : SolverStats
    }

    SAT outcome and reproducible search counters.

    SolverConfig

    source
    pub struct SolverConfig {
      // private fields
    }

    Search bound for the deterministic DPLL solver.

    SolverConfig::new

    source
    fn SolverConfig::new(max_search_nodes : Int) -> SolverConfig?

    Create a positive search budget. Values above one million are rejected to make accidental unbounded searches harder to trigger.

    SolverStats

    source
    pub struct SolverStats {
      search_nodes : Int
      decisions : Int
      propagations : Int
      conflicts : Int
    }

    Counters collected while solving one formula.

    Source Files

    Powered by MoonBit

    Site sourceReport issueModulesSkillsCLIBuild queueStatistics

    © 2026 mooncakes.io