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?
$\begingroup$
$\endgroup$
3
-
$\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$– vznCommented Feb 4, 2016 at 5:37
-
1$\begingroup$ By "interesting", do you basically mean " hard to solve"? $\endgroup$– JuhoCommented Feb 4, 2016 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$– AndrewCommented Feb 4, 2016 at 14:30
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
5
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).
-
$\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$– user12859Commented Feb 4, 2016 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$– JuhoCommented Feb 4, 2016 at 12:15
-
$\begingroup$ 2-variables-per-vertex would allow him to use the next Mycielski graph. $\endgroup$– user12859Commented Feb 4, 2016 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$– AndrewCommented Feb 5, 2016 at 0:46
-
$\begingroup$
$\endgroup$
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.
