Documentation
¶
Overview ¶
Package explain provides facilities to check and understand UNSAT instances.
Index ¶
- Variables
- type Options
- type Problem
- func (pb *Problem) CNF() string
- func (pb *Problem) MUS() (mus *Problem, err error)
- func (pb *Problem) MUSDeletion() (mus *Problem, err error)
- func (pb *Problem) MUSInsertion() (mus *Problem, err error)
- func (pb *Problem) MUSMaxSat() (mus *Problem, err error)
- func (pb *Problem) Unsat(cert io.Reader) (valid bool, err error)
- func (pb *Problem) UnsatChan(ch chan string) (valid bool, err error)
- func (pb *Problem) UnsatSubset() (subset *Problem, err error)
Examples ¶
Constants ¶
This section is empty.
Variables ¶
var ErrNotUnsat = fmt.Errorf("problem is not UNSAT")
ErrNotUnsat is the error returned when trying to get the MUS or UnsatSubset of a satisfiable problem.
Functions ¶
This section is empty.
Types ¶
type Options ¶
type Options struct {
// If Verbose is true, information about resolution will be written on stdout.
Verbose bool
}
Options is a set of options that can be set to true during the checking process.
type Problem ¶
type Problem struct {
Clauses [][]int
NbVars int
NbClauses int
Options Options
// contains filtered or unexported fields
}
A Problem is a conjunction of Clauses. This package does not use solver's representation. We want this code to be as simple as possible to be easy to audit. On the other hand, solver's code must be as efficient as possible.
func (*Problem) CNF ¶
CNF returns a representation of the problem using the Dimacs syntax.
Example ¶
const cnf = `p cnf 3 3
c This is a simple problem
1 2 -3 0
-1 -2 3 0
2 0`
pb, err := ParseCNF(strings.NewReader(cnf))
if err != nil {
fmt.Printf("could not parse problem: %v", err)
} else {
fmt.Println(pb.CNF())
}
Output: p cnf 3 3 1 2 -3 0 -1 -2 3 0 2 0
func (*Problem) MUS ¶
MUS returns a Minimal Unsatisfiable Subset for the problem. A MUS is an unsatisfiable subset such that, if any of its clause is removed, the problem becomes satisfiable. A MUS can be useful to understand why a problem is UNSAT, but MUSes are expensive to compute since a SAT solver must be called several times on parts of the original problem to find them. The exact algorithm used to compute the MUS is not guaranteed. If you want to use a given algorithm, use the relevant functions.
Example ¶
const cnf = `p cnf 6 9
c This is a simple problem
1 2 -3 0
-1 -2 3 0
2 5 0
6 0
2 -5 0
3 4 5 0
-1 -2 0
1 3 0
1 -3 0`
pb, err := ParseCNF(strings.NewReader(cnf))
if err != nil {
fmt.Printf("could not parse problem: %v", err)
return
}
mus, err := pb.MUS()
if err != nil {
fmt.Printf("could not compute MUS: %v", err)
return
}
musCnf := mus.CNF()
// Sort clauses so as to always have the same output
lines := strings.Split(musCnf, "\n")
sort.Sort(sort.StringSlice(lines[1:]))
musCnf = strings.Join(lines, "\n")
fmt.Println(musCnf)
Output: p cnf 6 5 -1 -2 0 1 -3 0 1 3 0 2 -5 0 2 5 0
func (*Problem) MUSDeletion ¶
MUSDeletion returns a Minimal Unsatisfiable Subset for the problem using the insertion method. A MUS is an unsatisfiable subset such that, if any of its clause is removed, the problem becomes satisfiable. A MUS can be useful to understand why a problem is UNSAT, but MUSes are expensive to compute since a SAT solver must be called several times on parts of the original problem to find them. The deletion algorithm is guaranteed to call exactly n SAT solvers, where n is the number of clauses in the problem. It can be quite efficient, but each time the solver is called, it is starting from scratch. Other methods keep the solver "hot", so despite requiring more calls, these methods can be more efficient in practice.
func (*Problem) MUSInsertion ¶
MUSInsertion returns a Minimal Unsatisfiable Subset for the problem using the insertion method. A MUS is an unsatisfiable subset such that, if any of its clause is removed, the problem becomes satisfiable. A MUS can be useful to understand why a problem is UNSAT, but MUSes are expensive to compute since a SAT solver must be called several times on parts of the original problem to find them. The insertion algorithm is efficient is many cases, as it calls the same solver several times in a row. However, in some cases, the number of calls will be higher than using other methods. For instance, if called on a formula that is already a MUS, it will perform n*(n-1) calls to SAT, where n is the number of clauses of the problem.
func (*Problem) MUSMaxSat ¶
MUSMaxSat returns a Minimal Unsatisfiable Subset for the problem using the MaxSat strategy. A MUS is an unsatisfiable subset such that, if any of its clause is removed, the problem becomes satisfiable. A MUS can be useful to understand why a problem is UNSAT, but MUSes are expensive to compute since a SAT solver must be called several times on parts of the original problem to find them. With the MaxSat strategy, the function computes the MUS through several calls to MaxSat.
func (*Problem) Unsat ¶
Unsat will parse a certificate, and return true iff the certificate is valid, i.e iff it makes the problem UNSAT through unit propagation. If pb.Options.ExtractSubset is true, a subset will also be extracted for that problem.
func (*Problem) UnsatChan ¶
UnsatChan will wait RUP clauses from ch and use them as a certificate. It will return true iff the certificate is valid, i.e iff it makes the problem UNSAT through unit propagation. If pb.Options.ExtractSubset is true, a subset will also be extracted for that problem.
func (*Problem) UnsatSubset ¶
UnsatSubset returns an unsatisfiable subset of the problem. The subset is not guaranteed to be a MUS, meaning some clauses of the resulting problem might be removed while still keeping the unsatisfiability of the problem. However, this method is much more efficient than extracting a MUS, as it only calls the SAT solver once.
Source Files