6
$\begingroup$

I'm noodling around with making a hardware SAT solver on an FPGA, and I'm wondering if there are any interesting SAT problems smaller than, say, 50 variables both to stay within the limits of the FPGA board (namely the number of LEDs) and so I can brute-force if needed to get all possible solutions. I looked into factorizing small integers, but it seems that even relatively small numbers quickly get in to the hundreds of variables. Is there anything else I can look at besides random-SAT?

$\endgroup$
  • $\begingroup$ you want to implement the solver using FPGA gates? the bigger question is how big the solver algorithm is converted to gates... how are you converting the solving algorithm to gates? anyway, interesting project! definitely suggest dropping by Computer Science Chat. fairly simple problems easy to verify/ implement would involve integer arithmetic eg addition or subtraction. see also tseytin transform $\endgroup$ – vzn Feb 4 '16 at 5:37
  • 1
    $\begingroup$ By "interesting", do you basically mean " hard to solve"? $\endgroup$ – Juho Feb 4 '16 at 7:08
  • $\begingroup$ @Juho interesting means that if I could scale it up with fancier custom hardware (bought by investors) to sizes people care about then I'd be rich :) $\endgroup$ – Andrew Feb 4 '16 at 14:30
4
$\begingroup$

In general, you can look at hard combinatorial instances. If 50 variables is not a hard limit, try e.g., an instance arising from combinatorial block design having 105 variables described in [1]. The actual instance in DIMACS format is here provided by the authors. For the instance, the authors write in [1] that: "We issue a challenge for any solver to solve it in less than one day."

Something that will be not as hard, but still not entirely trivial is coloring Mycielski graphs. These are graphs with clique number 2, but the chromatic number can be arbitrarily large. Again, if 50 variables is really a hard limit, it seems the largest Mycielski graphs you can consider is the Grötzsch graph if you use the obvious encoding to CNF. The obvious encoding will have 33 variables if you test for 3-colorability (UNSAT), and 44 variables if you test for 4-colorability (SAT).


[1] Van Gelder, Allen, and Ivor Spence. "Zero-one designs produce small hard SAT instances." Theory and Applications of Satisfiability Testing–SAT 2010. Springer Berlin Heidelberg, 2010. 388-397.

$\endgroup$
  • $\begingroup$ Are your 33 and 44 assuming he's restricting to 3-SAT? ​ (I see an easy way to encode each of those as 22-variable 4-SAT instances.) ​ ​ ​ ​ $\endgroup$ – user12859 Feb 4 '16 at 11:46
  • $\begingroup$ @RickyDemer Maybe, but I feel like I wasn't. Anyway, it should not matter too much if 50 variables really is a hard limit. $\endgroup$ – Juho Feb 4 '16 at 12:15
  • $\begingroup$ 2-variables-per-vertex would allow him to use the next Mycielski graph. ​ ​ $\endgroup$ – user12859 Feb 4 '16 at 12:17
  • $\begingroup$ @Juho this seems exactly like what I was looking for! I'm a physicist by training, though, so I'm going to have to do some research to unpack all of this... $\endgroup$ – Andrew Feb 5 '16 at 0:46
  • $\begingroup$ @Andrew Great, glad it helps :-) $\endgroup$ – Juho Feb 5 '16 at 7:03
3
$\begingroup$

See the international SAT solver competition. It's a competition that tests various solvers by running them on a library of hard SAT instances. You can download the instances they used to evaluate the SAT solvers. I would suggest you look at these competitions and see if any of the instances they've used would meet your needs.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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