search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
391 stars 71 forks source link

get_core #76

Closed algebravic closed 3 years ago

algebravic commented 3 years ago

Which solvers can extract an unsolveable core? I have a few large sat problems which I'm solving (or proving to be unsat). When the problem is unsat, I extract a proof with the get_proof method and the core with the get_core method. The proofs work ok, but get_core always returns None. I've tried a few different solvers -- Cadical, Glucose3, Glucose4 and MapleCM, but they all give the same behavior. Do I have to set some sort of option before calling the solver? I'm using Python 3.9.1 on a mac running Big Sur, and the pysat version is '0.1.7.dev1'.

alexeyignatiev commented 3 years ago

@algebravic, unless I am missing something, all the solvers in PySAT should be able to report unsatisfiable cores. But since a core is a subset of the input set of assumption literals, in order to get a core, you need to make sure you give your solver such a set of assumptions when calling solve(). For details, see the description.

algebravic commented 3 years ago

Alex, Thanks for pointing out the reference. I wasn't completely clear on what a core was (as opposed to an MUS).

Victor