作者ric2k1 (Ric)
看板EE_DSnP
標題[公告] (更正) SatSolver::addXorCNF() in sat.h
時間Tue Jan 11 03:54:57 2011
底下 function 要改一下... (明天再更新 fraig.tgz)
// fa/fb = true if it is inverted
void addXorCNF(Var vf, Var va, bool fa, Var vb, bool fb) {
vec<Lit> lits;
Lit lf = Lit(vf);
Lit la = fa? ~Lit(va): Lit(va);
Lit lb = fb? ~Lit(vb): Lit(vb);
lits.push(~la); lits.push( lb); lits.push( lf);
_solver->addClause(lits); lits.clear();
lits.push( la); lits.push(~lb); lits.push( lf);
_solver->addClause(lits); lits.clear();
lits.push( la); lits.push( lb); lits.push(~lf);
_solver->addClause(lits); lits.clear();
lits.push(~la); lits.push(~lb); lits.push(~lf);
_solver->addClause(lits); lits.clear();
}
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 114.36.51.20