README
¶
boolrecognition
Recognitation and transformation procedures for boolean functions written in Go.
Installation
First you have to install lpsolve (the linear program solver) and the Go bindings for lpsolve. Due to copyright problems lpsolve is not shipped with boolrecognition. You can find the installation instructions here. After this just use go get github.com/FabianWe/boolrecognition/... and then build the binary with go build cmd/benchmarklpb/benchmarklpb.go (from the directory FabianWe/boolrecognition).
Usage
Currenty benchmarklp accepts text files where each line contains an LPB in the format: First all the coefficients are separated by a space, then the threshold follows, also separated by a space.
So the LPB 2 ⋅ x1 + 1 ⋅ x2 + 1 ⋅ x3 ≥ 2 is represented by "2 1 1 2".
You can find benchmarks here. Example:
./benchmarklpb -lpb lpb_benchmarks/full/lpb/full_6.lpb -verify
(adjust the path to the lpb file). This uses the combinatorial solver (known to be not complete). To use the linear program solver use
./benchmarklpb -lpb lpb_benchmarks/full/lpb/full_6.lpb -verify -solver lp
For more options see ./benchmarklpb -help.
Documentation
¶
Overview ¶
Package boolrecognition is designed to recognize certain classes of boolean functions, but also provides functions to work with boolean functions.
State of the Project ¶
Currently we're working on solver for the so called threshold synthesis problem (transforming a minimal DNF to a linear pseudo-Boolean constraint). But we would welcome more contributions and other projects.
The code is contained in the subpackage lpb.
Components of this Package ¶
This package defines some base types, such as clauses (a set of literals) and clause sets (a set of clauses). We chose a simple form of representation: A clause is just a slice of integers and a clause set (DNF or CNF) is a slice of clauses. Thus each variable is identified by an integer id. How these ids are used may depend on the problem domain. For example it is ok to identify each variable with an integer 1 ≤ i ≤ n. Positive occurrences of i are denoted by i and negative occurrences of i are denoted by -i. Sometimes it also can be useful to start variable ids with 0 (for example for positive DNF only use positive integers 0 ≤ i < n).
Also some algorithm may require that the clauses (or even the DNF / CNF) are sorted in a particular way, make sure to document the code properly.
Winder matrix ¶
We implemented to so called winder matrix (Threshold Logic by Robert O. Winder).
Index ¶
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func BinSearch ¶
BinSearch performs a binary search on s to check if val is present. There is a similar function in the sort package (sort.Search), but this one uses a function as an argument. This makes the approach in sort slower, since binary search is a very simple procedure I've reimplemented it here.
This method will return the index of val in the slice if it is present and -1 if val is not present.
Some runtime comparisons (slice of size 100000): With sort.Search: 10130768 ns/op With this method: 7126174 ns/op which is a factor of ≈ 1.5
func CompareMatrixEntry ¶
CompareMatrixEntry returns two rows in a Winder matrix.
That is needed in order to sort the matrix later on. It returns -1 if row1 ≺ row2, 1 if row1 ≻ row2 and 0 if they're equal.
row1 ≺ row2 iff for the first entry where row1[i] and row2[i] are diffferent it holds that row1[i] < row2[i]. row1 ≻ row2 iff for the first entry where row1[i] and row2[i] are diffferent it holds that row[i] > row2[i].
Types ¶
type BooleanVector ¶
type BooleanVector []bool
func NewBooleanVector ¶
func NewBooleanVector(size int) BooleanVector
func (BooleanVector) Clone ¶
func (vector BooleanVector) Clone() BooleanVector
Clone returns a new boolean vector initialized with the contents of this vector.
func (BooleanVector) String ¶
func (vector BooleanVector) String() string
type Clause ¶
type Clause []int
Clause is a clause either in a CNF or DNF. It just stores all literals in a slice.
How the elements are stored in a clause is up to the implementation and problem specific. For example you might say that variables are identified by integers ≠ 0 and a positive occurrence of a variable v is expressed by storing v whereas ¬v is expressed by storing -a.
Or if you're dealing with only positive occurrences you might start your enumeration with 0.
It is however important to document this properly.
func NewClause ¶
NewClause returns an empty clause but with the capacity of the underlying slice big enough to hold initialCapacity variables.
type ClauseSet ¶
type ClauseSet []Clause
ClauseSet is a set of clauses, so a DNF or CNF (or whatever you have in mind...).
func NewClauseSet ¶
NewClauseSet returns an empty clause set but with the capacity of the underlying slice big enough to hold initialCapacity clauses.
func ParsePositiveDIMACS ¶
ParsePositiveDIMACS parses a clause set from the reader r. It returns the 'name' of the problem (the stuff right after the p in the problem line), the number of variables (nbvar) and the ClauseSet itself.
It only parses positive variables, i.e. negative occurrences of variables are not allowed and result in an error.
Variables are represented starting with 0, i.e. if you have the clause "c 1 4 7" in your DIMACS file this clause will be represented as {0, 3, 6}.
For more information on the DIMACS format see http://www.satcompetition.org/2009/format-benchmarks2009.html
func (ClauseSet) DeepSortedEquals ¶
func (ClauseSet) SortAll ¶
func (phi ClauseSet) SortAll()
SortAll will sort all clauses in increasing order.
func (ClauseSet) SortedEquals ¶
SortedEquals is a simple equality check for clause sets. It does compare literally each clause in the sets and checks if they're equal, therefore they should be sorted.
Also the clauses must be in the some ordering.
func (ClauseSet) WriteDIMACS ¶
WriteDIMACS writes the DNF in DIMACS format to the writer.
nbvar must be the number of variables in the DNF. If zeroBased is true we add 1 to each variable before writing (in DIMACS variables always start with 1).
type WinderMatrix ¶
type WinderMatrix [][]int
Class representing the Winder Matrix of a Boolean function in DNF representation.
For a positive Boolean function f := {x1, ..., xn} → {0, 1} and a DNF ϕ consisting of the prime implicants of f (so ϕ represents f) the Winder matrix of f is defined as the n × n matrix R s.t. r[i][d] is the number of prime implicants of f that contain the variable xi and contain d variables. (Definition from "Boolean Functions: Theory, Algorithms, and Applications" by Yves Crama and Peter L. Hammer)
For example consider the DNF ϕ ≡ { {x1, x2}, {x1, x3}, {x1, x4, x5}, {x2, x3, x4} }. The Winder matrix of ϕ (or better to say the function f it represents) is
0 2 1 0 0, 0 1 1 0 0, 0 1 1 0 0, 0 0 2 0 0, 0 0 1 0 0
For example the first row counts all occurrences of x1. So the two 2 comes from the fact that x1 occurs in two clauses of size 2.
The last two columns contain 0 everywhere because there is no clause of size 4 or 5.
The matrix as we compute it also contains an addition column that saves the id of the variable the corresponding row was created for, so we actually create the following matrix:
0 2 1 0 0 | 1, 0 1 1 0 0 | 2, 0 1 1 0 0 | 3, 0 0 2 0 0 | 4, 0 0 1 0 0 | 5
We will also assume that ϕ is zero based, meaning that
func NewWinderMatrix ¶
func NewWinderMatrix(phi ClauseSet, nbvar int, create bool) WinderMatrix
NewWinderMatrix returns a new winder matrix with the given size. That is it returns a matrix of size nbvar × nbvar + 1 (because in each colum) we also save the variable id.
The matrix gets initialized with the correct values if create = true. Otherwise the matrix will be initalized with 0 everywhere (excet the last row that becomes the variable id).
func (WinderMatrix) Create ¶
func (matrix WinderMatrix) Create(phi ClauseSet)
Create initializes the matrix with the DNF ϕ, that is it sets up the correct occurrences in the matrix.
func (WinderMatrix) Equals ¶
func (matrix WinderMatrix) Equals(other WinderMatrix) bool
func (WinderMatrix) Sort ¶
func (matrix WinderMatrix) Sort()
Sort sorts the whole matrix according to the ≻ order as defined in CompareMatrixEntry. That is the most important variable comes first etc.
This function is implemented with the sort package, however I read in Boolean Functions: Theory, Algorithms, and Applications by Yves Crama and Peter L. Hammer that the runtime can be improved here.
Source Files
Directories
¶
| Path | Synopsis |
|---|---|
|
cmd
|
|
|
benchmarklpb
Just for playing around a bit and testing stuff.
|
Just for playing around a bit and testing stuff. |
|
playground
Just for playing around a bit and testing stuff.
|
Just for playing around a bit and testing stuff. |
|
Package lpb provides solving algorithms for converting a minimal DNF ϕ to a so called linear pseudo-Boolean constraint (LPB).
|
Package lpb provides solving algorithms for converting a minimal DNF ϕ to a so called linear pseudo-Boolean constraint (LPB). |