独特的3sat解决方案示例

Question

我正在寻找具有独特解决方案的 3sat 问题。到目前为止，我只找到一个网站 https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

该网站上有很好的 3sat 实例示例，但问题是如果可以满足的话，他们有不止 1 个解决方案。我想要 3sat 的这么大的实例，有 20 40 个变量和至少 100 个子句（越多越好）但是有独特的解决方案。我在哪里可以得到这样的问题列表或者是否有任何算法可以生成具有独特解决方案的3sat问题？

Answer 1

要构建具有唯一解决方案的 3SAT 问题，您可以使用算术电路，如 adder 或 multiplier。然后使用数字比较器将所得输出线与已知结果进行比较。

设计流程如下：

写出要使用的算术表达式。
示例：x * 7、x - 1、x * x
将表达式转换为逻辑门的布尔电路。
这可以通过合适的 python 脚本来完成。
将电路变换为合取范式（CNF）使用像 bc2cnf 这样的工具。
如果结果子句数量太大或太少，返回步骤 1. 并调整表达式操作数的位长。

这种电路最简单的变体是没有预先连接算术电路的数字比较器。

要得到唯一解，算术表达式必须有唯一解。反例包括整数除法和整数平方根。

Answer 2

https://it-in-industry.com/itii_papers/2019/7219itii03.pdf讨论了生成独特的 3-sat 问题。可能是一个很好的起点。

Answer 3

要获得唯一解的 3SAT 问题：

选择任何变量

a、b、c、d、e、f
为这些变量选择任意值（此时，我们已经有了解决方案）

a = 真，b = 假，c = 真，d = 真，e = 假，f = 假
为每个变量创建一个单位子句，并具有令人满意的文字（此时，我们已经遇到了这个简单的问题）
```
(a) ∧
(¬b) ∧
(c) ∧
(d) ∧
(¬e) ∧
(¬f)
```

通过在一个子句上添加另一个变量的文字并在另一个子句上添加相反的文字来复制某些子句

(a ∨ ¬b) ∧
(a ∨ b) ∧
(¬b) ∧
(c ∨ a) ∧
(c ∨ ¬a) ∧
(d) ∧
(¬e ∨ ¬b) ∧
(¬e ∨ b) ∧
(¬f ∨ e) ∧
(¬f ∨ ¬e)

再做一次

(a ∨ ¬b ∨ ¬c) ∧
(a ∨ ¬b ∨ c) ∧
(a ∨ b) ∧
(¬b) ∧
(c ∨ a ∨ e) ∧
(c ∨ a ∨ ¬e) ∧
(c ∨ ¬a ∨ ¬b) ∧
(c ∨ ¬a ∨ b) ∧
(d) ∧
(¬e ∨ ¬b ∨ f) ∧
(¬e ∨ ¬b ∨ ¬f) ∧
(¬e ∨ b) ∧
(¬f ∨ e) ∧
(¬f ∨ ¬e ∨ a) ∧
(¬f ∨ ¬e ∨ ¬a)

融化它

(¬b ∨ a ∨ ¬c) ∧
(d) ∧
(¬f ∨ ¬e ∨ ¬b) ∧
(¬e ∨ ¬f ∨ ¬a) ∧
(¬f ∨ e) ∧
(c ∨ ¬e ∨ a) ∧
(¬a ∨ c ∨ b) ∧
(¬e ∨ f ∨ ¬b) ∧
(a ∨ c ∨ ¬b) ∧
(c ∨ ¬b ∨ ¬a) ∧
(b ∨ ¬e) ∧
(a ∨ c ∨ e) ∧
(a ∨ b) ∧
(¬b) ∧
(¬f ∨ a ∨ ¬e)

您有一个 3SAT 问题，有一个独特的解决方案。该算法不详尽，所有这些问题都可以在多项式时间内解决。

这里是没有熔化的Python实现（数字是变量名，符号是不是）：

#!/usr/bin/env python

import random
import copy

def generate():
    variable_number = 20 + random.randint(0, 20)
    solution = [0] * variable_number

    for i in range(variable_number):
        sign = 1 if random.randint(0, 2) == 0 else -1
        solution[i] = (i + 1) * sign

    problem = [0] * variable_number

    for i in range(len(solution)):
        problem[i] = [solution[i]]

    new_problem = []

    for k in range(2):
        for i in range(len(problem)):
            clause = problem[i]
            new_problem.append(clause)

            if 0 < random.randint(0, 3):
                found = False
                other_variable = 0

                while not found:
                    other_variable = (random.randint(0, variable_number) + 1)
                    found = True

                    for j in range(len(clause)):
                        if abs(clause[j]) == other_variable:
                            found = False

                duplicate_clause = copy.deepcopy(clause)
                clause.append(other_variable)
                duplicate_clause.append(-other_variable)
                new_problem.append(duplicate_clause)

    problem = new_problem

    return problem, solution

a_problem, a_solution = generate()
print("The problem")
print(a_problem)
print("The solution")
print(a_solution)

独特的3sat解决方案示例

问题描述投票：0回答：3

3个回答

最新问题

独特的3sat解决方案示例

问题描述 投票：0回答：3

3个回答

最新问题

问题描述投票：0回答：3