Уникальные тесты

Этот вопрос, вероятно, находится на границе между темой и темой, однако я видел подобные вопросы здесь, поэтому я задам его.

Я реализую уникальный $k$ -SAT-решатель, вход которого представляет собой формулу $k$ -CNF, имеющую не более $1$ удовлетворительного назначения. Чтобы проверить его практическое поведение, мне нужен набор таких формул. Я искал их в Интернете и ничего не нашел (хотя, с другой стороны, очень легко найти наборы обычных формул $k$ CNF).

Где я могу найти уникальные экземпляры $k$ -SAT?

В качестве альтернативы я хотел бы также знать любую процедуру для генерации уникально удовлетворяемых экземпляров. Единственный подход, о котором я знаю, идет под именем генерации установленного экземпляра SAT : вы случайным образом генерируете назначение $n$ переменных, а затем генерируете только те предложения, которые согласуются с таким назначением. Этот подход неудовлетворителен для моих целей по следующим причинам:

• Полученная формула может иметь дополнительные нежелательные удовлетворяющие назначения.
• Чтобы быть уверенным, что формула однозначно удовлетворяется желаемым присваиванием, вы должны ввести все возможные пункты, которые с ней согласны. Это приведет к получению формул со слишком большим количеством предложений, которые, вероятно, будет легко решить и, следовательно, не будут отражать поведение решателя в худшем случае. Для меня не очевидно, как мы можем эффективно навязывать уникальность, сохраняя при этом разумное количество пунктов.

Как мы можем генерировать однозначно выполнимые формулы с разумным количеством предложений? Под разумным я подразумеваю далеко от максимума .$2^k \cdot {n \choose k}$

Вот один из способов генерирования уникального экземпляра -SAT, учитывая экземпляр SAT φ, который, как вы знаете, выполним. Рассмотрим формулу ф ( х ) , данное$k$$\varphi$$\psi(x)$

где является хэш - функция , которая отображает задание х к к -битных значение (для некоторого малого значения к ), и у является случайной K значения -битный. Если φ имеет около 2 k удовлетворяющих заданий, то (эвристически) мы предполагаем, что ψ будет иметь только одно удовлетворяющее присваивание (с постоянной вероятностью). Мы можем проверить, является ли это случаем, используя решатель SAT (а именно, проверить, является ли ψ выполнимым; если это так, и x 0 является одним удовлетворяющим назначением, проверить, является ли ψ ( x ) ∧ $h$$x$$k$$k$$y$$k$$\varphi$$2^k$$\psi$$\psi$$x_0$ выполнимо). Если k не известно, вы можете найти k с помощью бинарного поиска или просто итерируя по каждому значению-кандидату k = 1 , 2 , … , n (где n - число булевых переменных в x ).$\psi(x) \land x \ne x_0$$k$$k$$k=1,2,\dots,n$$n$$x$

Вы можете свободно выбирать хэш-функции. Возможно, вы захотите сделать это как можно проще. Одна чрезвычайно простая конструкция состоит в том, чтобы выбрал случайное подмножество k битов из x . Немного более сложная конструкция состоит в том, чтобы i- й бит h ( x ) был xor двух случайно выбранных битов из x (выбирая отдельную пару позиций бит для каждого i , независимо). Сохранение h простым будет ψ относительно простым.$h$$k$$x$$i$$h(x)$$x$$i$$h$$\psi$

Этот вид преобразования иногда используется / предлагается, как часть схемы для оценки числа удовлетворяющих присвоений формуле ; Я адаптировал это для вашей конкретной потребности.$\varphi$

В Интернете можно найти множество тестовых стендов экземпляров SAT, и вы можете применить это преобразование ко всем из них, чтобы получить коллекцию уникальных экземпляров -SAT.$k$

Другой возможностью было бы создание уникальных экземпляров -SAT из криптографии. Например, предположим, что f : { 0 , 1 } n → { 0 , 1 } n является криптографической односторонней перестановкой. Пусть x - случайно выбранный элемент из { 0 , 1 } n , и пусть y = f ( x ) . Тогда формула φ ( x ) определяется как f ( x ) $k$$f:\{0,1\}^n \to \{0,1\}^n$$x$$\{0,1\}^n$$y=f(x)$$\varphi(x)$ является уникальнымэкземпляром k -SAT. В качестве другого примера,случайным образомвыберите два больших простых числа p , q и пусть n = p q . Тогда формула φ ( x , y ), заданная как x ⋅ y = n ∧ x > 1 ∧ y > 1 ∧ x ≤ y (с очевидным соответствием между битовыми строками и целыми числами), является уникальной$f(x)=y$$k$$p,q$$n=pq$$\varphi(x,y)$$x \cdot y = n \land x>1 \land y>1 \land x \le y$$k$-SAT экземпляр. Тем не менее, эти конструкции не кажутся полезным способом для сравнения или оптимизации вашего решателя. Все они имеют особую структуру, и нет никаких оснований полагать, что эта структура является представителем реальных проблем. В частности, известно, что экземпляры SAT, извлеченные из криптографических задач, чрезвычайно сложны, намного сложнее, чем экземпляры SAT, взятые из многих других реальных приложений решателей SAT, поэтому они не являются хорошей основой для сравнительного анализа вашего решателя.

В целом, все методы, упомянутые в этом ответе, имеют недостаток, заключающийся в том, что они генерируют уникальные экземпляры -SAT с определенной структурой, поэтому они могут быть не тем, что вы ищете, или, по крайней мере, вы можете не захотеть полагаться исключительно по формулам, сгенерированным таким образом. Лучшим подходом было бы определить приложения Unique k -SAT (кто, по вашему мнению, будет использовать ваш решатель и для каких целей?), А затем попытаться получить некоторые реалистичные примеры из этих областей применения.$k$$k$

Для связанной темы, см. Также Создание интересных задач комбинаторной оптимизации

Вы могли бы рассмотреть алгоритмы, которые используются для генерации головоломок Судоку - предположительно, обобщенные до - поскольку (обычно) головоломки Судоку должны иметь уникальное решение. С другой стороны, у головоломок Судоку обычно гарантированно есть хотя бы одно решение ... Но обнаружение этого решения все же может стать хорошим эталоном для вашего решателя.$n \times n$

Вы можете использовать генератор судоку вместе с сокращением до SAT, или вы можете подумать о том, как применить методы, используемые при создании судоку, для более непосредственного создания уникальных экземпляров SAT. Что касается первого, очевидно, что ваши экземпляры SAT будут иметь некоторую структуру, но мне неясно, является ли она более или менее структурной, чем, например, установка решения или использование техники изоляции свидетеля. Вероятно, зависит от ваших потребностей и вашего решателя.

Единственное упоминание, о котором я здесь знаю, это: Создание головоломок судоку: от легкого к злому .

Я думаю, что хорошим тестовым примером было бы генерировать случайные однозначно удовлетворяемые экземпляры 3XOR (посаженные экземпляры) с ограничениями а затем преобразовывать их в экземпляры 3SAT.$\Theta(n)$

imho Один из лучших способов создать «предположительно сложные» экземпляры SAT при управлении количеством решений - это использовать целочисленные факторинговые экземпляры / схемы, закодированные в двоичном виде. код не очень сложен, он использует в основном схемы сложения EE и не приводит к «большим» экземплярам SAT. количество решений равно количеству факторов (включая «перестановки» факторов). поэтому простые числа порождают ровно два решения: . одно решение может быть гарантировано при дальнейшем «сравнении» ограничение , которое ограничивает факторы , которые $(1,p),(p,1)$$a<b$$a \neq 1$$b \neq p$ .

Также при таком подходе это относительно легко найти номера с примерно однако многие факторы / растворы. чем «ровнее» число, тем больше факторов.

Различные исследователи на протяжении многих лет создавали этот код SAT факторинга (например, для соревнований DIMACS / arcihve, в котором хранились некоторые случаи факторинга в прошлом), но, к сожалению, эта версия не является общедоступной. см. также 1-ю ссылку ниже для ссылки, где код был написан / реализован, очевидно, для аспирантуры.

• Сведение задачи целочисленной факторизации к задаче NP-Complete
• Генерация схемы 3SAT для примера факторизации целых чисел

another empirical/iterative approach that may be useful for some, to create more "unstructured" instances: create random SAT instances $e_n$ near the transition point (the region where the equation has a probability 50% between "solvable and unsolvable"), and then solve the equation. if it is unsolvable, throw away and restart. if it is solvable, add clauses that restrict the solution "not" to be the found solution, obtaining $e_{n+1}$, and re-solve. repeat if necessary. when the equation $e_{n+1}$ is no longer solvable, the $e_n$ must have had a single/unique solution.

You can easily generate directly Unique SAT formulas with reasonable size $(|F|<n+2^k)$

Let $m$ be the unique model - say $m$ contains only "0"s (rename the variables later if needed).
Let $F$ a $k$-SAT formula satisfied only by $m$ - the maximum size of $F$ is the total number of clauses satisfied by $m$ i.e. $(2^k-1) \binom{n}{k}$.

Take the $\binom{k}{1}$ clauses that eliminate all models assigning exactly one "1" among $x_1,x_2 \ldots x_k$:
$(\lnot x_1, x_2 \ldots x_k)(x_1, \lnot x_2 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_k)$

Take the $\binom{k}{2}$ clauses that eliminate all models assigning exactly two "1" among $x_1,x_2 \ldots x_k$:
$(\lnot x_1, \lnot x_2, x_3 \ldots x_k)(\lnot x_1,x_2, \lnot x_3 \ldots x_k)\ldots (x_1,x_2 \ldots \lnot x_{k-1} \lnot x_k)$

Keep going until taking the only $\binom{k}{k}$ clause that eliminates all models assigning "1" to each variables among $x_1,x_2 \ldots x_k$.

The only models which are not yet eliminated assign all $x_1,x_2 \ldots x_k$ to "0". Since $m$ is a model, then take any set of $n-k$ clauses that eliminate all models assigning "1" to $x_i (k<i\leq n)$ and $0$ to any $k-1$ variables among $x_1,x_2 \ldots x_k$, for instance:
$(\lnot x_{k+1}, x_1 \ldots, x_{k-1}) \ldots (\lnot x_n, x_1 \ldots x_{k-1})$.

Then $|F|=\sum_{i=1}^k \binom{k}{i} +n-k = 2^k-1+n-k$

To get more clauses, add any clause containing at least one negated variable. To get an unsatisfiable formula, just add a clause with $k$ unnegated variables.