search

cjdrake / pyeda

Python EDA
BSD 2-Clause "Simplified" License
305 stars 55 forks source link

Feature Request: MUS extraction (through picomus) #123

Closed sschnug closed 7 years ago

sschnug commented 9 years ago

At least the current release of picosat (960) includes picomus, a tool to extract a minimal unsatisfiable core' also known as 'minimal unsatisfiable set' (MUS).

In my opinion, this could be very helpful when debugging SAT-models.

Would it be possible to include this to pyeda? I don't know how pyeda uses picosat internally and can't estimate the amount of work this will need.

cjdrake commented 9 years ago

Could you please provide some background? For example, how are you currently using pyeda, and how will this help you accomplish your goal? Also, any relevant info about minimal unsatisfiable sets.

sschnug commented 9 years ago

Well, no magic involved :-)

My personal usage:

I'm using SAT-solvers erratically to tackle discrete-optimization problems (not part of my job; more or less recreationally). Examples: Edge-Matching, Graph coloring, Mahjong-Solitaire and much more....

I discovered pyeda and i'm trying to evaluate if it helps my with my workflow or if some customized code works better. So far, pyeda's general ability to build cnf-formulas (in emergency cases: tseitin-transformation) seems to work well for me (in terms of implementation time). A lot of features are not that important for me (BDDs, Espresso Minimization...; these seem to be more common in circuit-desing), others are missing and maybe i will think about implementing these on top of pyeda (cardinality-constraints; some circuit-based, some based on sorting-networks...).

Minimal Unsatisfiable Core

I don't have experience with this concept, but to my understanding (i think i can't tell you more than what you will learn within 3 minutes of googling), a MUS is a UNSAT subset of the original clauses, where each subset of this subset will be SAT (Wiki).

How would it (possibly) help me?

During my modelling phase, a lot of debugging is needed. Often some constraints are redundant or just wrong and produce UNSAT where i feed it with instances which are guaranteed to be SAT. There is a similar idea used in LP/MIP for debugging these faulty models: irreducible infeasible subsystem (IIS) (compare Link). In general i just want to try the MUS-capabilities to recognize which part of my constraints are contradicting each other.

Thanks for reading and all your work on this promising library!

cjdrake commented 9 years ago

Scanned the picomus source code just now. I would say it's a medium-complexity task. All that's required is to copy Armin Biere's methodology from picomus.c, but it takes some effort to integrate that using the Python C API, translate data structures and so forth. Lately, I've been investigating how to use cffi to make this kind of programming a bit easier.

Can't give an estimate, but would gladly entertain a pull request from a volunteer.