From 998aeff15e96cc1b49ea7e7d21c8c7bc76ad7a23 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 7 Jun 2016 00:22:32 -0700 Subject: Improvement to CNF encoding of cardinality constraints proposed by Mathias Soaken. --- src/aig/gia/giaSatMap.c | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src') diff --git a/src/aig/gia/giaSatMap.c b/src/aig/gia/giaSatMap.c index 56f739d8..0ddd4a39 100644 --- a/src/aig/gia/giaSatMap.c +++ b/src/aig/gia/giaSatMap.c @@ -314,6 +314,12 @@ static inline void Sbm_AddCardinConstrMerge( sat_solver * p, int * pVars, int lo Sbm_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars ); for ( i = lo+r; i < hi-r; i += step ) Sbm_AddSorter( p, pVars, i, i+r, pnVars ); + for ( i = lo+r; i < hi-r-1; i += r ) + { + lit Lits[2] = { Abc_Var2Lit(pVars[i], 0), Abc_Var2Lit(pVars[i+r], 1) }; + int Cid = sat_solver_addclause( p, Lits, Lits + 2 ); + assert( Cid ); + } } } static inline void Sbm_AddCardinConstrRange( sat_solver * p, int * pVars, int lo, int hi, int * pnVars ) -- cgit v1.2.3