search

conp-solutions / riss

Riss SAT Solver
GNU Lesser General Public License v2.1
8 stars 5 forks source link

modelcount,simplify: limit keep vars #20

Closed conp-solutions closed 2 years ago

conp-solutions commented 2 years ago

We might need to keep only a given subset of variables stable during simplification, e.g. the first N variables. Add such a capability to the simplification scrpit, to support use cases like projected model counting.

Signed-off-by: Norbert Manthey nmanthey@conp-solutions.com

conp-solutions commented 2 years ago

To simplify a formula, only keeping the first N variables 'stable':

./coprocessor-for-modelcounting.sh -o simp.cnf -k 2 -t test.cnf

(simplify formula test.cnf, print to ismp.cnf, keep the variables 1..2 stable)