Victor S. Miller

Parallel runs

2

I would like to run a large number of experiments. Since I have a number of CPUs and GPUs available, I'd like to run them in parallel. I didn't see...

Support for relaxations

2

I would like to ask that the following features be added for relaxations: 1) Lagrangian relaxations. It would be nice to have a model, plus a specific set of constraints...

Since I have a lot of latex in my org files, I routinely have lines at the beginning like #+latex_header: \newcommand{\BB}{\mathbb{B}} These definitions are necessary for the TeX to be...

Using solvers that are obtained by other means (such as homebrew)

1

A number of solvers on your list (such as z3, yices, etc.) have more recent versions installed either via homebrew, or via github. Is there any way to have pysmt...

negate

3

The following has been puzzling me for days, until I saw a subtlety. I wanted to generate a not equals constraint. So I took the clauses generated by `CardEnc.equals`, and...

Support for lexicographic constraints

3

It would be nice if you had support for lexicographic comparison between two lists of literals, somewhat analogous to the support that you have for cardinality constraints.

random seeds in solvers

3

Most (all?) of the solvers use randomness, and have a command option to set the random seed, for reproducibility. What does pysat do about that? It would be nice to...

Solver version information

2

I've been using pysat to do some systematic exploration on the effect of encodings for a particular class of combinatorial problems. I've run a bunch of solvers with all combinations...

Time out for sat solvers

1

From the documentation one can use solve_limited with expect_interrupt to get a SAT solver to terminate for some external reason -- like a time limitation. However, not all of the...

I just found pyhsmm last week. First a minor issue: It looks like future is not installed by default in anaconda's distribution of python, so that pip install pyhsmm fails,...