Journal on Satisfiability, Boolean Modeling and Computation - Volume 4, issue 1
The scope of JSAT is propositional reasoning, modeling, and computation. The Satisfiability discipline is a central focus of JSAT. We welcome all sorts of contributions to this theme but also encourage authors to submit papers on related topics as Computational Logic, Constraint Programming, Satisfiability Modulo Theories, Quantified Boolean Logic, Pseudo Boolean Methods, zero-one Programming, Integer Programming and Operations Research, whenever the link to Satisfiability is apparent.
Especially JSAT welcomes substantial extensions of conference papers, where the actual conference contribution must be cited. As such, authors are able to provide more detailed information about their work (theoretical details, proofs or theorems, algorithmic or implementation details, more exhaustive empirical evaluations) which were enforced to be omitted in the conference proceedings simply because of strict page limitations.
JSAT also welcomes detailed descriptions of new promising but challenging applications around SAT, to make the SAT community aware of those new applications, and to provide it the opportunity to tackle those challenges.
Occasionally JSAT also publishes Research Notes. Research Notes are also thoroughly reviewed but are not considered full Journal publications and hence will be designated and must be referenced to as such. Also, JSAT publishes papers on System Descriptions, being contributions with a focus on the internals of a Solver.
Abstract: Many aspects of the relation of different decision tree and DNF complexity measures of Boolean functions have been more or less substantially explored. This paper adds a new detail to the picture: we prove that DNF tautologies with terms conflicting in one or two variables pairwise possess a tree-like structure. An equivalent reformulation of this result (adopting the terminology of [7, 8, 9]) is the following. Call a clause-set (or CNF) a hitting clause-set if any two distinct clauses of it clash in at least one literal, and call a hitting clause-set an at-most-d hitting clause-set if any…two clauses of it clash in at most d variables. If now an at-most-2 hitting clause-set Φ is unsatisfiable (as a CNF), then, by the above result, there must exist a variable occurring (negated or unnegated) in each clause of Φ.
Abstract: This paper proposes a new semidefinite programming relaxation for the satisfiability problem. This relaxation is an extension of previous relaxations arising from the paradigm of partial semidefinite liftings for 0/1 optimization problems. The construction of the relaxation depends on a choice of permutations of the clauses, and different choices may lead to different relaxations. We then consider the Tseitin instances, a class of instances known to be hard for certain proof systems, and prove that for any choice of permutations, the proposed relaxation is exact for these instances, meaning that a Tseitin instance is unsatisfiable if and only if the…corresponding semidefinite programming relaxation is infeasible.
Keywords: satisfiability, semidefinite programming, discrete optimization, global optimization
Abstract: The local search algorithm GSAT is based on the notion of Satisfiability. It has been used successfully for colouring graphs, solving instances of the 3SAT problem, planning blocks world exercises, and other applications. The runtime performance of GSAT can be considerably enhanced by the incorporation of a noise generating component such as tabu search or random walk. This has been verified experimentally on numerous occasions, but few attempts have been made to explain the observed phenomena analytically. This paper examines, in the context of graph colouring, some aspects of the role of the tabu list in GSAT. Two slightly different…SAT formulations of graph colouring are considered. Three classes of graphs are defined that have the interesting property that, for certain initial partial colourings of the nodes, a proper colouring cannot be achieved by GSAT without the use of a tabu list. The minimum length of the tabu list that is necessary for solving the problem is determined for each class. It is found that this length varies considerably from case to case, and is sometimes quite large. We study experimentally the variation of runtime with the length of the tabu list to verify and further explore the theoretical results. We examine the general performance of other local search SAT methods like WalkSAT, Novelty, RNovelty, Novelty+ and RNovelty+ on these classes of graphs and to make a comparative assessment of all these methods.
Keywords: SAT algorithm, graph colouring, tabu search
Abstract: In this paper, we consider the problem of classifying Hamiltonian cycles in a binary hypercube. Previous work proposed a classification of these cycles using the edge representation, and presented it for dimension 4. We classify cycles in two further dimensions using a reduction to propositional SAT. Our proposed algorithm starts with an over-approximation of the set of equivalence classes, which is then refined using queries to a SAT-solver to remove spurious cycles. Our method performs up to three orders of magnitude faster than an enumeration with symmetry breaking in the 5-cube.