Author name cluster

Charles Jordan

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

SAT Conference 2014 Conference Paper

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing

Charles Jordan
Lukasz Kaiser
Florian Lonsing
Martina Seidl

Abstract Inspired by recent work on parallel SAT solving, we present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular, our approach uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes. It abstains from globally exchanging information between the workers, but keeps learnt information only locally. To this end, we equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated it in our novel solver MPIDepQBF as backend solver. Extensive experiments on standard computers as well as on the supercomputer Tsubame show the impact of our approach.

Details

SAT Conference 2013 Conference Paper

Experiments with Reduction Finding

Charles Jordan
Lukasz Kaiser

Abstract Reductions are perhaps the most useful tool in complexity theory and, naturally, it is in general undecidable to determine whether a reduction exists between two given decision problems. However, asking for a reduction on inputs of bounded size is essentially a \(\Sigma^p_2\) problem and can in principle be solved by ASP, QBF, or by iterated calls to SAT solvers. We describe our experiences developing and benchmarking automatic reduction finders. We created a dedicated reduction finder that does counter-example guided abstraction refinement by iteratively calling either a SAT solver or BDD package. We benchmark its performance with different SAT solvers and report the tradeoffs between the SAT and BDD approaches. Further, we compare this reduction finder with the direct approach using a number of QBF and ASP solvers. We describe the tradeoffs between the QBF and ASP approaches and show which solvers perform best on our \(\Sigma^p_2\) instances. It turns out that even state-of-the-art solvers leave a large room for improvement on problems of this kind. We thus provide our instances as a benchmark for future work on \(\Sigma^p_2\) solvers.

Details

Highlights Conference 2013 Conference Abstract

Machine learning using descriptive complexity and SAT-solvers

Łukasz Kaiser
Charles Jordan

In machine learning there is an inherent trade-off between the efficiency of the learning algorithm and the expressiveness of the hypothesis that one is allowed to learn. Even though this trade-off is present in almost every machine learning task, it is hard to capture formally and still often resolved based on instinct and experience. We propose using parametrized logical formulas to represent hypotheses and then exploit propositional solvers for efficient learning and results from descriptive complexity to get expressiveness guarantees. This allows a more systematic study of the above trade-off and, as we show on a few examples, it is applicable to practical learning tasks. 11: 12 11: 36 Coffee break

PDF Details