Journal on Satisfiability, Boolean Modeling and Computation - Volume 4, issue 1

Authors: Szörényi, Balázs

Article Type: Research Article

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 Φ. Show more

Keywords: disjoint DNF tautologies, decision trees, unsatisfiable hitting clause sets, read-once resolution refutation, conflict bound

DOI: 10.3233/SAT190035

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 1, pp. 1-14, 2008

Authors: Anjos, Miguel F.

Article Type: Research Article

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. Show more

Keywords: satisfiability, semidefinite programming, discrete optimization, global optimization

DOI: 10.3233/SAT190036

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 1, pp. 15-31, 2008

Authors: Acharyya, Sriyankar

Article Type: Research Article

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. Show more

Keywords: SAT algorithm, graph colouring, tabu search

DOI: 10.3233/SAT190037

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 1, pp. 33-55, 2008

Authors: Chebiryak, Yury | Kroening, Daniel

Article Type: Research Article

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.

Keywords: bitonic sorting network, code equivalence, Gray code, Hamiltonian cycle, hypercube, SAT-solver, symmetry breaking

DOI: 10.3233/SAT190038

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 4, no. 1, pp. 57-74, 2008