diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-07 00:22:32 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-07 00:22:32 -0700 |
| commit | 998aeff15e96cc1b49ea7e7d21c8c7bc76ad7a23 (patch) | |
| tree | a3684d2f1afe502fdbf249da1d7eb85dad0e0c04 /src/aig/gia | |
| parent | 31b2e8bebd9a531d4a1a6a807436615e0497c75e (diff) | |
| download | abc-998aeff15e96cc1b49ea7e7d21c8c7bc76ad7a23.tar.gz abc-998aeff15e96cc1b49ea7e7d21c8c7bc76ad7a23.tar.bz2 abc-998aeff15e96cc1b49ea7e7d21c8c7bc76ad7a23.zip | |
Improvement to CNF encoding of cardinality constraints proposed by Mathias Soaken.
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/giaSatMap.c | 6 |
1 files changed, 6 insertions, 0 deletions
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 ) |