Abstract: 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.
Journal on Satisfiability, Boolean Modeling and Computation ISSN: 1574-0617
JSAT is an open access peer reviewed journal, publishing high quality original research papers and
survey papers which evidently contribute to deeper insight. It is an electronic medium, guaranteeing
fast publication.
JSAT volume 10
That volume started in our previous platform Open Journal System. The first three papers have been published in 2016 and 2017.
The remaining papers have been published since July 2019.
Table of Contents
Abstract: 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.
Abstract: 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 tautology, and the guarded ordering tautologies. This shows that regular resolution does not simulate linear resolution.
Abstract: 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 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.