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
iCal

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.

« October 2019 »
October
MoTuWeThFrSaSu
123456
78910111213
14151617181920
21222324252627
28293031
Upcoming Events
RISC Forum Oct 28, 2019 01:30 PM - 01:45 PM
RISC Forum Nov 04, 2019 01:30 PM - 01:45 PM
RISC Forum Nov 11, 2019 01:30 PM - 02:30 PM
RISC Forum Nov 18, 2019 01:30 PM - 02:15 PM
RISC Forum Nov 25, 2019 01:30 PM - 01:45 PM
Previous events…
Upcoming events…