Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting (#SAT), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation.Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers.

Model counting (also known as #SAT) is a fundamental problem in knowledge representation and reasoning, with applications ranging from probabilistic inference to formal verification. However, state-of-the-art model counters are limited by computational resources on a single machine. In this paper, we propose a novel distributed framework for model counting, exploiting the embarrassingly parallel nature of the problem. By decomposing the search space into independent subproblems and distributing them across different computation nodes, our approach achieves near-linear scalability on practical instances. Extensive experiments on standard benchmarks demonstrate both the effectiveness and efficiency of our framework.

Quantitative information flow analyses (QIF) are a class of techniques for measuring the amount of confidential information leaked by a program to its public outputs. Shannon entropy is an important method to quantify the amount of leakage in QIF. This paper focuses on the programs modeled in Boolean constraints and optimizes the two stages of the Shannon entropy computation to implement a scalable precise tool PSE. In the first stage, we design a knowledge compilation language called ADD[∧] that combines Algebraic Decision Diagrams and conjunctive decomposition. ADD[∧] avoids enumerating possible outputs of a program and supports tractable entropy computation. In the second stage, we optimize the model counting queries that are used to compute the probabilities of outputs. We compare PSE with the state-of-the-art probabilistic approximately correct tool EntropyEstimation, which was shown to significantly outperform the previous precise tools. The experimental results demonstrate that PSE solved 56 more benchmarks compared to EntropyEstimation in a total of 459. For 98% of the benchmarks that both PSE and EntropyEstimation solved, PSE is at least 10× as efficient as EntropyEstimation.

The Guaranteed Delivery (GD) advertising is a crucial component of the online advertising industry, and the allocation of inventory in GD advertising is an important procedure that influences directly the ability of the publisher to fulfill the requirements and increase its revenues. Nowadays, as the requirements of advertisers become more and more diverse and fine-grained, the focus ratio requirement, which states that the portion of allocated impressions of a designated contract on focus media among all possible media should be greater than another contract, often appears in business scenarios. However, taking these requirements into account brings hardness for the GD advertising inventory allocation as the focus ratio requirements involve non-convex multilinear constraints. Existing methods which rely on the convex properties are not suitable for processing this problem, while mathematical programming or constraint-based heuristic solvers are unable to produce high-quality solutions within the time limit. Therefore, we propose a local search framework to address this challenge. It incorporates four new operators designed for handling multilinear constraints and a two-mode algorithmic architecture. Experimental results demonstrate that our algorithm is able to compute high-quality allocations with better business metrics compared to the state-of-the-art mathematical programming or constraint based heuristic solvers. Moreover, our algorithm is able to handle the general multilinear constraints and we hope it could be used to solve other problems in GD advertising with similar requirements.

The Maximum k-Defective Clique Problem (MDCP), as a clique relaxation model, has been used to solve various problems. Because it is a hard computational task, previous works can hardly solve the MDCP for massive sparse graphs derived from real-world applications. In this work, we propose a novel branch-and-bound algorithm to solve the MDCP based on several new techniques. First, we propose two new upper bounds of the MDCP as well as corresponding reduction rules to remove redundant vertices and edges. The proposed reduction rules are particularly useful for massive graphs. Second, we present another new upper bound by counting missing edges between fixed vertices and an unfixed vertex for cutting branches. We perform extensive computational experiments to evaluate our algorithm. Experimental results show that our reduction rules are very effective for removing redundant vertices and edges so that graphs are reduced greatly. Also, our algorithm can solve benchmark instances efficiently, and it has significantly better performance than state-of-the-art algorithms.