new features

[Scott Cotton]

Hi all,

There is a branch of gini I'm working on that adds some new features.  In particular,

there is support for recyclable activation literals and an interface for plugging in 

cnf simplifiers.  The latter is pretty bare-bones, and doesn't allow for 

model or proof reconstruction or anything yet, but it does allow to add and remove clauses in a way that interleaves with incremental calls to solve.

If there are any thoughts about next steps, would love to hear them.

--

Scott Cotton

http://www.iri-labs.com

[Burning Game]

Hi, Scott:

I looked through gini's doc but didn't find any clue if gini can tell me how many solutions there are for a sat problem.

I found it in gophersat. https://github.com/crillab/gophersat

Since I am pretty new, I am not sure if I missed its information or this can be a new feature.

Thanks,

Boning

[Scott Cotton]

Hi Boning,

Gini does not currently support model counting.  Model counting, as well as the related providing 

justifications/{0,1,x}- models that maximise the number of 'x' variables in a model, would be nice to add 

to gini.

Not sure when I can add those things, but doing so is not as involved as say adding proofs and proof checking or in-processing, so it is possible in the not so distant future. 

I'm curious to know if model counting is an important feature for you?

Scott

--
You received this message because you are subscribed to the Google Groups "gini sat solver" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ginisat+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ginisat/64881028-b206-4f97-9ba1-eea83f5146fc%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Burning Game]

Hi, Scott:

I agree that this may not be an essential feature to gini. But yes, knowing all the solutions, not only sat/not sat, can do more help to me. 

I am implementing a random data generator, gini can help me decide if there is a valid output. Knowing all the solutions means I can find all valid outputs. 

Since I am pretty new to sat solver, there might be alternatives I don't know.

Boning

[Scott Cotton]

Hi Boning,

My experience has been that SAT solvers are fast because they are built to answer yes/no existential queries 

(does there exist a solution?).  If one actually needs to represent the full set of solutions, often binary decision diagrams are a better choice, but they can blow up in space whereas a SAT solver will never need exponential space, and so they have been replaced by SAT solvers over time as people have figured out how to attack problems by not needing all solutions but rather using existential queries.

That said, here are some thoughts that might help.

- model counting is not the same thing as knowing all solutions and SAT based techniques are good.

- for CNF random solution generation, this paper may be of interest.

- Also here are some slides on a more recent counting paper

- If you have a circuit like gini/logic.C which isn't too hard to satisfy, then plain old simulation (see methods Eval and Eval64) can sample solutions very quickly.  Note that AIG/non-CNF structure can confuse the CNF based methods above because of the distinction between inputs (actual variables) vs and-nodes/gates (variables in CNF but which are functions of the inputs).

Scott

To view this discussion on the web visit https://groups.google.com/d/msgid/ginisat/751fc53f-b84f-4786-91d6-6537fdbe7731%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

[Burning Game]

Thank you Scott for those helpful links which I am currently looking into. 

Although not efficient, I think enumerate is not hard to implement by adding new solutions to original clauses iteratively.

Boning

[Scott Cotton]

---------- Forwarded message ---------
From: Scott Cotton <w...@iri-labs.com>
Date: Tue, 11 Dec 2018 at 18:12
Subject: Re: new features
To: Burning Game <sdi...@gmail.com>

Hi Boning,

If you are only interested in a subset of the variables, like the outputs to a circuit, then you can 

also restrict the blocking clauses you add to those variables.  

Scott

To view this discussion on the web visit https://groups.google.com/d/msgid/ginisat/dbb54215-5c13-4c35-b1e6-8298195bd59a%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

--

Scott Cotton

http://www.iri-labs.com

--

Scott Cotton

http://www.iri-labs.com