SAT Hard制約中に得たFixed LitsをSAT SOFT制約に投入してもよいか？

 Q.SATでHARD制約のみでSAT解を得た時のレベル０STACKをFIXEDLITSとして得る。SOFT制約を追加して、SAT SOLVEするが、前FIXEDLITSをADDしても厳密性は失われないか？

結論から言うと：

HARD 制約だけで得たレベル 0 の FIXED LITS（＝レベル 0 で強制される単位伝播の結果）を、 SOFT 制約を追加した後の SAT SOLVE にそのまま ADD しても、 厳密性（soundness）は一切失われません。

むしろ レベル 0 の FIXED LITS は「HARD 制約から論理的に必然な真理」なので、 SOFT 制約を追加しても常に保持すべき情報 です。

🎯 結論（最重要）

• レベル 0 の FIXED LITS は HARD 制約から論理的に導かれる必然の事実

• SOFT 制約は目的関数を変えるだけで、HARD 制約の論理的帰結を壊さない

• よって レベル 0 の FIXED LITS を再投入しても soundness は完全に保たれる

🔍 なぜ soundness が保たれるのか（論理的理由）

◆ 1. レベル 0 の FIXED LITS とは何か？

レベル 0 の割り当ては：

• HARD 制約だけで単位伝播した結果

• どんな SAT 解でも必ず満たさなければならない真理

• つまり HARD 制約の論理的帰結（logical consequences）

形式的には：

$$\text{HARD}\models l$$

という形で表せる。

◆ 2. SOFT 制約は「目的関数」または「優先度」を追加するだけ

SOFT 制約は：

• 満たされなくてもよい（ただしペナルティがある）

• HARD 制約の論理的帰結を壊すことはない

つまり SOFT 制約を追加しても：

$$\text{HARD}\models l$$

は変わらない。

◆ 3. よって FIXED LITS を再投入しても soundness は壊れない

なぜなら：

• FIXED LITS は HARD 制約の論理的帰結

• SOFT 制約は HARD 制約を弱めない

• したがって FIXED LITS を追加しても 本来存在する最適解を排除しない

つまり soundness が保たれる。