While there exist several approaches in the constraint programming community to learn a constraint theory, few of them have considered the learning of constraint optimization problems.To alleviate this situation, we introduce an initial approach to learning first-order weighted MAX-SAT theories. It employs inductive logic programming techniques to learn a set of first-order clauses and then uses preference learning techniques to learn the weights of the clauses.In order to learn these weighted clauses, the clausal optimization system uses examples of possible worlds and a set of preferences that state which examples are preferred over other ones.The technique is also empirically evaluated on a number of examples.These experiments show that the system is capable of learning clauses and weights that accurately capture underlying models.

This paper describes a collection of ideas that allow large games of imperfect information to be solved with counterfactual regret minimization (CFR) using little memory. We replace the regret matching component of CFR with a simple approach known as "follow-the-leader." This helps us quantize the regret values computed in CFR to a single byte. We also investigate not maintaining the accumulated strategy, which saves additional memory. Ultimately, our collection of techniques allows CFR to be run with only 1/16 of the memory required by classic approaches. We present experimental results on poker.

Model counting and weighted model counting are key problems in artificial intelligence. Marginal inference can be reduced to model counting in many statistical-relational systems, such as Markov Logic. One common approach used by model counters is splitting a theory into disjoint subtheories, performing model counting on the subtheories, and then caching the result. If an identical subtheory is encountered again in the search, the cached result is used, greatly reducing runtime. In this work we introduce a way to cache symmetric subtheories compactly, which could potentially decrease required cache size, increase cache hits, and decrease runtime of solving.

Recent work by Janhunen, Tasharrofi, and Ternovska (2016) started from the following observation: "if SAT From the result of this oracle call, a learned clause is generated and added to ϕ. Now that formalism; (2) It can be immediately combined with other these highly-performant SATsolvers exist, research often SAT extensions (such as integer variables, acyclicity, or any stretches beyond SAT, either because of trying to tackle other theory propagator); (3) No dedicated propagators need problems of a complexity higher than NP or because the input to be developed for the new extension because the nested format of SAT solvers (propositional logic) is too limited solver is (automatically) used as a propagator for its internal to concisely and naturally express certain domain specific theory; for example, it was shown by Janhunen, Tasharrofi, constraints, such as graph properties.

Many problems from the area of AI have been shown tractable for bounded treewidth. In order to put such results into practice, quite involved dynamic programming (DP) algorithms on tree decompositions have to be designed and implemented. These algorithms typically show recurring patterns that call for tasks like subset minimization. In this paper, we provide a new method for obtaining DP algorithms from simpler principles, where the necessary data structures and algorithms for subset minimization are automatically generated. Moreover, we discuss how this method can be implemented in systems that perform more space-efficiently than current approaches.

We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Wintersteiger et al, who give experimental evidence that extended Q-resolution is stronger than weak extended Q-resolution. Here we prove an exponential separation between the two systems, thereby confirming the conjecture of Wintersteiger et al. Conceptually, this separation relies on showing strategy extraction for weak extended Q-resolution by bounded-depth circuits. In contrast, we show that this strong strategy extraction result fails in extended Q-resolution.

2QBF is a special case of general quantified Boolean formulae (QBF). It is limited to just two quantification levels, i.e., to a form forall-exists. Despite this limitation it applies to a wide range of applications, e.g., to artificial intelligence, graph theory, synthesis, etc.. Recent research showed that CEGAR-based methods give a performance boost to QBF solving (e.g, compared to QDPLL). Conjunctive normal form (CNF) is a commonly accepted representation for both SAT and QBF problems; however, it does not reflect the circuit structure that might be present in the problem. Existing attempts of extracting this structure from CNF and using it in 2QBF context do not show advantages over CNF based 2QBF solvers. In this work we introduce a new workflow for 2QBF, containing a new semantic circuit extraction algorithm and a CEGAR-based 2QBF solver that uses circuit structure and is improved by a so-called "cofactor sharing'' heuristics. We evaluate the proposed methodology on a range of benchmarks and show the practicality of the new approach.

The increasing penetration of renewable energy sources and electric vehicles raises important challenges related to the operation of electricity grids. For instance, the amount of power generated by wind turbines is time-varying and dependent on the weather, which makes it hard to match flexible electric vehicle demand and uncertain wind power supply. In this paper we propose a vehicle aggregation framework which uses Markov Decision Processes to control charging of multiple electric vehicles and deals with uncertainty in renewable supply. We present a grouping technique to address the scalability aspects of our framework. In experiments we show that the aggregation framework maximizes the profit of the aggregator while reducing usage of conventionally-generated power and cost of customers.

With the efforts of moving to sustainable and reliable energy supply, electricity markets are undergoing far-reaching changes. Due to the high-cost of failure in the real-world, it is important to test new market structures in simulation. This is the focus of the Power Trading Agent Competition (Power TAC), which proposes autonomous electricity broker agents as a means for stabilizing the electricity grid. This paper focuses on the question: how should an autonomous electricity broker agent act in competitive electricity markets to maximize its profit. We formalize the complete electricity trading problem as a continuous, high-dimensional Markov Decision Process (MDP), which is computationally intractable to solve. Our formalization provides a guideline for approximating the MDP's solution, and for extending existing solutions. We show that a previously champion broker can be viewed as approximating the solution using a lookahead policy. We present TacTex15, which improves upon this previous approximation and achieves state-of-the-art performance in competitions and controlled experiments. Using thousands of experiments against 2015 finalist brokers, we analyze TacTex15's performance and the reasons for its success. We find that lookahead policies can be effective, but their performance can be sensitive to errors in the transition function prediction, specifically demand-prediction.

The current approaches to model dynamism in DCOPs solve a sequence of static problems, reacting to the changes in the environment as the agents observe them. Such approaches, thus, ignore possible predictions on the environment evolution. To overcome such limitations, we introduce the Proactive Dynamic DCOP (PD-DCOP) model, a novel formalism to model dynamic DCOPs in the presence of exogenous uncertainty. In contrast to reactive approaches, PD-DCOPs are able to explicitly model the possible changes to the problem, and take such information into account proactively, when solving the dynamically changing problem.