Trevor Hansen

@rgov, when I read it, what sticks out to me is the "additionally" part: > The C library at the core of this Perl module can additionally > be used,...

Personally if Bit::Vector is licensed under either artistic licence, it seems enough to me. Both have clauses (see below) which mean people can modify and distribute STP pretty much however...

Because the licence that Bit::Vector includes in its package is the artistic licence 1.0. It seems that we have just one question for Steffen: Is the C code in Bit::Vector...

STP does some simplifications which preserve satisfiability, but not the number of solutions. Unconstrained variable elimination & polarity analysis come to mind, no doubt there's others too. So the CNF...

Thanks for explaining @msoos. It sounds like we need two things to use STP for solution counting: 1) We need STP to not alter the number of solutions. 2) We...

I feel like we should be able to agree on some of these changes. As a start, can anyone see issues if we: * As @rgov mentioned, remove the "begin...

> I (genuinely) think the best way to resolve this issue is to drop the authors bit from the top of each file and do this: > If the file...

I've added the latest results in - stp/stp.github.io@29d546f8b76ec0085a9fcd2e2abc68acc9033bd3

It seems like the '-' character isn't allowed in variables names in the CVC language. The modern CVC4 can't parse the example instance either. Looking quickly at the history, STP...

hi @pseudo-aloha, I don't know to fix your problem, but a suggestion that might let you avoid the problem it is to build the STP executable with Docker and then...