README
¶
PiGoSAT
Go (golang) bindings for Picosat, the satisfiability solver
Tested on Go versions 1.7 and 1.8, but may work on earlier versions of Go.
Downloading
The project is hosted on GitHub. You can either download a release or use "go get":
$ go get github.com/wkschwartz/pigosat
PiGoSAT is a wrapper around Picosat, whose C source files are included in this repository.
Contributing
If you notice a bug or would like to request a feature, please file an issue ticket, checking to see if one exists already.
If you would like to contribute code, please fork PiGoSAT and send a pull request.
Updating PicoSAT
Replace picsoat.h, picosat.c, and update PicosatVersion in
pigosat.go. Copy LICENSE from PicoSAT to LICENSE.picosat in PiGoSAT.
Other maintenance notes
Test PiGoSAT by switching to its source directory and running
$ go vet .
$ go test -race
Before committing, please run
$ gofmt -w -s .
The only place you need to update the version number is in pigosat.go's
Version constant. However, if you git tag or make a release on GitHub,
make sure the version number matches the tag name.
When a new major or minor version (x.0 or 1.x) of Go is available, increment the
versions you test PiGoSAT with in .travis.yml, and make a note at the top of
this README document. Go only supports the current and last minor versions
(e.g., 1.8 and 1.7) with security releases, so these are the versions that
PiGoSAT should support.
Documentation
¶
Overview ¶
Package pigosat is a Go binding for the PicoSAT satisfiability solver.
A satisfiability (SAT) solver is for solving expressions such as
(a || b || !c) && (c || !d)
for logical variables a, b, c, and d so that the expression is true. The whole expression is called a formula and each parenthesized unit is called a clause. Variables such as c and their negations such as !c are called literals. The SAT formulation PicoSAT, and thereby PiGoSAT, uses is called "conjunctive normal form" (CNF) dictates that formulas are the conjunctions (AND) of clauses, and clauses are the disjunction (OR) of literals. To allow arbitrary numbers of literals, we think of variables as having names like x_k, where k is an integer at least 1. Empty clauses evaluate to false.
In PicoSAT, and thereby PiGoSAT, we refer to variable x_k simply as k. Instead of a NOT operator ! as part of negated literals, we take the additive inverse, so -k instead of !x_k. Zero is never the name of a variable, so we can use it to mark the end of clauses. In PiGoSAT, the Literal type is an integer type, the Clause type is a slice of Literals, and the Formula type is a slice of Clauses. Thus, the formula above might be written as
Formula{Clause{1, 2, -3, 0}, Clause{3, 4, 0}}
A solution to this formula assigns truth values to variables x_1, ..., x_4. Using the Solution type, we could write a solution to the above formula as
Solution{1: true, 2: false, 3: false, 4: false}
(Notice that the zeroth element is always false). This works because we can substitute for the variables as follows
(true || false || !false) && (false || !false)
which evaluates to true. There are many solutions to the formula. Another one is
Solution{1: false, 2: true, 3: false, 4: false}
Use the Pigosat type to solve SAT problems as follows. First create a Pigosat instance:
p := New(nil).
The argument to New allows advanced users to pass in an Option instance. See its documentation for details. Next, supply the Pigosat instance with your formula:
p.Add(Formula{{1, 2, -3}, {3, 4}})
(This is also a correct way to write the formula for PiGoSAT.)
Calling p.Solve() returns two objects. The second is a Status object, one of the constants Satisfiable, Unsatisfiable, or Unknown. The latter is the status when some (optional) limitation prevents Solve from working long enough to find a solution. This is important because p.Solve() has time complexity exponential in the size of the formula in the worst case, meaning p.Solve() can be very slow. Hopefully you will get a status of Satisfiable or Unsatisfiable. If the status is Unsatisfiable or Unknown, the solution will be nil. If the status is Satisfiable, the first return value is a Solution object, such as one of the ones above. The Solution object is a proof of satisfiability in the Satisfiable case.
p.Solve() can just tell you yes or no to a formula, but PiGoSAT has facilities for optimization problems as well. Check out the Minimizer interface and the Minimize function. The idea is that Minimize calls a function you write called IsFeasible with different integer parameter values. IsFeasible generates a formula based on this parameter, constructs a Pigosat object, and calls its Solve method. If your problem is such that IsFeasible always returns Satisfiable above some parameter value K and Unsatisfiable below K, Minimize can find K. An example of where this is useful is in graph coloring problems. The parameter can represent the number of available colors. Your custom IsFeasible function generates a formula based on some input graph to determine whether there is a proper coloring (an assignment of colors to vertices so that neighboring vertices have different colors) of the graph that uses at most that number of colors. Minimize can then determine the chromatic number of the graph, the minimum number of colors needed for a proper coloring.
Example ¶
p, _ := New(nil)
// Calling Delete is not usually necessary. Advanced users, see Delete's
// documentation.
defer p.Delete()
p.Add(Formula{{1, 2, -3}, {3, 4}})
fmt.Printf("Number of variables == %d\n", p.Variables())
fmt.Printf("Number of clauses == %d\n", p.AddedOriginalClauses())
solution, status := p.Solve()
fmt.Println(status, "solution ==", solution)
fmt.Printf(" == %#v\n", solution)
p.BlockSolution(solution)
fmt.Println("\nMore solutions:")
for solution, status := p.Solve(); status == Satisfiable; solution, status = p.Solve() {
fmt.Println(status, "solution ==", solution)
p.BlockSolution(solution)
}
Output: Number of variables == 4 Number of clauses == 2 Satisfiable solution == {1:true , 2:true , 3:true , 4:true} == pigosat.Solution{false, true, true, true, true} More solutions: Satisfiable solution == {1:true , 2:true , 3:true , 4:false} Satisfiable solution == {1:true , 2:true , 3:false, 4:true} Satisfiable solution == {1:true , 2:false, 3:false, 4:true} Satisfiable solution == {1:true , 2:false, 3:true , 4:true} Satisfiable solution == {1:true , 2:false, 3:true , 4:false} Satisfiable solution == {1:false, 2:false, 3:false, 4:true} Satisfiable solution == {1:false, 2:true , 3:false, 4:true} Satisfiable solution == {1:false, 2:true , 3:true , 4:true} Satisfiable solution == {1:false, 2:true , 3:true , 4:false}
Index ¶
- Constants
- func Minimize(m Minimizer) (min int, optimal, feasible bool)
- type Clause
- type Formula
- type Literal
- type Minimizer
- type Options
- type Pigosat
- func (p *Pigosat) Add(clauses Formula)
- func (p *Pigosat) AddedOriginalClauses() int
- func (p *Pigosat) Assume(lit Literal)
- func (p *Pigosat) BlockSolution(solution Solution) error
- func (p *Pigosat) Delete()
- func (p *Pigosat) FailedAssumption(lit Literal) bool
- func (p *Pigosat) FailedAssumptions() []Literal
- func (p *Pigosat) MaxSatisfiableAssumptions() []Literal
- func (p *Pigosat) NextMaxSatisfiableAssumptions() []Literal
- func (p *Pigosat) Print(w io.Writer) error
- func (p *Pigosat) Res() (status Status)
- func (p *Pigosat) Seconds() time.Duration
- func (p *Pigosat) Solve() (solution Solution, status Status)
- func (p *Pigosat) Variables() int
- func (p *Pigosat) WriteClausalCore(f io.Writer) error
- func (p *Pigosat) WriteCompactTrace(f io.Writer) error
- func (p *Pigosat) WriteExtendedTrace(f io.Writer) error
- type Solution
- type Status
Examples ¶
Constants ¶
const PicosatVersion = "965"
PicosatVersion is the version string from the underlying PicoSAT library.
const Version = "1.0.0"
Version is PiGoSAT's semantic version number. See http://semver.org.
Variables ¶
This section is empty.
Functions ¶
func Minimize ¶ added in v0.3.1
Minimize finds the value min that minimizes Minimizer m. If the value can be proved to be optimal, that is, k < min causes m.IsFeasible(k) to return status Unsatisfiable, optimal will be set to true. If m.IsFeasible(m.UpperBound()) returns status Unsatisfiable, feasible will be set to false. Every return value from IsFeasible will be passed to m.RecordSolution. Panic if m.UpperBound() < m.LowerBound(). If m.IsFeasible returns a status other than Satisfiable, it will be treated as Unsatisfiable.
Types ¶
type Clause ¶ added in v1.0.0
type Clause []Literal
Clause is a slice of Literals ORed together. An optional zero ends a clause, even in the middle of a slice: [1, 0, 2] is the same as [1, 0] is the same as [1]. An empty Clause always evaluates false and thus can never be satisfied.
type Literal ¶ added in v1.0.0
type Literal int32
Literal represents a variable or its logical negations. We name variables by ID numbers starting from one and use arithmetic negation to indicate logical negation. The zero literal indicates the end of a clause.
type Minimizer ¶ added in v0.3.1
type Minimizer interface {
// LowerBound returns a lower bound for the optimal value of k.
LowerBound() int
// UpperBound returns an upper bound for the optimal value of k.
UpperBound() int
// IsFeasible takes a value k and returns whether the Minimizer instance's
// underlying model is feasible for that input value. IsFeasible can model
// any set of constraints it likes as long as there is a unique integer K
// such that k < K implies IsFeasible(k) returns status Unsatisfiable and
// k >= K implies IsFeasible(k) returns status Satisfiable.
IsFeasible(k int) (solution Solution, status Status)
// RecordSolution allows types implementing this interface to store
// solutions for after minimization has finished.
RecordSolution(k int, solution Solution, status Status)
}
Minimizer allows you to find the lowest integer K such that
LowerBound() <= K <= UpperBound()
and IsFeasible(K) returns status Satisfiable.
type Options ¶ added in v0.3.1
type Options struct {
// Set PropagationLimit to a positive value to limit how long the solver
// tries to find a solution.
PropagationLimit uint64
// Default (nil value) output file is standard out. The client is
// responsible for closing the file after he is done with the Pigosat
// object.
OutputFile *os.File
// Set verbosity level. A verbosity level of 1 and above prints more and
// more detailed progress reports on the output file, set by OutputFile.
// Verbose messages are prefixed with the string set by Prefix.
Verbosity uint
// Set the prefix used for printing verbose messages and statistics.
// Default is "c ".
Prefix string
// Measure all time spent in all calls in PicoSAT's solver (extra time in
// PiGoSAT is generally linear in the number of variables). By default only
// the time spent in PicoSAT's internal solver is measured. Setting this
// option may as much as triple the time needed to add large formulas.
MeasureAllCalls bool
// If you want to extract cores or proof traces using WriteClausalCore,
// WriteCompactTrace, WriteExtendedTrace, then set this option true. Doing
// so may increase memory usage.
EnableTrace bool
}
Options contains optional settings for the Pigosat constructor. Zero values for each field indicate default behavior.
type Pigosat ¶
type Pigosat struct {
// contains filtered or unexported fields
}
Pigosat must be created with New and stores the state of the solver. It is safe for concurrent use.
You must not use runtime.SetFinalizer with Pigosat objects. Attempting to call a method on an uninitialized or deleted Pigosat object panics.
Casual users of PiGoSAT need not call the Delete method. More intensive users should consult Delete's documentation.
func New ¶ added in v1.0.0
New returns a new Pigosat instance, ready to have literals added to it. The error return value need only be checked if the OutputFile option is non-nil. If options is nil, New chooses all defaults.
func (*Pigosat) Add ¶ added in v1.0.0
Add appends a slice of Clauses to p's existing formula. See the documentation for Literal, Clause, and Formula to understand how p.Solve will interpret the formula.
A zero in a clause terminates the clause even if the zero is not at the end of the slice. An empty clause always causes the formula to be unsatisfiable.
func (*Pigosat) AddedOriginalClauses ¶
AddedOriginalClauses returns the number of clauses in the formula: The n in the DIMACS header "p cnf m <n>".
func (*Pigosat) Assume ¶ added in v1.0.0
Assume adds a temporary unit clause, i.e., a clause containing the one literal you pass as an argument. An assumption remains valid after the next call to Solve returns until a call to Add, Assume, or a second Solve. You can add arbitrary many assumptions before the next call to Solve. Methods FailedAssumptions, FailedAssumptions, MaxSatisfiableAssumptions, and NextMaxSatisfiableAssumptions operate on the current, valid assumptions.
Example ¶
ExamplePigosat_Assume demonstrates how to use Assume and related methods.
var formula = Formula{{1, 2, 3}, {1, 2}, {2, 3}}
p, _ := New(nil)
p.Add(formula)
fmt.Println("Formula:", formula)
solution, status := p.Solve()
fmt.Println("No assumptions:", status, "solution ==", solution)
// Satisfiable assumptions
fmt.Println()
fmt.Println("**** SATISFIABLE ASSUMPTIONS ****")
p.Assume(1)
p.Assume(-2)
// Assumptions do not change the number of clauses.
fmt.Println("Assume 1, -2 : Number of clauses:", p.AddedOriginalClauses())
solution, status = p.Solve()
fmt.Println(" ", status, "solution ==", solution)
// Calls to p.Add or p.Assume cancel assumptions 1 and -2
// immediately, or a second call to p.Solve also cancels the assumptions.
p.Assume(-3)
solution, status = p.Solve()
fmt.Println("Assume -3:", status, "solution ==", solution)
// Unsatisfiable assumptions
fmt.Println()
fmt.Println("**** UNSATISFIABLE ASSUMPTIONS ****")
p.Assume(-1) // assume unit clause Clause{-1, 0}
p.Assume(-2) // assume unit clause Clause{-2, 0}
solution, status = p.Solve() // assumes -1 and -2 hold
fmt.Println("Assume -1, -2 :", status, "solution ==", solution)
// Assumptions -1 and -2 caused unsatisfiability.
fmt.Println(" Failed assumptions:", p.FailedAssumptions())
fmt.Println(" Assumption -1 failed:", p.FailedAssumption(-1))
fmt.Println(" Assumption -2 failed:", p.FailedAssumption(-2))
// Not every subset of the assumptions causes unsatisfiability.
// p.MaxSatisfiableAssumptions would return the same as
// p.NextMaxSatisfiableAssumptions, but the return value wouldn't change
// with each call like it does with p.NextMaxSatisfiableAssumptions.
fmt.Println(" Maximal satisfiable subset of assumptions 1:", p.NextMaxSatisfiableAssumptions())
fmt.Println(" Maximal satisfiable subset of assumptions 2:", p.NextMaxSatisfiableAssumptions())
fmt.Println(" Maximal satisfiable subset of assumptions 3:", p.NextMaxSatisfiableAssumptions())
// p.NextMaxSatisfiableAssumptions does add clauses.
fmt.Println(" Number of clauses:", p.AddedOriginalClauses())
// Unknown status
// Assumptions are valid but p.Solve returns no Solution assignment. The
// solver knowns the status is Unknown until a call to p.Assume,
// p.Add, or p.Solve resets the assumptions.
Output: Formula: [[1 2 3] [1 2] [2 3]] No assumptions: Satisfiable solution == {1:true , 2:true , 3:true} **** SATISFIABLE ASSUMPTIONS **** Assume 1, -2 : Number of clauses: 3 Satisfiable solution == {1:true , 2:false, 3:true} Assume -3: Satisfiable solution == {1:true , 2:true , 3:false} **** UNSATISFIABLE ASSUMPTIONS **** Assume -1, -2 : Unsatisfiable solution == {} Failed assumptions: [-1 -2] Assumption -1 failed: true Assumption -2 failed: true Maximal satisfiable subset of assumptions 1: [-1] Maximal satisfiable subset of assumptions 2: [-2] Maximal satisfiable subset of assumptions 3: [] Number of clauses: 5
func (*Pigosat) BlockSolution ¶ added in v0.3.1
BlockSolution adds a clause to the formula ruling out a given solution. It returns an error if the solution is the wrong length.
func (*Pigosat) Delete ¶
func (p *Pigosat) Delete()
Delete frees memory associated with p's PicoSAT object. Use of p's methods after calling p.Delete() panics.
Casual users do not need to call p.Delete() explicitly. The Go garbage collector should call it automatically as a finalizer. However, if you are creating large numbers of Pigosat objects or are writing a library, explicitly call p.Delete() because the Go garbage collector does not guarantee when or whether finalizers run.
func (*Pigosat) FailedAssumption ¶ added in v1.0.0
FailedAssumption returns whether a given literal is a valid, "failed" assumption (see Assume), meaning the last call to Solve used the assumption to derive unsatisfiability. FailedAssumption always returns false when the last call to Solve had status other than Unsatisfiable. This may be an over-approximation of the set of assumptions necessary to derive unsatisfiability.
func (*Pigosat) FailedAssumptions ¶ added in v1.0.0
FailedAssumptions returns a list of failed assumptions, i.e., all the for which FailedAssumption returns true. See FailedAssumption.
func (*Pigosat) MaxSatisfiableAssumptions ¶ added in v1.0.0
MaxSatisfiableAssumptions computes a maximal subset of satisfiable assumptions. See Assume's documentation. You need to set the assumptions and call Solve() before calling this method. The result is a list of assumptions that consistently can be asserted at the same time.
func (*Pigosat) NextMaxSatisfiableAssumptions ¶ added in v1.0.0
NextMaxSatisfiableAssumptions is like MaxSatisfiableAssumptions, but operates like an iterator to give a different maximal subset of satisfiable assumptions upon each call. To do this, it internally calls Solve followed by BlockSolution, which modifies the underlying formula (thus changing the result of AddedOriginalClauses), and then reassuming the solutions that were valid when you called NextMaxSatisfiableAssumptions. Use it as follows. First, set your formula and assumptions using Add and Assume. Then iterate over the different maximal satisfiable subsets of assumptions with:
for mss := p.NextMaxSatisfiableAssumptions(); len(mss) > 0; mss = p.NextMaxSatisfiableAssumptions() {
// Do stuff with mss
}
func (*Pigosat) Print ¶ added in v1.0.0
Print appends the formula in DIMACS format to the given io.Writer.
func (*Pigosat) Res ¶ added in v1.0.0
Res returns Solve's last status, or Unknown if Solve hasn't yet been called.
func (*Pigosat) Solve ¶
Solve the formula and return the status of the solution: one of the constants Unsatisfiable, Satisfiable, or Unknown. If satisfiable, return a slice indexed by the variables in the formula (so the first element is always false). Assigning these boolean values to the variables will satisfy the formula and assumptions that p.Add and p.Assume have added to the Pigosat object. See the documentation for Assume regarding when assumptions are valid.
Solve can be used like an iterator, yielding a new solution until there are no more feasible solutions:
for solution, status := p.Solve(); status == Satisfiable; solution, status = p.Solve() {
// Do stuff with solution, status
p.BlockSolution(solution)
}
func (*Pigosat) Variables ¶
Variables returns the number of variables in the formula: The m in the DIMACS header "p cnf <m> n".
func (*Pigosat) WriteClausalCore ¶ added in v1.0.0
WriteClausalCore writes in DIMACS format the clauses that were used in deriving the empty clause. Requires that p was created with EnableTrace.
func (*Pigosat) WriteCompactTrace ¶ added in v1.0.0
WriteCompactTrace writes a compact proof trace in TraceCheck format. Requires that p was created with EnableTrace.
type Solution ¶ added in v1.0.0
type Solution []bool
Solution is a slice of truth values indexed by and corresponding to each variable's ID number (starting at one). The zeroth element has no meaning and is always false.
type Status ¶ added in v1.0.0
type Status int
Status is returned by Pigosat.Solve to indicate success or failure.
const ( // PicoSAT cannot determine the satisfiability of the formula. Unknown Status = C.PICOSAT_UNKNOWN // The formula is satisfiable. Satisfiable Status = C.PICOSAT_SATISFIABLE // The formula cannot be satisfied. Unsatisfiable Status = C.PICOSAT_UNSATISFIABLE )
Return values for Pigosat.Solve's status.
Source Files