Tommi A. Junttila

Proceedings of the Handbook of Satisfiability - Second Edition, 2021

2020

An adaptive prefix-assignment technique for symmetry reduction.

[BibT_eX]

[DOI]

J. Symb. Comput., 2020

2014

Conflict-Driven XOR-Clause Learning (extended version).

[BibT_eX]

[DOI]

CoRR, 2014

Classifying and Propagating Parity Constraints (extended version).

[BibT_eX]

[DOI]

CoRR, 2014

2013

Simulating Parity Reasoning (extended version).

[BibT_eX]

[DOI]

CoRR, 2013

Simulating Parity Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Bounded Model Checking of an MITL Fragment for Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Application of Concurrency to System Design, 2013

2012

Exploiting step semantics for efficient bounded model checking of asynchronous systems.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2012

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

[BibT_eX]

[DOI]

CoRR, 2012

Conflict-Driven XOR-Clause Learning.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Extending Clause Learning SAT Solvers with Complete Parity Reasoning.

[BibT_eX]

[DOI]

Proceedings of the IEEE 24th International Conference on Tools with Artificial Intelligence, 2012

Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Systems, 2012

SMT-Based Induction Methods for Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012

Classifying and Propagating Parity Constraints.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2012

2011

Efficient model checking of PSL safety properties.

[BibT_eX]

[DOI]

Tuomas Launiainen

IET Comput. Digit. Tech., 2011

Partitioning Search Spaces of a Randomized Search.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2011

Conflict Propagation and Component Recursion for Canonical Labeling.

[BibT_eX]

[DOI]

Petteri Kaski

Proceedings of the Theory and Practice of Algorithms in (Computer) Systems, 2011

Equivalence Class Based Parity Reasoning with DPLL(XOR).

[BibT_eX]

[DOI]

Proceedings of the IEEE 23rd International Conference on Tools with Artificial Intelligence, 2011

Grid-Based SAT Solving with Iterative Partitioning and Clause Learning.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming - CP 2011, 2011

Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Application of Concurrency to System Design, 2011

2010

Partitioning SAT Instances for Distributed Solving.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Extending Clause Learning DPLL with Parity Reasoning.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2010, 2010

Exact Cover via Satisfiability: An Empirical Study.

[BibT_eX]

[DOI]

Petteri Kaski

Proceedings of the Principles and Practice of Constraint Programming - CP 2010, 2010

2009

Non-Clausal SAT and ATPG.

[BibT_eX]

[DOI]

Rolf Drechsler

Proceedings of the Handbook of Satisfiability, 2009

Incorporating Clause Learning in Grid-Based Randomized SAT Solving.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2009

Limitations of restricted branching in clause learning.

[BibT_eX]

[DOI]

Constraints An Int. J., 2009

Structure-aware computation of predicate abstraction.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008

Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Justification-Based Local Search with Adaptive Noise Strategies.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Symbolic Step Encodings for Object Based Communicating State Machines.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

Justification-Based Non-Clausal Local Search for SAT.

[BibT_eX]

[DOI]

Proceedings of the ECAI 2008, 2008

Strategies for Solving SAT in Grids by Randomized Search.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

Incorporating Learning in Grid-Based Randomized SAT Solving.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence: Methodology, 2008

Symbolic model checking of hierarchical UML state machines.

[BibT_eX]

[DOI]

Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD 2008), 2008

On the Power of Top-Down Branching Heuristics.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, 2008

2007

Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs.

[BibT_eX]

[DOI]

Petteri Kaski

Proceedings of the Nine Workshop on Algorithm Engineering and Experiments, 2007

2006

Linear Encodings of Bounded LTL Model Checking.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2006

Efficient theory combination via boolean search.

[BibT_eX]

[DOI]

Inf. Comput., 2006

A Distribution Method for Solving SAT in Grids.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Bounded Model Checking for Weak Alternating Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Unrestricted vs restricted cut in a tableau method for Boolean circuits.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 2005

Simple Is Better: Efficient Bounded Model Checking for Past LTL.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2005

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

Incremental and Complete Bounded Model Checking for Full PLTL.

[BibT_eX]

[DOI]

Timo Latvala

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Efficient Satisfiability Modulo Theories via Delayed Theory Combination.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

The MathSAT 3 System.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2005

2004

Simple Bounded LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

New Canonical Representative Marking Algorithms for Place/Transition-Nets.

[BibT_eX]

[DOI]

Proceedings of the Applications and Theory of Petri Nets 2004, 2004

New Orbit Algorithms for Data Symmetries.

[BibT_eX]

[DOI]

Proceedings of the 4th International Conference on Application of Concurrency to System Design (ACSD 2004), 2004

2001

Computational Complexity of the Place/Transition-Net Symmetry Reduction Method.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2001

2000

Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking.

[BibT_eX]

[DOI]

Proceedings of the Computational Logic, 2000

1999

Finding Symmetries of Algebraic System Nets.

[BibT_eX]

[DOI]