A5081120128- Logic, Reasoning, and Knowledge
- Formal Methods in Verification
- Multi-Agent Systems and Negotiation
- Constraint Satisfaction and Optimization
- Bayesian Modeling and Causal Inference
- Logic, programming, and type systems
- Semantic Web and Ontologies
- AI-based Problem Solving and Planning
- Machine Learning and Algorithms
- Software Testing and Debugging Techniques
- Business Process Modeling and Analysis
- Model-Driven Software Engineering Techniques
- Complexity and Algorithms in Graphs
- Advanced Graph Theory Research
- Data Management and Algorithms
- Natural Language Processing Techniques
- Advanced Software Engineering Methodologies
- Distributed and Parallel Computing Systems
- Synthetic Organic Chemistry Methods
- Software Engineering Research
- Data Quality and Management
- Multi-Criteria Decision Making
- Software Reliability and Analysis Research
- Rough Sets and Fuzzy Logic
- Scientific Computing and Data Management
University of Helsinki
2015-2024
Helsinki Institute for Information Technology
2012-2021
Helsinki Art Museum
2017-2020
Institute of Information Science
2017
TU Wien
2017
York University
2010
Helsinki Institute of Physics
2005-2008
The International SAT Solver Competition is today an established series of competitive events aiming at objectively evaluating the progress in state‐of‐the‐art procedures for solving Boolean satisfiability (SAT) instances. Over years, competitions have significantly contributed to fast solver technology that has made a practical success story computer science. This short article provides overview competitions.
The SAT Competitions constitute a well-established series of yearly open international algorithm implementation competitions, focusing on the Boolean satisfiability (or propositional satisfiability, SAT) problem. In this article, we provide detailed account 2020 instantiation Competition, including new competition tracks and benchmark selection procedures, overview solving strategies implemented in top-performing solvers, analysis empirical data obtained from running competition.
We give an overview of SAT Competition 2016, the 2016 edition thefamous competition for Boolean satisfiability (SAT) solvers with over 20 years history. A key aim is to point out ``what's hot'' in competitions i.e., new developments thecompetition series, including tracks and solver techniquesimplemented some award-winning solvers.
The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization quantified (QSAT) have become central declarative programming paradigms through which real-world instances various computationally hard problems can be efficiently solved. This success has been achieved several breakthroughs in practical implementations decision procedures for SAT QSAT, that is, QSAT solvers. Here, simplification techniques conjunctive normal form (CNF) prenex...
Abstract argumentation frameworks (AFs), originally proposed by Dung, constitute a central formal model for the study of computational aspects in AI. Credulous and skeptical acceptance arguments given AF are well-studied problems both terms theoretical analysis—especially complexity—and development practical decision procedures problems. However, AFs make assumption that all attacks between certain (i.e., present known to exist, missing not exist), which can various settings be restrictive...
Argumentation is an active area of modern artificial intelligence (AI) research, with connections to a range fields, from computational complexity theory and knowledge representation reasoning philosophy social sciences, as well application-oriented work in domains such legal reasoning, multi-agent systems, decision support. frameworks (AFs) abstract argumentation have become the graph-based formal model choice for many approaches AI, semantics defining sets jointly acceptable arguments,...
The challenging task of learning structures probabilistic graphical models is an important problem within modern AI research. Recent years have witnessed several major algorithmic advances in structure for Bayesian networks - arguably the most central class especially what known as score-based setting. A successful generic approach to optimal network (BNSL), based on integer programming (IP), implemented GOBNILP system. Despite recent advances, current understanding foundational aspects...
Due to the wide employment of automated reasoning in analysis and construction correct systems, results reported by engines must be trustworthy. For Boolean satisfiability (SAT) solvers - more recently SAT-based maximum (MaxSAT) trustworthiness is obtained integrating proof logging into solvers, making capable emitting machine-verifiable proofs certify correctness steps performed. In this work, we enable for first time based on VeriPB format multi-objective MaxSAT (MO-MaxSAT) optimization...