Documentation
¶
Overview ¶
Package bf offers facilities to test the satisfiability of generic boolean formula.
SAT solvers usually expect as an input CNF formulas. A CNF, or Conjunctive Normal Form, is a set of clauses that must all be true, each clause being a set of potentially negated literals. For the clause to be true, at least one of these literals must be true.
However, manually translating a given boolean formula to an equivalent CNF is tedious and error-prone. This package provides a set of logical connectors to define and solve generic logical formulas. Those formulas are then automatically translated to CNF and passed to the gophersat solver.
For example, the following boolean formula:
¬(a ∧ b) → ((c ∨ ¬d) ∧ ¬(c ∧ (e ↔ ¬c)) ∧ ¬(a ⊻ b))
Will be defined with the following code:
f := Not(Implies(And(Var("a"), Var("b")), And(Or(Var("c"), Not(Var("d"))), Not(And(Var("c"), Eq(Var("e"), Not(Var("c"))))), Not(Xor(Var("a"), Var("b"))))))
When calling `Solve(f)`, the following equivalent CNF will be generated:
a ∧ b ∧ (¬c ∨ ¬x1) ∧ (d ∨ ¬x1) ∧ (c ∨ ¬x2) ∧ (¬e ∨ ¬c ∨ ¬x2) ∧ (e ∨ c ∨ ¬x2) ∧ (¬a ∨ ¬b ∨ ¬x3) ∧ (a ∨ b ∨ ¬x3) ∧ (x1 ∨ x2 ∨ x3)
Note that this formula is longer than the original one and that some variables were added to it. The translation is both polynomial in time and space. When fed this CNF as an input, gophersat then returns the following map:
map[a:true b:true c:false d:true e:false]
Index ¶
Examples ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func Dimacs ¶
Dimacs writes the DIMACS CNF version of the formula on w. It is useful so as to feed it to any SAT solver. The original names of variables is associated with their DIMACS integer counterparts in comments, between the prolog and the set of clauses. For instance, if the variable "a" is associated with the index 1, there will be a comment line "c a=1".
Example ¶
f := Eq(And(Or(Var("a"), Not(Var("b"))), Not(Var("a"))), Var("b"))
if err := Dimacs(f, os.Stdout); err != nil {
fmt.Printf("Could not generate DIMACS file: %v", err)
}
Output: p cnf 4 6 c a=2 c b=3 -2 -1 0 3 -1 0 1 2 3 0 2 -3 -4 0 -2 -4 0 4 -3 0
Types ¶
type CNF ¶
type CNF struct {
Clauses [][]int
// contains filtered or unexported fields
}
A CNF is the representation of a boolean formula as a conjunction of disjunction. It can be solved by a SAT solver.
type Formula ¶
type Formula interface {
String() string
Eval(model map[string]bool) bool
// contains filtered or unexported methods
}
A Formula is any kind of boolean formula, not necessarily in CNF.
var False Formula = falseConst{}
False is the constant denoting a contradiction.
var True Formula = trueConst{}
True is the constant denoting a tautology.
Source Files