You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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

open access

Open Access
ISSN  1574-0617 (E)
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.
results per page

On Using Cutting Planes in Pseudo-Boolean Optimization

Authors: Manquinho, Vasco M. | Marques-Silva, João

Article Type: Research Article

Abstract: Cutting planes are a well-known, widely used, and very effective technique for Integer Linear Programming (ILP). However, cutting plane techniques are seldom used in Pseudo-Boolean Optimization (PBO) algorithms. This paper addresses the utilization of Gomory mixed-integer and clique cuts, in Satisfiability-based algorithms for PBO, and shows how these cuts can be used for computing lower bounds and for learning new constraints. A side result of learning new constraints is that the utilization of cutting planes enables non-chronological backtracking. Besides cutting planes, the paper also shows that the utilization of search restarts in PBO can be effective in practice, allowing the … Show more

Keywords: pseudo-Boolean optimization, cutting planes, search restarts

DOI: 10.3233/SAT190023

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 209-219, 2006

Get PDF open access

Locality and Hard SAT-Instances

Authors: Markström, Klas

Article Type: Research Article

Abstract: In this note we construct a family of SAT-instance based on Eulerian graphs which are aimed at being hard for resolution based SAT-solvers. We discuss some experiments made with instances of this type and how a solver can try to avoid at least some of the pitfalls presented by these instances. Finally we look at how the density of subformulae can influence the hardness of SAT instances.

Keywords: satisfiability, hard instances, resolution, graphs, density

DOI: 10.3233/SAT190024

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 221-227, 2006

Get PDF open access

Back to the SAT05 Competition: an a Posteriori Analysis of Solver Performance on Industrial Benchmarks

Authors: Zarpas, Emmanuel

Article Type: Research Article

Abstract: This paper analyzes the SAT05 solver competition on industrial instances. We carefully investigate the performance of solvers from the competition and demonstration categories. We also present details on solver performance per subsets of the benchmarks per contributor and on SAT versus UNSAT instances. Finally we give recommendations for next SAT competition.

Keywords: satisfiability, benchmarking, performances, metrics, industrial problems

DOI: 10.3233/SAT190025

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 229-237, 2006

Get PDF open access
Show more