gophersat: github.com/crillab/gophersat/bf Index | Examples | Files

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.

Index

Examples

Package Files

bf.go doc.go parser.go

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

Code:

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

Code:

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 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 2019-07-03. Refresh now. Tools for package owners.