Given a first-order sentence ? and a domain size n, how can one sample a model of ? on the domain {1, . . . , n} efficiently as n scales? We consider two variants of this problem: the uniform sampling regime, in which the goal is to sample a model uniformly at random, and the symmetric weighted sampling regime, in which models are weighted according to the number of groundings of each predicate appearing in them. Solutions to this problem have applications to the scalable generation of combinatorial structures, as well as sampling in several statistical-relational models such as Markov logic networks and probabilistic logic programs. In this paper, we identify certain classes of sentences that are domain-liftable under sampling, in the sense that they admit a sampling algorithm that runs in time polynomial in n. In particular, we prove that every sentence of the form âˆ€xâˆ€y: ?(x, y) for some quantifier-free formula ?(x,y) is domain-liftable under sampling. We then further show that this result continues to hold in the presence of one or more cardinality constraints as well as a single tree axiom constraint.

Domain-Lifted Sampling for Universal Two-Variable Logic and Extensions

Given a propositional formula Ïˆ, the model counting problem, also referred to as #SAT, seeks to compute the number of satisfying assignments (or models) of Ïˆ. Modern search-based model counting algorithms are built on conflict-driven clause learning, combined with the caching of certain subformulas (called components) encountered during the search process. Despite significant progress in these algorithms over the years, state-of-the-art model counters often struggle to handle large but structured instances that typically arise in combinatorial settings. Motivated by the observation that these counters do not exploit the inherent symmetries exhibited in such instances, we revisit the component caching architecture employed in current counters and introduce a novel caching scheme that focuses on identifying symmetric components. We first prove the soundness of our approach, and then integrate it into the state-of-the-art model counter GANAK. Our extensive experiments on hard combinatorial instances demonstrate that the resulting counter, SymGANAK, leads to improvements over GANAK both in terms of PAR-2 score and the number of instances solved.

Symmetric Component Caching for Model Counting on Combinatorial Instances

Main_Track

technical paper

The purpose of the AAAI conference is to promote research in artificial intelligence (AI) and scientific exchange among AI researchers, practitioners, scientists, and engineers in affiliated disciplines. 

Timothy van Bremen

2

SHORT BIO

Presentations

Domain-Lifted Sampling for Universal Two-Variable Logic and Extensions

Symmetric Component Caching for Model Counting on Combinatorial Instances

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES