Journal on Satisfiability, Boolean Modeling and Computation - Volume 3, issue 3-4
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: The notion of minimal unsatisfiability and minimal falsity will be extended to non-clausal and non-prenex quantified Boolean formulas. For quantified Boolean formulas in negation normal form we generalize the notion of deficiency to the so-called cohesion, which is 1+ the difference between the number of occurrences of the conjunction symbol ∧ and the number of existential and free variables. Further, we show that all the complexity results with respect to minimal unsatisfiability or minimal falsity known for formulas with fixed deficiency can be adapted to formulas with fixed cohesion. For example, (1) the minimal unsatisfiability of propositional formulas with fixed…cohesion is still solvable in polynomial time and, (2) the minimal falsity of quantified Boolean formulas with cohesion 1 is solvable in polynomial time.
Abstract: We study a new approach to the satisfiability problem, which we call the Support Paradigm . Given a CNF formula F and an assignment to its variables we say that a literal x supports a clause C in F w.r.t. ψ if x is the only literal that evaluates to true in C . Our focus in this work will be on heuristics that obey the following general template: start at some assignment to the variables, then iteratively, using some predefined (greedy) rule, try to minimize the number of unsatisfied clauses (or the…distance from some satisfying assignment) until a satisfying assignment is reached. We say that such a heuristic is part of the Support Paradigm if the greedy rule uses the support as its main criterion. We present a new algorithm in the Support Paradigm and rigorously prove its effectiveness for a certain distribution over satisfiable k -CNF formulas known as the planted distribution. One motivation for this work is recent experimental results showing that some simple variants of the RWalkSAT algorithm, which base their greedy rule on the support, seem to remain e ective for random 3CNF formulas in the “hard” near-threshold regime, while for example RWalkSAT , which disregards the support, is already inefficient in a much earlier stage.
Keywords: average case analysis, random k-SAT, efficient heuristics, computational complexity
Abstract: Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some decidable first-order theory T (SMT ( T ) ). These problems are typically not handled adequately by standard automated theorem provers. SMT is being recognized as increasingly important due to its applications in many domains in different communities, in particular in formal verification. An amount of papers with novel and very efficient techniques for SMT has been published in the last years, and some very efficient SMT tools are now available. Typical SMT (…T ) problems require testing the satisfiability of formulas which are Boolean combinations of atomic propositions and atomic expressions in T , so that heavy Boolean reasoning must be efficiently combined with expressive theory-specific reasoning. The dominating approach to SMT ( T ) , called lazy approach , is based on the integration of a SAT solver and of a decision procedure able to handle sets of atomic constraints in T (T -solver ), handling respectively the Boolean and the theory-specific components of reasoning. Unfortunately, neither the problem of building an efficient SMT solver, nor even that of acquiring a comprehensive background knowledge in lazy SMT, is of simple solution. In this paper we present an extensive survey of SMT, with particular focus on the lazy approach. We survey, classify and analyze from a theory-independent perspective the most effective techniques and optimizations which are of interest for lazy SMT and which have been proposed in various communities; we discuss their relative benefits and drawbacks; we provide some guidelines about their choice and usage; we also analyze the features for SAT solvers and T -solvers which make them more suitable for an integration. The ultimate goals of this paper are to become a source of a common background knowledge and terminology for students and researchers in different areas, to provide a reference guide for developers of SMT tools, and to stimulate the cross-fertilization of techniques and ideas among different communities.