We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF) - that is, propositional formulas in which the variables are existentially or universally quantified. Bule allows the user to write a high-level representation of the problem in a natural, rule-based language, that is inspired by stratified Datalog. We implemented a tool of the same name that converts the high-level representation into DIMACS format and thus provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity-theoretic properties of our modeling language, provide a library for common modeling patterns, and evaluate our language and tool on several examples.

Pseudo-Boolean constraints are omnipresent in practical applications, and thus a significant effort has been devoted to the development of good SAT encoding techniques for them. Some of these encodings first construct a Binary Decision Diagram (BDD) for the constraint, and then encode the BDD into a propositional formula. These BDD-based approaches have some important advantages, such as not being dependent on the size of the coefficients, or being able to share the same BDD for representing many constraints. We first focus on the size of the resulting BDDs, which was considered to be an open problem in our research community. We report on previous work where it was proved that there are Pseudo-Boolean constraints for which no polynomial BDD exists. We also give an alternative and simpler proof assuming that NP is different from Co-NP. More interestingly, here we also show how to overcome the possible exponential blowup of BDDs by \emph{coefficient decomposition}. This allows us to give the first polynomial generalized arc-consistent ROBDD-based encoding for Pseudo-Boolean constraints. Finally, we focus on practical issues: we show how to efficiently construct such ROBDDs, how to encode them into SAT with only 2 clauses per node, and present experimental results that confirm that our approach is competitive with other encodings and state-of-the-art Pseudo-Boolean solvers.