ログイン
編集不可のページディスカッション情報添付ファイル

2015-04-27 21:41:08時点のリビジョン1

メッセージを消す
CTF/Toolkit/z3py
MMA

z3py

Z3はMicrosoft Researchの開発した，SAT・SMTソルバである． ブール代数の充足問題に限らず，整数計画問題などにも適用が可能である．

目次

  1. z3py
    1. インストール
    2. 基本的な流れ
    3. 変数の作成
      1. ブール変数を作る
      2. 整数変数を作る
    4. 制約の設定
      1. 条件の追加
      2. AND
      3. OR
      4. イコール
      5. 不等式
    5. 解を得る方法
      1. ブール変数の解を得る
      2. 整数変数の解を得る

インストール

基本的な流れ

変数の作成

ブール変数を作る

整数変数を作る

制約の設定

条件の追加

AND

OR

イコール

不等式

解を得る方法

ブール変数の解を得る

整数変数の解を得る