2
$\begingroup$

I need SAT instances, involving 9 to 20 variables. They need to be hard to solve for humans. Both SAT and UNSAT instances are needed.

I tried random-SAT generators on the web, but the results were not satisfactory because they are trivial. A good example of what I'm looking for is the following 4-variable instance from The Art of Computer Programming: $$12\bar3, 23\bar4, 134, \bar124, \bar1\bar23, \bar2\bar34, \bar1\bar3\bar4, 1\bar2\bar4.$$

$\endgroup$
5
  • 3
    $\begingroup$ "They need to be hard to solve for humans." Arguably any SAT instance would do since the average human does not even know what SAT is. $\endgroup$
    – dkaeae
    Commented Jan 25, 2019 at 8:40
  • $\begingroup$ Start building a solution, and add random SAT lines that respects it until no other solution is possible. You won't likely obtain a trivial problem with 9 to 20 variables. $\endgroup$
    – Optidad
    Commented Jan 25, 2019 at 9:20
  • $\begingroup$ @Vince: I tried random kSAT with 9 variables, 6 literals per clause and 600 clauses and finally got it to be unsatisfiable. 500 clauses wouldn't work. It's so big. I need smaller and more carefully designed instances. $\endgroup$
    – Zirui Wang
    Commented Feb 5, 2019 at 4:05
  • $\begingroup$ @dkaeae Best but not so lucky human. $\endgroup$
    – Zirui Wang
    Commented Feb 13, 2019 at 12:46
  • 1
    $\begingroup$ Generating random instances is unlikely to work: random SAT is computationally easy in most parameterizations. $\endgroup$ Commented Aug 14, 2019 at 13:10

2 Answers 2

1
$\begingroup$

To build a satisfiable instance, start by picking an assignment to the variables that will be a solution. Then, randomly generate clauses that are satisfied by this assignment. Add as many clauses as desired. If you add enough clauses, then with high probability your chosen solution will be the only one, and the problem will be non-trivial.

For instance, suppose your assignment is $x_1=\text{True}$, $x_2=\text{False}$. Then you could add any subset of the clauses $x_1 \lor x_2$, $x_1 \lor \neg x_2$, or $\neg x_1 \lor \neg x_2$. For example, one random formula you could generate might be $(x_1 \lor x_2) \land (\neg x_1 \lor \neg x_2)$.

To build an unsatisfiable instance, proceed as above; then add one more clause that is violated by the solution you chose in advance. If you added enough clauses, it is likely that there will be no other solution, so the problem will be unsatisfiable. Check with a SAT solver just to be sure.

$\endgroup$
13
  • $\begingroup$ Give me an instance, maybe. $\endgroup$
    – Zirui Wang
    Commented Feb 13, 2019 at 12:43
  • $\begingroup$ @ZiruiWang, See edited answer for a simple example. You should be able to generate more yourself using the procedure listed here. That will involve writing a little bit of code; since it's your problem, I'll let you do that, as I have no particular interest in writing the code myself. $\endgroup$
    – D.W.
    Commented Feb 13, 2019 at 16:58
  • 1
    $\begingroup$ @ZiruiWang, I don't follow you. I'm not sure what distinction you're tryin g to draw. When you talk about efficiency, I'm not sure what you're trying to compare about. My answer is not based on efficiency; it's based on meeting your requirements. $\endgroup$
    – D.W.
    Commented Feb 19, 2019 at 5:49
  • 1
    $\begingroup$ @ZiruiWang, OK. I suggest writing a new question, where you define these new requirements in a precise way. I recommend that you state how small you need them to be; that you define "better"; that you list the metrics or criteria you will use to evaluate possible solutions; and that you show what methods you've already tried and how well they work along those metrics. That might help us meet your needs better. $\endgroup$
    – D.W.
    Commented Feb 21, 2019 at 18:16
  • 1
    $\begingroup$ @ZiruiWang, if you can't articulate your requirements clearly, we probably can't come up with a scheme that meets them. $\endgroup$
    – D.W.
    Commented Feb 23, 2019 at 19:46
0
$\begingroup$

I will do a quick calculation to show that small instances are rare. Consider an UNSAT instance. Suppose it’s $k$-SAT and every clause has exactly $k$ literals. Then there are at least $k$ variables, or some clauses will be trivial. So there are $2^k$ assignments and all of them have to be unsatisfiable. An assignment is unsatisfiable if there is a clause, in which all literals are false. When this happen, let’s call the assignment is covered by the clause. So your aim is to cover the entire $2^k$ assignments by clauses. But in this case, a clause can cover at most 1 assignment, so there are at least $2^k$ clauses in order to be unsatisfiable. When $k=6$, this is 64 and this is optimal. When $k=9$, this is 512. When $n>k$, the best case doesn’t change, but the probability shrinks as there is more noise.

$\endgroup$
2
  • $\begingroup$ OK but this doesn't answer your question. $\endgroup$ Commented Aug 14, 2019 at 13:09
  • $\begingroup$ @DavidRicherby OK but this shows that my expectation was too high and thus gives some kind of a negative answer: the instances have to be huge. Especially if you calculate the probabilities. By the way, I did figure out a way to generate instances both systematically and randomly. And also the number of instances, which is doubly exponential. So it’s better to survey rather than scan. That’s where I get. And the covering idea suggests that I should seek efficient data structures if I want to create a new, fast SAT solver. I.e., if everything is covered then it’s UNSAT and vice versa. Any idea? $\endgroup$
    – Zirui Wang
    Commented Aug 14, 2019 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.