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]
It is also possible to create boolean formulas using a dedicated syntax. The BNF grammar is as follows:
formula ::= clause { ';' clause }*
clause ::= implies { '=' implies }*
implies ::= or { '->' or}*
or ::= and { '|' and}*
and ::= not { '&' not}*
not ::= '^'not | atom
atom ::= ident | '(' formula ')'
So the formula
¬(a ∧ b) → ((c ∨ ¬d) ∧ ¬(c ∧ (e ↔ ¬c)) ∧ ¬(a ⊻ b))
would be written as
^(a & b) -> ((c | ^d) & ^(c & (e = ^c)) & ^(a = ^b))
a call to the `Parse` function will then create the associated Formula.
Index ¶
- func Dimacs(f Formula, w io.Writer) error
- func Solve(f Formula) map[string]bool
- type Formula
- func And(subs ...Formula) Formula
- func Eq(f1, f2 Formula) Formula
- func Implies(f1, f2 Formula) Formula
- func Not(f Formula) Formula
- func Or(subs ...Formula) Formula
- func Parse(r io.Reader) (Formula, error)
- func Unique(vars ...string) Formula
- func Var(name string) Formula
- func Xor(f1, f2 Formula) Formula
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
func Solve ¶
Solve solves the given formula. f is first converted as a CNF formula. It is then given to gophersat. The function returns a model associating each variable name with its binding, or nil if the formula was not satisfiable.
Example ¶
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"))))))
model := Solve(f)
if model != nil {
fmt.Printf("Problem is satisfiable")
} else {
fmt.Printf("Problem is unsatisfiable")
}
Output: Problem is satisfiable
Example (Sudoku) ¶
const varFmt = "line-%d-col-%d:%d" // Scheme for variable naming
f := True
// In each spot, exactly one number is written
for line := 1; line <= 9; line {
for col := 1; col <= 9; col {
vars := make([]string, 9)
for val := 1; val <= 9; val {
vars[val-1] = fmt.Sprintf(varFmt, line, col, val)
}
f = And(f, Unique(vars...))
}
}
// In each line, each number appears at least once.
// Since there are 9 spots and 9 numbers, that means each number appears exactly once.
for line := 1; line <= 9; line {
for val := 1; val <= 9; val {
var vars []Formula
for col := 1; col <= 9; col {
vars = append(vars, Var(fmt.Sprintf(varFmt, line, col, val)))
}
f = And(f, Or(vars...))
}
}
// In each column, each number appears at least once.
for col := 1; col <= 9; col {
for val := 1; val <= 9; val {
var vars []Formula
for line := 1; line <= 9; line {
vars = append(vars, Var(fmt.Sprintf(varFmt, line, col, val)))
}
f = And(f, Or(vars...))
}
}
// In each 3x3 box, each number appears at least once.
for lineB := 0; lineB < 3; lineB {
for colB := 0; colB < 3; colB {
for val := 1; val <= 9; val {
var vars []Formula
for lineOff := 1; lineOff <= 3; lineOff {
line := lineB*3 lineOff
for colOff := 1; colOff <= 3; colOff {
col := colB*3 colOff
vars = append(vars, Var(fmt.Sprintf(varFmt, line, col, val)))
}
}
f = And(f, Or(vars...))
}
}
}
// Some spots already have a fixed value
f = And(
f,
Var("line-1-col-1:5"),
Var("line-1-col-2:3"),
Var("line-1-col-5:7"),
Var("line-2-col-1:6"),
Var("line-2-col-4:1"),
Var("line-2-col-5:9"),
Var("line-2-col-6:5"),
Var("line-3-col-2:9"),
Var("line-3-col-3:8"),
Var("line-3-col-8:6"),
Var("line-4-col-1:8"),
Var("line-4-col-5:6"),
Var("line-4-col-9:3"),
Var("line-5-col-1:4"),
Var("line-5-col-4:8"),
Var("line-5-col-6:3"),
Var("line-5-col-9:1"),
Var("line-6-col-1:7"),
Var("line-6-col-5:2"),
Var("line-6-col-9:6"),
Var("line-7-col-2:6"),
Var("line-7-col-7:2"),
Var("line-7-col-8:8"),
Var("line-8-col-4:4"),
Var("line-8-col-5:1"),
Var("line-8-col-6:9"),
Var("line-8-col-9:5"),
Var("line-9-col-5:8"),
Var("line-9-col-8:7"),
Var("line-9-col-9:9"),
)
model := Solve(f)
if model == nil {
fmt.Println("Error: solving grid was found unsat")
return
}
fmt.Println("The grid has a solution")
for line := 1; line <= 9; line {
for col := 1; col <= 9; col {
for val := 1; val <= 9; val {
if model[fmt.Sprintf(varFmt, line, col, val)] {
fmt.Printf("%d", val)
}
}
}
fmt.Println()
}
Output: The grid has a solution 534678912 672195348 198342567 859761423 426853791 713924856 961537284 287419635 345286179
Types ¶
type Formula ¶
type Formula interface {
String() string
// 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.
func Parse ¶
Parse parses the formula from the given input Reader. It returns the corresponding Formula. Formulas are written using the following operators (from lowest to highest priority) :
- for a conjunction of clauses ("and"), the ";" operator
- for an equivalence, the "=" operator,
- for an implication, the "->" operator,
- for a disjunction ("or"), the "|" operator,
- for a conjunction ("and"), the "&" operator,
- for a negation, the "^" unary operator.
- for an exactly-one constraint, names of variables between curly braces, eg "{a, b, c}" to specify exactly one of the variable a, b or c must be true.
Parentheses can be used to group subformulas. Note there are two ways to write conjunctions, one with a low priority, one with a high priority. The low-priority one is useful when the user wants to describe a whole formula as a set of smaller formulas that must all be true.
Example ¶
expr := "a & ^(b -> c) & (c = d | ^a)"
f, err := Parse(strings.NewReader(expr))
if err != nil {
fmt.Printf("Could not parse expression %q: %v", expr, err)
} else {
model := Solve(f)
if model == nil {
fmt.Printf("Problem is unsatisfiable")
} else {
fmt.Printf("Problem is satisfiable, model: a=%t, b=%t, c=%t, d=%t", model["a"], model["b"], model["c"], model["d"])
}
}
Output: Problem is satisfiable, model: a=true, b=true, c=false, d=false
Example (Unique) ¶
expr := "a & {a, b, c}"
f, err := Parse(strings.NewReader(expr))
if err != nil {
fmt.Printf("Could not parse expression %q: %v", expr, err)
} else {
model := Solve(f)
if model == nil {
fmt.Printf("Problem is unsatisfiable")
} else {
fmt.Printf("Problem is satisfiable, model: a=%t, b=%t, c=%t", model["a"], model["b"], model["c"])
}
}
Output: Problem is satisfiable, model: a=true, b=false, c=false
Example (Unsatisfiable) ¶
expr := "(a|^b|c) & ^(a|^b|c)"
f, err := Parse(strings.NewReader(expr))
if err != nil {
fmt.Printf("Could not parse expression %q: %v", expr, err)
} else {
model := Solve(f)
if model == nil {
fmt.Printf("Problem is unsatisfiable")
} else {
fmt.Printf("Problem is satisfiable, model: a=%t, b=%t, c=%t", model["a"], model["b"], model["c"])
}
}
Output: Problem is unsatisfiable
func Unique ¶
Unique indicates exactly one of the given variables must be true. It might create dummy variables to reduce the number of generated clauses.
Example ¶
f := And(Var("a"), Unique("a", "b", "c", "d", "e"))
model := Solve(f)
if model != nil {
fmt.Printf("Problem is satisfiable: a=%t, b=%t, c=%t, d=%t", model["a"], model["b"], model["c"], model["d"])
} else {
fmt.Printf("Problem is unsatisfiable")
}
Output: Problem is satisfiable: a=true, b=false, c=false, d=false
Source Files