Showing 1–14 of 14 results for author: Niemela, I

Conflict-Driven XOR-Clause Learning (extended version)

Authors: Tero Laitinen, Tommi Junttila, Ilkka Niemelä

Abstract: Modern conflict-driven clause learning (CDCL) SAT solvers are very good in solving conjunctive normal form (CNF) formulas. However, some application problems involve lots of parity (xor) constraints which are not necessarily efficiently handled if translated into CNF. This paper studies solving CNF formulas augmented with xor-clauses in the DPLL(XOR) framework where a CDCL SAT solver is coupled wi… ▽ More Modern conflict-driven clause learning (CDCL) SAT solvers are very good in solving conjunctive normal form (CNF) formulas. However, some application problems involve lots of parity (xor) constraints which are not necessarily efficiently handled if translated into CNF. This paper studies solving CNF formulas augmented with xor-clauses in the DPLL(XOR) framework where a CDCL SAT solver is coupled with a separate xor-reasoning module. New techniques for analyzing xor-reasoning derivations are developed, allowing one to obtain smaller CNF clausal explanations for xor-implied literals and also to derive and learn new xor-clauses. It is proven that these new techniques allow very short unsatisfiability proofs for some formulas whose CNF translations do not have polynomial size resolution proofs, even when a very simple xor-reasoning module capable only of unit propagation is applied. The efficiency of the proposed techniques is evaluated on a set of challenging logical cryptanalysis instances. △ Less

Submitted 24 July, 2014; originally announced July 2014.

Classifying and Propagating Parity Constraints (extended version)

Authors: Tero Laitinen, Tommi Junttila, Ilkka Niemelä

Abstract: Parity constraints, common in application domains such as circuit verification, bounded model checking, and logical cryptanalysis, are not necessarily most efficiently solved if translated into conjunctive normal form. Thus, specialized parity reasoning techniques have been developed in the past for propagating parity constraints. This paper studies the questions of deciding whether unit propagati… ▽ More Parity constraints, common in application domains such as circuit verification, bounded model checking, and logical cryptanalysis, are not necessarily most efficiently solved if translated into conjunctive normal form. Thus, specialized parity reasoning techniques have been developed in the past for propagating parity constraints. This paper studies the questions of deciding whether unit propagation or equivalence reasoning is enough to achieve full propagation in a given parity constraint set. Efficient approximating tests for answering these questions are developed. It is also shown that equivalence reasoning can be simulated by unit propagation by adding a polynomial amount of redundant parity constraints to the problem. It is proven that without using additional variables, an exponential number of new parity constraints would be needed in the worst case. The presented classification and propagation methods are evaluated experimentally. △ Less

Submitted 18 June, 2014; originally announced June 2014.

Simulating Parity Reasoning (extended version)

Authors: Tero Laitinen, Tommi Junttila, Ilkka Niemelä

Abstract: Propositional satisfiability (SAT) solvers, which typically operate using conjunctive normal form (CNF), have been successfully applied in many domains. However, in some application areas such as circuit verification, bounded model checking, and logical cryptanalysis, instances can have many parity (xor) constraints which may not be handled efficiently if translated to CNF. Thus, extensions to the… ▽ More Propositional satisfiability (SAT) solvers, which typically operate using conjunctive normal form (CNF), have been successfully applied in many domains. However, in some application areas such as circuit verification, bounded model checking, and logical cryptanalysis, instances can have many parity (xor) constraints which may not be handled efficiently if translated to CNF. Thus, extensions to the CNF-driven search with various parity reasoning engines ranging from equivalence reasoning to incremental Gaussian elimination have been proposed. This paper studies how stronger parity reasoning techniques in the DPLL(XOR) framework can be simulated by simpler systems: resolution, unit propagation, and parity explanations. Such simulations are interesting, for example, for develo** the next generation SAT solvers capable of handling parity constraints efficiently. △ Less

Submitted 18 November, 2013; originally announced November 2013.

Bounded Model Checking of an MITL Fragment for Timed Automata

Authors: Roland Kindermann, Tommi Junttila, Ilkka Niemelä

Abstract: Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. MITL is a real-time extension of the linear time logic LTL. Originally, MITL was defined for traces of non-overlap** time intervals rather than the "super-dense" time traces allowing for intervals over… ▽ More Timed automata (TAs) are a common formalism for modeling timed systems. Bounded model checking (BMC) is a verification method that searches for runs violating a property using a SAT or SMT solver. MITL is a real-time extension of the linear time logic LTL. Originally, MITL was defined for traces of non-overlap** time intervals rather than the "super-dense" time traces allowing for intervals overlap** in single points that are employed by the nowadays common semantics of timed automata. In this paper we extend the semantics of a fragment of MITL to super-dense time traces and devise a bounded model checking encoding for the fragment. We prove correctness and completeness in the sense that using a sufficiently large bound a counter-example to any given non-holding property can be found. We have implemented the proposed bounded model checking approach and experimentally studied the efficiency and scalability of the implementation. △ Less

Submitted 26 April, 2013; originally announced April 2013.

Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)

Authors: Tero Laitinen, Tommi Junttila, Ilkka Niemelä

Abstract: Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instance is a combination of traditional clauses and parity constraints. This paper studies how such combined problems can be efficiently solved by augmenting a modern SAT solver with an xor-reasoning module in the DPLL(XOR) fr… ▽ More Instances of logical cryptanalysis, circuit verification, and bounded model checking can often be succinctly represented as a combined satisfiability (SAT) problem where an instance is a combination of traditional clauses and parity constraints. This paper studies how such combined problems can be efficiently solved by augmenting a modern SAT solver with an xor-reasoning module in the DPLL(XOR) framework. A new xor-reasoning module that deduces all possible implied literals using incremental Gauss-Jordan elimination is presented. A decomposition technique that can greatly reduce the size of parity constraint matrices while allowing still to deduce all implied literals is presented. It is shown how to eliminate variables occuring only in parity constraints while preserving the decomposition. The proposed techniques are evaluated experimentally. △ Less

Submitted 8 September, 2012; v1 submitted 4 July, 2012; originally announced July 2012.

SMT-based Induction Methods for Timed Systems

Authors: Roland Kindermann, Tommi Junttila, Ilkka Niemelä

Abstract: Modeling time related aspects is important in many applications of verification methods. For precise results, it is necessary to interpret time as a dense domain, e.g. using timed automata as a formalism, even though the system's resulting infinite state space is challenging for verification methods. Furthermore, fully symbolic treatment of both timing related and non-timing related elements of th… ▽ More Modeling time related aspects is important in many applications of verification methods. For precise results, it is necessary to interpret time as a dense domain, e.g. using timed automata as a formalism, even though the system's resulting infinite state space is challenging for verification methods. Furthermore, fully symbolic treatment of both timing related and non-timing related elements of the state space seems to offer an attractive approach to model checking timed systems with a large amount of non-determinism. This paper presents an SMT-based timed system extension to the IC3 algorithm, a SAT-based novel, highly efficient, complete verification method for untimed systems. Handling of the infinite state spaces of timed system in the extended IC3 algorithm is based on suitably adapting the well-known region abstraction for timed systems. Additionally, $k$-induction, another symbolic verification method for discrete time systems, is extended in a similar fashion to support timed systems. Both new methods are evaluated and experimentally compared to a booleanization-based verification approach that uses the original discrete time IC3 algorithm. △ Less

Submitted 25 April, 2012; originally announced April 2012.

Translating Answer-Set Programs into Bit-Vector Logic

Authors: Mai Nguyen, Tomi Janhunen, Ilkka Niemelä

Abstract: Answer set programming (ASP) is a paradigm for declarative problem solving where problems are first formalized as rule sets, i.e., answer-set programs, in a uniform way and then solved by computing answer sets for programs. The satisfiability modulo theories (SMT) framework follows a similar modelling philosophy but the syntax is based on extensions of propositional logic rather than rules. Quite… ▽ More Answer set programming (ASP) is a paradigm for declarative problem solving where problems are first formalized as rule sets, i.e., answer-set programs, in a uniform way and then solved by computing answer sets for programs. The satisfiability modulo theories (SMT) framework follows a similar modelling philosophy but the syntax is based on extensions of propositional logic rather than rules. Quite recently, a translation from answer-set programs into difference logic was provided---enabling the use of particular SMT solvers for the computation of answer sets. In this paper, the translation is revised for another SMT fragment, namely that based on fixed-width bit-vector theories. Thus, even further SMT solvers can be harnessed for the task of computing answer sets. The results of a preliminary experimental comparison are also reported. They suggest a level of performance which is similar to that achieved via difference logic. △ Less

Submitted 30 August, 2011; originally announced August 2011.

Comments: 12 pages, 1 figure, 3 tables

Origins of Answer-Set Programming - Some Background And Two Personal Accounts

Authors: Victor W. Marek, Ilkka Niemela, Miroslaw Truszczynski

Abstract: We discuss the evolution of aspects of nonmonotonic reasoning towards the computational paradigm of answer-set programming (ASP). We give a general overview of the roots of ASP and follow up with the personal perspective on research developments that helped verbalize the main principles of ASP and differentiated it from the classical logic programming. We discuss the evolution of aspects of nonmonotonic reasoning towards the computational paradigm of answer-set programming (ASP). We give a general overview of the roots of ASP and follow up with the personal perspective on research developments that helped verbalize the main principles of ASP and differentiated it from the classical logic programming. △ Less

Submitted 16 August, 2011; originally announced August 2011.

Comments: In G. Brewka, V.M. Marek, and M. Truszczynski, eds. Nonmonotonic Reasoning -- Essays Celebrating its 30th Anniversary, College Publications, 2011 (a volume of papers presented at NonMon at 30 meeting, Lexington, KY, USA, October 2010)

MSC Class: I.2.4

Logic programs with monotone abstract constraint atoms

Authors: V. W. Marek, I. Niemela, M. Truszczynski]

Abstract: We introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantic… ▽ More We introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with weight atoms (lparse programs) with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue. △ Less

Submitted 25 August, 2006; originally announced August 2006.

Comments: 33 pages

ACM Class: F.4.1; D.1.6

Logic programs with monotone cardinality atoms

Authors: Victor W. Marek, Ilkka Niemela, Miroslaw Truszczynski

Abstract: We investigate mca-programs, that is, logic programs with clauses built of monotone cardinality atoms of the form kX, where k is a non-negative integer and X is a finite set of propositional atoms. We develop a theory of mca-programs. We demonstrate that the operational concept of the one-step provability operator generalizes to mca-programs, but the generalization involves nondeterminism. Our m… ▽ More We investigate mca-programs, that is, logic programs with clauses built of monotone cardinality atoms of the form kX, where k is a non-negative integer and X is a finite set of propositional atoms. We develop a theory of mca-programs. We demonstrate that the operational concept of the one-step provability operator generalizes to mca-programs, but the generalization involves nondeterminism. Our main results show that the formalism of mca-programs is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with cardinality atoms and with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue. △ Less

Submitted 31 October, 2003; originally announced October 2003.

Comments: Proceedings of LPNMR-03 (7th International Conference), LNCS, Springer Verlag

ACM Class: D.1.6; I.2.3

Bounded LTL Model Checking with Stable Models

Authors: Keijo Heljanko, Ilkka Niemelä

Abstract: In this paper bounded model checking of asynchronous concurrent systems is introduced as a promising application area for answer set programming. As the model of asynchronous systems a generalisation of communicating automata, 1-safe Petri nets, are used. It is shown how a 1-safe Petri net and a requirement on the behaviour of the net can be translated into a logic program such that the bounded… ▽ More In this paper bounded model checking of asynchronous concurrent systems is introduced as a promising application area for answer set programming. As the model of asynchronous systems a generalisation of communicating automata, 1-safe Petri nets, are used. It is shown how a 1-safe Petri net and a requirement on the behaviour of the net can be translated into a logic program such that the bounded model checking problem for the net can be solved by computing stable models of the corresponding program. The use of the stable model semantics leads to compact encodings of bounded reachability and deadlock detection tasks as well as the more general problem of bounded model checking of linear temporal logic. Correctness proofs of the devised translations are given, and some experimental results using the translation and the Smodels system are presented. △ Less

Submitted 23 May, 2003; originally announced May 2003.

Comments: 32 pages, to appear in Theory and Practice of Logic Programming

ACM Class: D.2.4; D.2.2; F.4.1; I.2.4; F.3.1

Unfolding Partiality and Disjunctions in Stable Model Semantics

Authors: T. Janhunen, I. Niemela, D. Seipel, P. Simons, J. You

Abstract: The paper studies an implementation methodology for partial and disjunctive stable models where partiality and disjunctions are unfolded from a logic program so that an implementation of stable models for normal (disjunction-free) programs can be used as the core inference engine. The unfolding is done in two separate steps. Firstly, it is shown that partial stable models can be captured by tota… ▽ More The paper studies an implementation methodology for partial and disjunctive stable models where partiality and disjunctions are unfolded from a logic program so that an implementation of stable models for normal (disjunction-free) programs can be used as the core inference engine. The unfolding is done in two separate steps. Firstly, it is shown that partial stable models can be captured by total stable models using a simple linear and modular program transformation. Hence, reasoning tasks concerning partial stable models can be solved using an implementation of total stable models. Disjunctive partial stable models have been lacking implementations which now become available as the translation handles also the disjunctive case. Secondly, it is shown how total stable models of disjunctive programs can be determined by computing stable models for normal programs. Hence, an implementation of stable models of normal programs can be used as a core engine for implementing disjunctive programs. The feasibility of the approach is demonstrated by constructing a system for computing stable models of disjunctive programs using the smodels system as the core engine. The performance of the resulting system is compared to that of dlv which is a state-of-the-art special purpose system for disjunctive programs. △ Less

Submitted 2 January, 2004; v1 submitted 14 March, 2003; originally announced March 2003.

Comments: 49 pages, 4 figures, 1 table

ACM Class: I.2.4; F.4.1

DES: a Challenge Problem for Nonmonotonic Reasoning Systems

Authors: Maarit Hietalahti, Fabio Massacci, Ilkka Niemela

Abstract: The US Data Encryption Standard, DES for short, is put forward as an interesting benchmark problem for nonmonotonic reasoning systems because (i) it provides a set of test cases of industrial relevance which shares features of randomly generated problems and real-world problems, (ii) the representation of DES using normal logic programs with the stable model semantics is simple and easy to under… ▽ More The US Data Encryption Standard, DES for short, is put forward as an interesting benchmark problem for nonmonotonic reasoning systems because (i) it provides a set of test cases of industrial relevance which shares features of randomly generated problems and real-world problems, (ii) the representation of DES using normal logic programs with the stable model semantics is simple and easy to understand, and (iii) this subclass of logic programs can be seen as an interesting special case for many other formalizations of nonmonotonic reasoning. In this paper we present two encodings of DES as logic programs: a direct one out of the standard specifications and an optimized one extending the work of Massacci and Marraro. The computational properties of the encodings are studied by using them for DES key search with the Smodels system as the implementation of the stable model semantics. Results indicate that the encodings and Smodels are quite competitive: they outperform state-of-the-art SAT-checkers working with an optimized encoding of DES into SAT and are comparable with a SAT-checker that is customized and tuned for the optimized SAT encoding. △ Less

Submitted 8 March, 2000; originally announced March 2000.

Comments: 10 pages, 1 Postscript figure, uses aaai.sty and graphicx.sty

ACM Class: I.2.3; I.2.4

Smodels: A System for Answer Set Programming

Authors: Ilkka Niemela, Patrik Simons, Tommi Syrjanen

Abstract: The Smodels system implements the stable model semantics for normal logic programs. It handles a subclass of programs which contain no function symbols and are domain-restricted but supports extensions including built-in functions as well as cardinality and weight constraints. On top of this core engine more involved systems can be built. As an example, we have implemented total and partial stab… ▽ More The Smodels system implements the stable model semantics for normal logic programs. It handles a subclass of programs which contain no function symbols and are domain-restricted but supports extensions including built-in functions as well as cardinality and weight constraints. On top of this core engine more involved systems can be built. As an example, we have implemented total and partial stable model computation for disjunctive logic programs. An interesting application method is based on answer set programming, i.e., encoding an application problem as a set of rules so that its solutions are captured by the stable models of the rules. Smodels has been applied to a number of areas including planning, model checking, reachability analysis, product configuration, dynamic constraint satisfaction, and feature interaction. △ Less

Submitted 8 March, 2000; originally announced March 2000.

Comments: Proceedings of the 8th International Workshop on Non-Monotonic Reasoning, April 9-11, 2000, Breckenridge, Colorado 4 pages, uses aaai.sty

ACM Class: I.2.3; I.2.4