Personal tools
You are here: Home / Internal / RISC Forum / 2014 / Risc Colloquium

Risc Colloquium

Prof. Jordi Levy: The Nature of Industrial SAT Instances
When Jul 11, 2014
from 11:00 AM to 11:50 AM
Where Seminar Room pond, RISC
Add event to calendar vCal

We study the structure of "industrial" SAT formulas representing them as graphs, either as a bi-partite graphs where a variable node and a clause node are connected if the variable occurs in the clause, or as a graph where two variable nodes are connected if they occur together in a clause. We explore the instances used in the SAT competitions. This analysis can help to understand some heuristics and methods use in modern SAT solvers. The final objective is to improve their performance on "real" instances, and to get a better random model of them.

We show that most of the formulas have a scale-free structure, where variable-nodes degree (number of occurrences of variables) follow a power-law distribution, in almost all cases, and clause-nodes degree (size of clauses) too, in most of the cases.  We propose a method to randomly generating scale-free SAT formulas, and check how good are SAT solvers on them.

We analyze also the community structure of industrial SAT formulas. We see that most of them are highly modular (maybe as a consequence of scale-free structure).

Finally, we explore self-similarity of these graphs and compute their fractal dimension. We see that in most of the cases, graphs have a fractal dimension between 2 and 3. This implies that the diameter of graphs grow polynomially, and not logarithmically. This would also mean that industrial SAT solvers could be using some mechanism to focus their search in an area of the formula.

« January 2020 »
Upcoming Events
RISC Forum Jan 27, 2020 01:30 PM - 01:45 PM
RISC Forum Mar 02, 2020 01:30 PM - 01:45 PM
RISC Forum Mar 09, 2020 01:30 PM - 02:15 PM
RISC Forum Mar 23, 2020 01:30 PM - 01:45 PM
RISC Forum Mar 30, 2020 01:30 PM - 02:30 PM
Previous events…
Upcoming events…