The solution graph of a Boolean formula on n variables is the subgraph of the hypercube Hn induced by the satisfying assignments of the formula. The structure of solution graphs has been the object of much research in recent years since it is important for the performance of SAT-solving procedures ... more >>>

In this work we extend the study of solution graphs and prove that for boolean formulas in a class called CPSS, all connected components are partial cubes of small dimension, a statement which was proved only for some cases in [Schwerdtfeger 2013]. In contrast, we show that general Schaefer formulas ... more >>>

It is well known that problems encoded with circuits or formulas generally gain an exponential complexity blow-up compared to their original complexity.

We introduce a new way for encoding graph problems, based on $\textrm{CNF}$ or $\textrm{DNF}$ formulas. We show that contrary to the other existing succinct models, there are ... more >>>