gophersat: github.com/crillab/gophersat/bf

## package bf

`import "github.com/crillab/gophersat/bf"`

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.

### func Dimacs¶Uses

`func Dimacs(f Formula, w io.Writer) error`

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".

Code:

```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¶Uses

`func Solve(f Formula) map[string]bool`

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.

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"))))))
model := Solve(f)
if model != nil {
fmt.Printf("Problem is satisfiable")
} else {
fmt.Printf("Problem is unsatisfiable")
}```

Output:

```Problem is satisfiable
```

Code:

```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
```

### type Formula¶Uses

```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.

#### func And¶Uses

`func And(subs ...Formula) Formula`

And generates a conjunction of subformulas.

#### func Eq¶Uses

`func Eq(f1, f2 Formula) Formula`

Eq indicates a subformula is equivalent to another one.

#### func Implies¶Uses

`func Implies(f1, f2 Formula) Formula`

Implies indicates a subformula implies another one.

#### func Not¶Uses

`func Not(f Formula) Formula`

Not represents a negation. It negates the given subformula.

#### func Or¶Uses

`func Or(subs ...Formula) Formula`

Or generates a disjunction of subformulas.

#### func Parse¶Uses

`func Parse(r io.Reader) (Formula, error)`

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.

Code:

```expr := "a & ^(b -> c) & (c = d | ^a)"
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
```

Code:

```expr := "a & {a, b, c}"
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
```

Code:

```expr := "(a|^b|c) & ^(a|^b|c)"
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¶Uses

`func Unique(vars ...string) Formula`

Unique indicates exactly one of the given variables must be true. It might create dummy variables to reduce the number of generated clauses.

Code:

```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
```

#### func Var¶Uses

`func Var(name string) Formula`

Var generates a named boolean variable in a formula.

#### func Xor¶Uses

`func Xor(f1, f2 Formula) Formula`

Xor indicates exactly one of the two given subformulas is true.

Package bf imports 9 packages (graph) and is imported by 3 packages. Updated 2020-03-20. Refresh now. Tools for package owners.