DOCSEARCHbyAlgolia
Submit Docs

Gophersat

repository·master·Indexed 18 days ago

https://github.com/crillab/gophersat

A SAT, pseudo-boolean, and MAXSAT solver written purely in Go. It serves as an efficient inference engine for Go programs, supporting DIMACS CNF, OPB, and WCNF file formats. Key features include cardinality constraints, a cutting-planes solving strategy, model counting, and tools for analyzing unsatisfiable instances via RUP certificates and Minimal Unsatisfiable Subset (MUS) extraction.

Tokens
2.1K
Snippets
9
Records
15
Agent score
54%

What's inside gophersat

  1. What is MAXSAT?

    master

    MAXSAT is the optimization equivalent of the SAT decision problem. While a SAT solver returns a model satisfying all clauses or UNSAT, a MAXSAT solver returns a model that satisfies as many clauses as possible.

    Types of MAXSAT:

    • Partial MAXSAT: Some clauses (hard clauses) must be satisfied, while others (soft clauses) are optional.
    • Weighted MAXSAT: Clauses are associated with a cost (weight). The solver seeks to maximize the weight of satisfied clauses.
    • Partial Weighted MAXSAT: Combines both hard/soft clauses and weights.

  2. What is a pseudo-boolean problem?

    master

    A pseudo-boolean expression is a linear constraint of the form:

    w1 l1 + w2 x2 + ... + wn xn ≥ y

    where y and all wi are integer constants and all li are boolean literals.

    These are a generalization of propositional clauses. For example, the clause x1 ∨ x2 ∨ ... ∨ xn can be rewritten as x1 + x2 + ... + xn ≥ 1. Gophersat solves both decision problems and optimization problems (minimizing a cost function) for these constraints.

  3. Understand UNSAT certificates and MUSes in Gophersat

    master

    Since version 1.2, Gophersat provides facilities to analyze unsatisfiable (UNSAT) instances. This is useful for verifying solver correctness and obtaining explanations for why a formula cannot be made true.

    UNSAT Certificates

    An UNSAT certificate is a sequence of clauses (often using RUP notation or extensions) that can be deduced from the original formula. It provides a mathematical proof that the formula is unsatisfiable, allowing users to verify the result without trusting the solver's internal logic.

    Note: Because certificates are traces of the solving process, they can be significantly larger than the original formula.

    Minimal Unsatisfiable Subformula (MUS)

    A Minimal Unsatisfiable Subformula (MUS) is a subset of the original clauses that is itself UNSAT, but becomes satisfiable if any single clause is removed. MUSes help humans identify the specific core of a problem that causes unsatisfiability.

    Key considerations for MUS extraction:

    • Computational Cost: Finding a MUS is expensive. Gophersat finds a MUS by checking if each clause is required to maintain unsatisfiability, which involves calling the SAT solver $n$ times (where $n$ is the number of clauses). This can be extremely slow for large formulas.
    • Non-Uniqueness: A problem can have multiple MUSes. Finding one MUS does not guarantee you have found the shortest possible MUS, nor does it reveal how many other MUSes exist.
    • Limitations: Gophersat cannot find all MUSes or the absolute smallest MUS, as these tasks are computationally intractable.

  5. Install Gophersat

    master
    Gophersat is a SAT and pseudo-boolean solver written in Go. It is designed to provide SAT/PB technologies directly to Go developers without requiring C/C++ interfaces or cgo dependencies. It is suitable for applications with many small problems or those requiring minimal dependencies, though it may be slower than highly optimized state-of-the-art solvers for very large, difficult problems.

  6. Extract a Minimal Unsatisfiable Subset (MUS)

    master

    When a problem is unsatisfiable, you can use the -mus flag to extract a Minimal Unsatisfiable Subset (MUS). This identifies the smallest subset of clauses that still makes the problem unsatisfiable.

    Note: The CLI implementation of MUS extraction uses explain.ParseCNF and the .MUS() method on the parsed problem.

    gophersat -mus problem.cnf

  7. Count models for a boolean formula

    master

    Model counting allows you to determine how many solutions exist for a given formula.

    Using the Go API

    Use the CountModels method on a solver.Solver instance.

    Using the CLI

    You can count models directly from the command line by passing the --count flag followed by the filename (which can be a .opb or .cnf file).

    gophersat --count filename

  9. Generate UNSAT certificates and extract MUS

    master

    For pure SAT problems (not pseudo-boolean), Gophersat provides tools to understand unsatisfiable (UNSAT) instances.

    Generate an RUP certificate

    To generate a certificate using RUP notation, use the -certified flag. The certificate is printed to standard output. Note that if the problem is satisfiable, a partial/useless certificate may still be generated.

    gophersat -certified problem.cnf

    Extract a Minimal Unsatisfiable Subset (MUS)

    To extract a MUS from an UNSAT instance, use the -mus flag. The MUS is printed to standard output. If the problem is satisfiable, an error message will be displayed.

    gophersat -mus problem.cnf
    gophersat -certified problem.cnf
# or
gophersat -mus problem.cnf

  10. Solve MAXSAT problems with the CLI

    master

    Gophersat can solve weighted MAXSAT problems using the maxsat package by reading WCNF files.

    gophersat [--verbose] file.wcnf

    Options:

    • --verbose: Displays information during the solving process.
    gophersat --verbose file.wcnf

  11. Enable the cutting-planes strategy

    master

    For certain problems (like the pigeonhole problem) that are difficult for pure logical reasoning, you can use the optional cutting-planes solving strategy using the -cp flag.

    gophersat -cp problem.opb

  12. Solve pseudo-boolean problems with the CLI

    master

    Gophersat can solve pseudo-boolean decision and optimization problems by reading OPB files.

    gophersat [--verbose] file.opb

    Supported problem types:

    • DEC-SMALLINT-LIN: Decision problems (is there a solution?) for linear constraints on small integers ($n < 2^{30}$).
    • OPT-SMALLINT-LIN: Optimization problems (minimizing a cost function) for linear constraints on small integers.

    Options:

    • --verbose: Displays information during the solving process.
    gophersat --verbose file.opb