現在、z3 の python api を使用してビットベクトルの重みを計算しています。
st1より簡単な方法を Python API で検索した後、次の方法でビットベクトルの重み関数を実装しています。
Sum([( (st1 & (2**(i)))/(2**(i)) ) for i in range(bits)])
私の質問は比較的簡単です。より簡単で効率的な方法はありますか?
これらの重みの制約が 1500 以上含まれている問題があり、できる限り効率的に作業を進めたいと考えています。
編集：次の説明を追加します。計算しようとしているものには名前があります（ハミングウェイトです）。命令型言語で機能を実装する超効率的な方法があることは知っていますが、最終的には私が探しているものz3 ビットベクトルの個々のビットにアクセスするための基本的なメソッドがあるかどうかです。
質問に投稿した例で少し遊んでみました：
問題には多くの対称性があるように見えるため、不飽和インスタンスを解決するのは難しいと思います。その場合は、「対称性を破る制約」を含めることでパフォーマンスを向上させることができます。Z3 は、この種の問題に対して対称性を自動的に破ることはできません。
ここでは、マイナーなエンコーディングの改善があります。式((st1 & (2**(i)))/(2**(i))は基本的に i 番目のビットを抽出しています。Extract(i, i, st1)i 番目のビットを抽出するために使用できます。結果はサイズ 1 のビットベクトルです。次に、オーバーフローを避けるために「拡張」する必要があります。問題のビットベクトルには、最大で 28 ビットがあります。したがって、オーバーフローを回避するには 5 ビットで十分です。したがって、使用できますZeroExt(4, Extract(i, i, st1))。つまり、交換します
Sum([( (st1 & (2**(i)))/(2**(i)) ) for i in range(bits)])
と
Sum([ ZeroExt(4, Extract(i,i,st1)) for i in range(bits) ])
適度な 2 倍のスピードアップが得られます。したがって、Z3 はまだ 6 ビット unsat インスタンスを解決できません :(
再帰的な方法を試す必要があります。おそらく、この動的プログラミングを見てください。