slove_流程图
2020-10-10 16:08:31 0 举报程序流程图
作者其他创作
大纲/内容
model.clear();confilct.clear();
否
!withinBudget()
certifiedUNSAT
exit(-1)
ok = false
是
nbSatCalls++;
incremental && certifiedUNSAT
status == l_Undef
model[i] = value(i);i++;
!ok
status == l_True
i < nVars()
status == l_False && conflict.size() == 0
status == l_False
model.growTo(nVars())；int i =0;
curr_restarts++
return status
开始
fclose(certifiedOutput)
return l_False
cancelUntil(0);
nbUnsatCalls++;
solves++;lbool status = l_Undef；打印参数
status = search(0)
0 条评论
下一页
