计算机与数字工程
計算機與數字工程
계산궤여수자공정
COMPUTER & DIGITAL ENGINEERING
2009年
11期
4-6,78
,共4页
SAT问题%整数规划%线性规划%线性半定规划
SAT問題%整數規劃%線性規劃%線性半定規劃
SAT문제%정수규화%선성규화%선성반정규화
将线性半定规划应用到SAT问题的求解过程中.首先将SAT实例转化为整数规划问题,然后松弛为线性规划模型,最后再转化为一般的线性半定规划模型去求解.用SDPA-M软件求解线性半定规划问题后,规定了如何根据目标函数值去判定SAT实例和当CNF公式可满足时如何根据最优指派的概率x*i(i=1,…,n)去进行变元赋值,以期求得该公式的可满足指派.上述算法不仅可以判定SAT问题,而且对于符合算法规定可满足的CNF公式皆可给出一个可满足指派.求解SAT问题的线性半定规划算法在文章中被描述并被给予相应算例.
將線性半定規劃應用到SAT問題的求解過程中.首先將SAT實例轉化為整數規劃問題,然後鬆弛為線性規劃模型,最後再轉化為一般的線性半定規劃模型去求解.用SDPA-M軟件求解線性半定規劃問題後,規定瞭如何根據目標函數值去判定SAT實例和噹CNF公式可滿足時如何根據最優指派的概率x*i(i=1,…,n)去進行變元賦值,以期求得該公式的可滿足指派.上述算法不僅可以判定SAT問題,而且對于符閤算法規定可滿足的CNF公式皆可給齣一箇可滿足指派.求解SAT問題的線性半定規劃算法在文章中被描述併被給予相應算例.
장선성반정규화응용도SAT문제적구해과정중.수선장SAT실례전화위정수규화문제,연후송이위선성규화모형,최후재전화위일반적선성반정규화모형거구해.용SDPA-M연건구해선성반정규화문제후,규정료여하근거목표함수치거판정SAT실례화당CNF공식가만족시여하근거최우지파적개솔x*i(i=1,…,n)거진행변원부치,이기구득해공식적가만족지파.상술산법불부가이판정SAT문제,이차대우부합산법규정가만족적CNF공식개가급출일개가만족지파.구해SAT문제적선성반정규화산법재문장중피묘술병피급여상응산례.
