英文:
Example of unique 3sat solution
问题
我正在寻找具有唯一解的3sat问题。到目前为止，我只找到一个网站https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
该网站上有一些3sat实例的良好示例，但问题是如果它们是可满足的，它们可能有不止一个解。我想要具有20到40个变量和至少100个子句（更多更好）的这种大型3sat实例，但要求它们具有唯一解。我该在哪里找到这样的问题列表，或者是否有任何算法可以生成具有唯一解的3sat问题？
英文:
I am searching for 3sat problems having unique solution. Till now, I only found one site https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
There are good examples of 3sat instance on that site but the problem is they have more than 1 solution if it's satisfiable. I want such big instances of 3sat of having 20 40 variables and at least 100 clauses
( More will be good ) but having unique solution. Where can I get such list of questions Or is there any algorithm which can generate 3sat question having unique solution ?
答案1
得分: 0
https://it-in-industry.com/itii_papers/2019/7219itii03.pdf 讨论了生成独特的3-SAT问题。可能是一个好的起点。
英文:
https://it-in-industry.com/itii_papers/2019/7219itii03.pdf discusses generating unique 3-sat problems. Might be a good place to start.
答案2
得分: 0
构建一个具有唯一解的3SAT问题，您可以使用诸如adder或multiplier之类的算术电路。然后将得到的输出线与已知结果使用digital comparator进行比较。
设计流程可以如下：
- 编写要使用的算术表达式。
例如：x * 7，x - 1，x * x - 将表达式翻译成逻辑门的布尔电路。
这可以通过一个合适的Python脚本完成。 - 使用类似bc2cnf的工具将电路转换为合取范式（CNF）。
- 如果生成的子句数量过大或过小，
返回步骤1，并调整表达式操作数的比特长度。
这样一个电路的最简单变体将是一个没有预连接算术电路的数字比较器。
要获得唯一解，算术表达式必须具有唯一解。反例包括整数除法和整数平方根。
英文:
To construct a 3SAT problem with unique solution, you could use an arithmetic circuit like an adder or a multiplier. The resulting output lines are then compared against the known result using a digital comparator.
The design flow could be as follows:
- Write the arithmetic expression to be used.
Examples: x * 7, x - 1, x * x - Translate the expression into a boolean circuit of logical gates.
This can be done by a suitable python script. - Transform the circuit into Conjunctive Normal Form (CNF)
using a tool like bc2cnf. - If the resulting number of clauses is too big or too small,
go back to step 1. and adjust the bitlength of the expression operand.
The simplest variant of such a circuit would be a digital comparator without pre-attached arithmetic circuit.
To get a unique solution, the arithmetic expression must have a unique solution. Counterexamples include integer division and integer sqare root.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论