問題タブ [constraint-programming]

Z3 Python 関数で 255 を超える引数を使用する方法を教えてください。

次の作業例では、一致したモデルを取得する方法は?

例: 次のソルバーとして

奇妙な質問が続きます。
私は学校で問題解決コンテストを行っており、コンピューターを使用することが許可されています。競技会でコーディングの仕方を知っているのは私だけなので、C と Pascal プログラムを使用して問題をより迅速に解決します。疑似コードからコードへの演習、アルゴリズム、コラッツ予想の検証などでそれを行いました。
さて、昨日、私は次の課題 (4 月 18 日) のトレーニングをしていて、Young タブローの演習を見ました。それは次のように表現されました（イタリア語から翻訳するために最善を尽くします）：
「Ferrers ダイアグラムは、1 つ以上の水平行に分散された N 個のボックスの構成であり、左揃えで、すべての行がその上の行と同じかそれよりも少ない数のボックスを含むように構成されています。これらの構成は、この画像のようなボックスの数: _{(ソース: olimpiadiproblemsolving.it )} 若いタブローは、1 から N までの整数で満たされた N 個のボックスの Ferrers ダイアグラムです。例: _{(ソース: olimpiadiproblemsolving.it )}







ボックス内の数字が行ごと、列ごとに昇順になるように並べ替えられている場合、テーブルは「標準」です (例: 1 番目、3 番目、5 番目のタブロー)。標準的なタブローでは、最初の行の最初のボックスには常に 1 が含まれます。N は常に、図のいずれかの行の左端のボックスにあります。


問題

[6,3,2,1,1,1] Ferrers ダイアグラムを考えてみましょう:
1) 1 行目の 6 番目のボックスに 6 が固定され、1 列目の最後のボックスに 11 が固定されている場合、標準的な方法で図を完成させますか?

2) 1 行目の 6 番目のボックスに 7 が固定され、1 列目の最後のボックスに 11 が固定されている場合、標準的な方法で図を完成させる方法はいくつありますか?

3) 1 行 6 番目のボックスに 8 が固定され、1 列目の最後のボックスに 11 が固定されている場合、標準的な方法で図を完成させる方法はいくつありますか?

」これらの数字と「-1」を「行末文字」として埋めた行列を使って、「タブローが標準になるように可能な限りすべての方法で埋めてください」とコーディングするにはどうすればよいですか?

リスト内の数値の繰り返しを制限するにはどうすればよいですか?

次のコード例で適切な制約は何ですか?

いくつかのサンプル クエリと予想される回答:

次のサンプルのように、非常に大きな Z3 python プログラムを実行しようとしています。

一致したモデルを取得するためにセット制約を使用しました。一致したモデルは、次のように関数の引数に基づいて取得されます。

しかし、次のエラーが表示されます

部屋、コース、日数の 3 つの要因に基づいて試験スケジュールを作成するのに問題があります。部屋数r、コースc、日dがあり、各日3枠あります。

学生のセットと学生からコースへのマッピングもあり、競合が発生することはありません。

このためのアルゴリズムを見つけようとしていますが、これが最大フローの問題に適合することがわかりました。このためのフロー ネットワーク グラフを作成するのに問題があります。

ありがとう

数値 X があり、Y+Z=X、Z*Y = 1 などの連立方程式を解きたいとします。

さて、これには解 Y=1/Z と Z = (sqrt(X*X-4)+X)/2 または (X-(sqrt(X*X-4)))/2 があります。

したがって、Prolog で次のように記述できます。

これは機能します。

しかし

基本的に事前に問題を解決し、Prolog に回答を評価してもらうだけです。

Xを事前に解かずに、ZとYを取得する方法はありますか?

私はちょうどのようなものを書くことはできません

インスタンス化エラーのため。