On the Computational Complexity of Non-Dictatorial Aggregation

We investigate when non-dictatorial aggregation is possible from an algorithmic perspective, where non-dictatorial aggregation means that the votes cast by the members of a society can be aggregated in such a way that there is no single member of the society that always dictates the collective outcome. We consider the setting in which the members of a society take a position on a fixed collection of issues, where for each issue several different alternatives are possible, but the combination of choices must belong to a given set X of allowable voting patterns. Such a set X is called a possibility domain if there is an aggregator that is non-dictatorial, operates separately on each issue, and returns values among those cast by the society on each issue. We design a polynomial-time algorithm that decides, given a set X of voting patterns, whether or not X is a possibility domain. Furthermore, if X is a possibility domain, then the algorithm constructs in polynomial time a non-dictatorial aggregator for X. Furthermore, we show that the question of whether a Boolean domain X is a possibility domain is in NLOGSPACE. We also design a polynomial-time algorithm that decides whether X is a uniform possibility domain, that is, whether X admits an aggregator that is non-dictatorial even when restricted to any two positions for each issue. As in the case of possibility domains, the algorithm also constructs in polynomial time a uniform non-dictatorial aggregator, if one exists. Then, we turn our attention to the case where X is given implicitly, either as the set of assignments satisfying a propositional formula, or as a set of consistent evaluations of a sequence of propositional formulas. In both cases, we provide bounds to the complexity of deciding if X is a (uniform) possibility domain. Finally, we extend our results to four types of aggregators that have appeared in the literature: generalized dictatorships, whose outcome is always an element of their input, anonymous aggregators, whose outcome is not affected by permutations of their input, monotone, whose outcome does not change if more individuals agree with it and systematic, which aggregate every issue in the same way.

Lilotane: A Lifted SAT-based Approach to Hierarchical Planning

One of the oldest and most popular approaches to automated planning is to encode the problem at hand into a propositional formula and use a Satisfiability (SAT) solver to find a solution. In all established SAT-based approaches for Hierarchical Task Network (HTN) planning, grounding the problem is necessary and oftentimes introduces a combinatorial blowup in terms of the number of actions and reductions to encode. Our contribution named Lilotane (Lifted Logic for Task Networks) eliminates this issue for Totally Ordered HTN planning by directly encoding the lifted representation of the problem at hand. We lazily instantiate the problem hierarchy layer by layer and use a novel SAT encoding which allows us to defer decisions regarding method arguments to the stage of SAT solving. We show the correctness of our encoding and compare it to the best performing prior SAT encoding in a worst-case analysis. Empirical evaluations confirm that Lilotane outperforms established SAT-based approaches, often by orders of magnitude, produces much smaller formulae on average, and compares favorably to other state-of-the-art HTN planners regarding robustness and plan quality. In the International Planning Competition (IPC) 2020, a preliminary version of Lilotane scored the second place. We expect these considerable improvements to SAT-based HTN planning to open up new perspectives for SAT-based approaches in related problem classes.

Chapter 25. Model Counting

Model counting, or counting the number of solutions of a propositional formula, generalizes SAT and is the canonical #P-complete problem. Surprisingly, model counting is hard even for some polynomial-time solvable cases like 2-SAT and Horn-SAT. Efficient algorithms for this problem will have a significant impact on many application areas that are inherently beyond SAT, such as bounded-length adversarial and contingency planning, and, perhaps most importantly, general probabilistic inference. Model counting can be solved, in principle and to an extent in practice, by extending the two most successful frameworks for SAT algorithms, namely, DPLL and local search. However, scalability and accuracy pose a substantial challenge. As a result, several new ideas have been introduced in the last few years that go beyond the techniques usually employed in most SAT solvers. These include division into components, caching, compilation into normal forms, exploitation of solution sampling methods, and certain randomized streamlining techniques using special constraints. This chapter discusses these techniques, exploring both exact methods as well as fast estimation approaches, including those that provide probabilistic or statistical guarantees on the quality of the reported lower or upper bound on the model count.

Chapter 27. Non-Clausal SAT and ATPG

When studying the propositional satisfiability problem (SAT), that is, the problem of deciding whether a propositional formula is satisfiable, it is typically assumed that the formula is given in the conjunctive normal form (CNF). Also most software tools for deciding satisfiability of a formula (SAT solvers) assume that their input is in CNF. An important reason for this is that it is simpler to develop efficient data structures and algorithms for CNF than for arbitrary formulas. On the other hand, using CNF makes efficient modeling of an application cumbersome. Therefore one often employs a more general formula representation in modeling and then transforms the formula into CNF for SAT solvers. Transforming a propositional formula in CNF either increases the formula size exponentially or requires the use of auxiliary variables, which can have an negative effect on the performance of a SAT solver in the worst-case. Moreover, by translating to CNF one often loses information about the structure of the original problem. In this chapter we survey methods for solving propositional satisfiability problems when the input formula is not given in CNF but as a general formula or even more compactly as a Boolean circuit. We show how the techniques applied in CNF level Davis-Putnam-Loveland-Logemann algorithm generalize to Boolean circuits and how the problem structure available in the circuit form can be exploited. Then we consider a closely related area of automatic test pattern generation (ATPG) for digital circuits and review classical ATPG algorithms, formulation of ATPG as a SAT problem, and advanced techniques for SAT-based ATPG.

Boolean Games: Inferring Agents' Goals Using Taxation Queries

In Boolean games, each agent controls a set of Boolean variables and has a goal represented by a propositional formula. We study inference problems in Boolean games assuming the presence of a PRINCIPAL who has the ability to control the agents and impose taxation schemes. Previous work used taxation schemes to guide a game towards certain equilibria. We present algorithms that show how taxation schemes can also be used to infer agents' goals. We present experimental results to demonstrate the efficacy our algorithms. We also consider goal inference when only limited information is available in response to a query.

On the Approximability of Weighted Model Integration on DNF Structures

Weighted model counting (WMC) consists of computing the weighted sum of all satisfying assignments of a propositional formula. WMC is well-known to be #P-hard for exact solving, but admits a fully polynomial randomised approximation scheme (FPRAS) when restricted to DNF structures. In this work, we study weighted model integration, a generalization of weighted model counting which involves real variables in addition to propositional variables, and pose the following question: Does weighted model integration on DNF structures admit an FPRAS? Building on classical results from approximate volume computation and approximate weighted model counting, we show that weighted model integration on DNF structures can indeed be approximated for a class of weight functions. Our approximation algorithm is based on three subroutines, each of which can be a weak (i.e., approximate), or a strong (i.e., exact) oracle, and in all cases, comes along with accuracy guarantees. We experimentally verify our approach over randomly generated DNF instances of varying sizes, and show that our algorithm scales to large problem instances, involving up to 1K variables, which are currently out of reach for existing, general-purpose weighted model integration solvers.

RAT Elimination

Inprocessing techniques have become one of the most promising advancements in SAT solving over the last decade. Some inprocessing techniques modify a propositional formula in non model-perserving ways. These operations are very problematic when Craig inter- polants must be extracted: existing methods take resolution proofs as an input, but these inferences require stronger proof systems; state-of-the-art solvers generate DRAT proofs. We present the first method to transform DRAT proofs into resolution-like proofs by elim- inating satisfiability-preserving RAT inferences. This solves the problem of extracting interpolants from DRAT proofs.

The regression Tsetlin machine: a novel approach to interpretable nonlinear regression

Relying simply on bitwise operators, the recently introduced Tsetlin machine (TM) has provided competitive pattern classification accuracy in several benchmarks, including text understanding. In this paper, we introduce the regression Tsetlin machine (RTM), a new class of TMs designed for continuous input and output, targeting nonlinear regression problems. In all brevity, we convert continuous input into a binary representation based on thresholding, and transform the propositional formula formed by the TM into an aggregated continuous output. Our empirical comparison of the RTM with state-of-the-art regression techniques reveals either superior or on par performance on five datasets. This article is part of the theme issue ‘Harmonizing energy-autonomous computing and intelligence’.

Combining Conflict-Driven Clause Learning and Chronological Backtracking for Propositional Model Counting

In propositional model counting, also named #SAT, the search space needs to be explored exhaustively, in contrast to SAT, where the task is to determine whether a propositional formula is satisfiable. While state-of-the-art SAT solvers are based on non- chronological backtracking, it has also been shown that backtracking chronologically does not significantly degrade solver performance. Hence investigating the combination of chronological backtracking with conflict-driven clause learning (CDCL) for #SAT seems evident. We present a calculus for #SAT combining chronological backtracking with CDCL and provide a formal proof of its correctness.

Finding Optimal Solutions in HTN Planning - A SAT-based Approach

Over the last years, several new approaches to Hierarchical Task Network (HTN) planning have been proposed that increased the overall performance of HTN planners. However, the focus has been on agile planning - on finding a solution as quickly as possible. Little work has been done on finding optimal plans. We show how the currently best-performing approach to HTN planning - the translation into propositional logic - can be utilised to find optimal plans. Such SAT-based planners usually bound the HTN problem to a certain depth of decomposition and then translate the problem into a propositional formula. To generate optimal plans, the length of the solution has to be bounded instead of the decomposition depth. We show the relationship between these bounds and how it can be handled algorithmically. Based on this, we propose an optimal SAT-based HTN planner and show that it performs favourably on a benchmark set.