questions for beta users

[Scott Cotton]

Following the release of the gini sat solver on github, we've created a discussion group.

Gini is in beta, and in addition to ironing out any issues, we'd like to invite people to think about the interfaces, as we'd like to freeze them by the time of the first production release and then commit to backward compatibility thereafter.

Thanks,

Scott

[Burning Game]

Hi, Scott. Thanks for setting up this channel. I am a new user finding it a little bit hard to understand gini's design and interfaces.

The gini_test.go file is useful, but I still not clear about how to use z.Lit().

So can we get an example of a simple solve? Which I believe can help first-time users a lot.

Ex. https://github.com/mitchellh/go-sat

Thanks,

Boning

[Scott Cotton]

Hi Boning

Thanks for the question.

The README.md explains CNFs, and there it says that a literal is a Boolean variable or its negation.

Also, z.Lit is a type representing a literal.  The godoc for the package reads:

"""

Variables and literals are represented as uint32s. The LSB indicates for a literal whether or not it is the negation of a variable.

"""

which gives a low level way of creating variables and literals: eg z.Var(2).Pos() == z.Lit(4) && z.Var(2).Neg() == z.Lit(5).

But this is not very useful by itself, of course one wants to create formulas and solve them.

There are 2 main interfaces to constructing formulas to solve.  One is in CNF, using Add().  Gini.Add()'s docs give an example of adding

a clause.  (You can also construct a CNF formula for a solver in dimacs format using gini.NewDimacs).  So one can add all the clauses one likes and the call Solve() if your formula is in CNF.

The other interface is a circuit represented in gini/logic.C. here is one example in the docs for an equivalence check on a circuit.  Using circuits 

makes it easy to construct arbitrary form formulas.  Solving circuits requires using assumptions, as in the example.  I recommend using circuits unless you already have formulas in CNF.

Finally, the gini/gen package gives examples of pigeon hole principle problems and similar.

The docs for the Solve() and GoSolve() methods of the solver should be clear.

I hope this helps, and please do feel free to ask any other questions or raise an issue requesting features or documentation or anything else you feel would improve the interface.

Scott 

[Scott Cotton]

As a followup, since it seems you are maybe doing things with board games, 

I just pushed a godoc sudoku example to the gini package. 

Scott

[Burning Game]

Thanks so much for your sudoku example. It helps me a lot to understand how gini works with the help of this post:

https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/