Category: Feature Articles

An Arboriculture Approach for Parallel SMT and Symbolic Model Checking

by M. Marescotti, A.E.J. Hyvärinen, N. SharyginaFormal Verification and Security LabUniversità della Svizzera ItalianaSwitzerland FULL PAPER Abstract: The inherent complexity of parallel computing makes development, resource monitoring, and debugging for parallel constraint-solving-based applications difficult. This paper presents SMTS, a framework for parallelizing sequential constraint…

The SAT Compiler in Picat

By Neng-Fa Zhou (CUNY Brooklyn College & Graduate Center) Abstract SAT solvers’ performance has drastically improved during the past 20 years, thanks to the inventions of techniques from conflict-driven clause learning, backjumping, variable and value selection heuristics, to random restarts.…

PSOA RuleML Bridges Graph and Relational Databases

By Harold Boley University of New Brunswick, Fredericton, Canada ABSTRACT In PSOA RuleML, Graph Databases and Relational Databases are bridged conceptually, with interoperation paths through its metamodel of three orthogonal dimensions, as well as programmatically, with transition rules realized in…

DLV: Evolution and Perspectives

DLV is a system for Answer Set Programming (ASP), a logic-based programming paradigm for solving problems in a fully declarative way. It has been one of the first solid and reliable ASP systems, widely used in academy and fruitfully employed in many relevant industrial applications. In this paper …