問題タブ [sat]

.SAT 形式を .3mf などの 3D 印刷ファイル形式に変換するモジュール/アプリケーションを構築したいと考えており、事前定義された関数を使用できるように ACIS カーネル上に構築したいと考えています。

ACIS カーネル ソース コードにアクセスできますが、どこから始めればよいかわかりません。彼らがRADFと呼ばれるこのフレームワークを持っていることは知っていますが、それが私が望むものに役立つかどうかはわかりません.

素朴な質問ばかりですが、答えていただけるとありがたいです。

1. カーネルに基づいてアプリケーションを構築するとはどういう意味ですか? VS、C# プログラミング言語を使用していて、ACIS カーネル ソース コードがあるとします。VS で新しいプロジェクトを開始し、その機能を使用できるように ACIS ライブラリを追加する必要がありますか? これについては、有益で有益な回答が本当に必要なので、事前に感謝します!

2. この状況で RADF は何をしますか? 必要ですか？C# を使いたい場合、必要ですか? (ACIS は C++ で記述されているため)

3. 前の質問に対する答えが「はい」の場合、RADF および SPADotnet ソリューションを構築するための支援が本当に必要です。経験者の方がいらっしゃいましたら質問させていただきます。

4. アプリケーションの出力を .3mf ファイルにしたいと言ったのですが、コンソーシアムによって開発された .3mf ソース コードを使用しなければならないということですか? (GitHub にあるもの)

最後に、オンラインのドキュメントやその他のものを読んで、これらのことを本当に学ぼうとしていると言いたいのですが、答えが見つかりません。

私はミニサットのソースを研究していますが、ここにはフォローインライン機能があります

入力として整数 var (DIMAC ファイルの整数) を受け取り、リテラル p を返します。なぜ var に var が追加され、次に符号が追加されるのかわかりません。それを理解するのを手伝ってくれませんか？

Z3 で仮定を表現する方法はありますか (私は Z3Py ライブラリを使用しています)、エンジンがそれらの有効性をチェックせず、定理の証明のように、それらを基礎となる理論として採用するようにしますか?

たとえば、Real 型の引数を持つ 2 つの単項関数があるとします。すべての入力値について、f1(t) が f2(t) と等しいことを Z3 エンジンに伝えたいと思います。

次のような Z3Py でエンコードされます:
t = Real("t"
)

提示されたコードの問題は、アサーション セットが非常に大きく、量指定子を使用していることです (リアルタイム システムの充足可能性を証明しようとしています)。上記のアサーションを他のアサーションのセットに追加すると、チェック手順が終了しません。

モデルで Alloy を呼び出し、返されたインスタンスで何かを行う必要があるプログラムを作成しています。問題は、Alloy コマンドが呼び出されるたびに Alloy インターフェイスが開かれることです。インターフェイスを開かずにJavaコードからAlloyを呼び出すことができる方法があるかどうか疑問に思っています。

私の理解では、インクリメンタル SAT 解法は、互いに非常に近いさまざまなモデルを評価するのに役立ちます。

これを使用してモデルを評価し、後で変更した場合は、以前のソリューションを使用して再評価し、より迅速な結果を得たいと考えています。しかし、さまざまな SAT ソルバー (Sat4J、Minisat、mathsat5) を調べたところ、すべてのモデルが 1 回の実行で提示された場合にのみ、漸進的に解決できるようです。

私はSATの解決にかなり慣れていないので、何かを見落としているかもしれません。後で使用するために解決インスタンスを保存する方法はありませんか? インスタンスを閉じると、すべての学習が失われますか?

SAT2016 を定義 = {\phi | \phi は、最大で 2016 句を含む CNF 式です}。P \neq NP を仮定すると、SAT2016 は NP 完全ですか?

各節のリテラルの数は制限されていないため、節の数が一定に制限されている式の充足可能性をチェックするための多項式時間アルゴリズムが存在するかどうかはすぐにはわかりません。

あなたのアイデアは大歓迎です。