Journal on Satisfiability,Boolean Modelling and Computation

Is well-known that the proof size in propositional resolution is sensitive to the order of how variables are resolved on. Indeed, imposing a certain resolution order can lead to an exponential blowup compared to unrestricted resolution. In this paper we study even a weaker restriction. We require that one partition of variables is resolved on before the second partition (this is a special case of a partial order). We show that this also can lead to an exponential blowup. This helps us to understand why dynamic variable orderings in SAT solvers is so successful but also it motivates further investigation in variable orderings in SAT solvers.

We establish a reduction of a combinatorial problem defined via autocorrelation to an instance of Boolean satisfiability. As a consequence, we obtain a family of hard satisfiable 3-SAT instances. The combinatorial problem that we reduce is the D-optimal matrices problem. We generated a family of 3-SAT instances from the D-optimal matrices problem with the motivation to solve interesting cases using the power of SAT solvers. We give a detailed construction of the generated instances that were submitted to SAT competition 2014. Our reduction techniques is fairly straightforward and can be adapted to various other problems that are defined via autocorrelation.

We discuss the relationship between linear resolution, s-linear resolution and other fragments of resolution, including tree-like resolution, regular resolution and general resolution. We also discuss linear resolution with restarts. We present polynomial-size linear resolution proofs of the ordering tautologies (also known as “graph tautologies”), and the guarded ordering tautologies. This shows that regular resolution does not simulate linear resolution.

The solution-graph of a Boolean formula on n variables is the subgraph of the hypercube H n 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 based on local search. Several authors have studied connectivity problems in such graphs focusing on how the structure of the original formula might affect the complexity of the connectivity problems in the solution-graph.

In this paper we study the complexity of the isomorphism problem of solution-graphs of Boolean formulas. We consider the classes of formulas that arise in the CSP-setting and investigate how the complexity of the isomorphism problem depends on the formula type.

We observe that for general formulas the solution-graph isomorphism problem can be solved in exponential time while in the cases of 2CNF formulas, as well as for CPSS formulas, the problem is in the counting complexity class C = P , a subclass of PSPACE. We also prove a strong property on the structure of solution-graphs of Horn formulas showing that they are just unions of partial cubes.

In addition, we give a PSPACE lower bound for the problem on general Boolean functions. We prove that for 2CNF, as well as for CPSS formulas the solution-graph isomorphism problem is hard for C = P under polynomial time many-one reductions, thus matching the given upper bound.