v0.4.0

Features

• eq: support explanation of equality logic propagation. #137 (Arthur Bit-Monnot)
• solver: Record events for variable creation. #137 (Arthur Bit-Monnot)
• solver: Use equality logic in table constraints. #137 (Arthur Bit-Monnot)
• eq: Distinguish pos and neg edges among enabled edges. #137 (Arthur Bit-Monnot)
• eq: Implement simplification of equality constraints. #137 (Arthur Bit-Monnot)
• planning: Add experimental PSP symmetry breaker. #137 (Arthur Bit-Monnot)
• planning: preprocessing to merge identical condition whose interval meet. #137 (Arthur Bit-Monnot)
• planning: Improved detection of state variables from sets of predicates. #137 (Arthur Bit-Monnot)
• planning: Additional preprocessing of mutex predicates. #137 (Arthur Bit-Monnot)
• planning: In PSP symmetry-braking, ensure actions are not inserted only for detrimental supports. #137 (Arthur Bit-Monnot)
• planning: Exploit Knoblock's hierarchy in symmetry breaking. #137 (Arthur Bit-Monnot)
• cp: add a new method to Solver to enumerate all possible assignments to a set of variables. #137 (Arthur Bit-Monnot)
• planning: add a new preprocesing step that rollup actions. #137 (Arthur Bit-Monnot)
• planning: Improved propagation for table constraints. #137 (Arthur Bit-Monnot)
• planning: Make enforcing minimality optional in PSP symmetry breaking. #137 (Arthur Bit-Monnot)
• planning: Add command line option to lcp to specify known sat/unsat status. #137 (Arthur Bit-Monnot)
• solver: new struct for representing constant values. #137 (Arthur Bit-Monnot)
• planning: Allow unrolling action in the solution plan. #137 (Arthur Bit-Monnot)
• up: Declare support of undefined initial values. #137 (Arthur Bit-Monnot)
• scheduling: Add support for flexible jobshop problems. #149 (Arthur Bit-Monnot)
• csp: initial implementation of the alternative constraint for integer variables #149 (Arthur Bit-Monnot)
• fjs: redundant constraint that may improve lower bound propagation in flexible JSP #149 (Arthur Bit-Monnot)
• csp: Allow reconstructing a snapshot of the state at previous point in the past. #149 (Arthur Bit-Monnot)
• csp: Implement max/min expressions. #149 (Arthur Bit-Monnot)
• jsp: Add new constraint to improve propagation. #149 (Arthur Bit-Monnot)
• search: Add an option to drive search away from last solution in LRB. #149 (Arthur Bit-Monnot)
• cp: Improve explanation of LinearLeq propagator to only have minimal clauses. #149 (Arthur Bit-Monnot)
• search: Support phase saving in the conflict-based brancher. #149 (Arthur Bit-Monnot)
• sat: permanently keep clauses with low LBD #149 (Arthur Bit-Monnot)
• search: Add option to periodically select a random variable. #149 (Arthur Bit-Monnot)
• sat: Allow more option for computing the impact of a variable. #149 (Arthur Bit-Monnot)
• sat: Improve command line options of sat solver (timeout + search tuning) #149 (Arthur Bit-Monnot)
• sat: Add geometric restarts to sat solver. #149 (Arthur Bit-Monnot)
• sat: Add alternating mode (stable/focused) to sat solver. #149 (Arthur Bit-Monnot)
• sched: Improve command line interface, allowing multi-threaded or round-robin strategies. #149 (Arthur Bit-Monnot)
• sat: Enable eager propagation of clauses in the presence of optional variables. #149 (Arthur Bit-Monnot)
• search: Allow lexical to choose between min or max value. #151 (Arthur Bit-Monnot)
• knapsack: Support bounded knapsack problems. #151 (Arthur Bit-Monnot)
• knapsack: Add a dynamic programming implementation fro 0/1 Knapsack #151 (Arthur Bit-Monnot)
• sat: add recursive clause minimization. #151 (Arthur Bit-Monnot)
• cp: add VarEqVarMulLit propagator #149 (Roland Godet)
• cp: add EqVarMulLit to ReifExpr #149 (Roland Godet)
• linear: add multiplication support #149 (Roland Godet)
• planning: encode numeric support constraints #149 (Roland Godet)
• upf: can specify max-depth #149 (Roland Godet)
• sat: Complete version of clause minization #151 (Arthur Bit-Monnot)
• sat: Implement All-UIP clause minimization. #151 (Arthur Bit-Monnot)
• stn: add relevance based theory propagation #151 (Arthur Bit-Monnot)
• stn: additional statistics on the propagation. #151 (Arthur Bit-Monnot)
• stn: Implement Dijkstra-absed bound propagation #151 (Arthur Bit-Monnot)
• collections: Add a variant of RefSet/RefMap that supports O(n) iteration and clearing #152 (Arthur Bit-Monnot)
• planning: add goals in useless support #156 (Roland Godet)
• planning: numeric symmetry breaking #157 (Roland Godet)
• planning: detect fixed fluents as numeric #157 (Roland Godet)
• planning: re-enable action rolling by default #155 (Arthur Bit-Monnot)

Bug Fixes

• plan: Re-enable boolean values in table constraints. #137 (Arthur Bit-Monnot)
• planning: ActivityBoolLight was not used when asked. #137 (Arthur Bit-Monnot)
• planning: Make sure we do not remove an effect that may induce a threat. #137 (Arthur Bit-Monnot)
• planning: Conditions & effect merging resulted in infinite loops. #137 (Arthur Bit-Monnot)
• planning: Allow multiple events in conflict based search. #137 (Arthur Bit-Monnot)
• linear-constraint: Simplification had a sign error. #137 (Arthur Bit-Monnot)
• eq: Work around bug in equality logic propagator. #137 (Arthur Bit-Monnot)
• planning: make sure all action templates are given a fluent-hierarchy level, even if they do not contribute meaningful effects. #137 (Arthur Bit-Monnot)
• planning: do not use plan-space symmetry breaking in hierarchical planning. #137 (Arthur Bit-Monnot)
• planning: conversion of bools into table constraints was incorrect #137 (Arthur Bit-Monnot)
• state-variables: lifting to ST from predicates had an erroneous case. #137 (Arthur Bit-Monnot)
• state-variables: ensure that all conditions can be lifted before commiting to lift a state variable. #137 (Arthur Bit-Monnot)
• state-variables: disable potentially a detrimental support recognition pattern with rare problematic corner cases #137 (Arthur Bit-Monnot)
• planning: check that we can unroll the action before allowing to roll #137 (Arthur Bit-Monnot)
• planning: Deactivate PSP symmetry breaking in numeric planning problems. #137 (Arthur Bit-Monnot)
• up: remove declared support for undefined values in the validator #137 (Arthur Bit-Monnot)
• up: Maximization of final value was incorrect (minimizing the value instead) #139 (Arthur Bit-Monnot)
• up: solution serialization sometime failed in the presence of non-symbolic parameters #141 (Arthur Bit-Monnot)
• sat: Relax an overly conservative check in LearningRate branching heuristic. #149 (Arthur Bit-Monnot)
• fjs: An instance had an incorrect number of machines #149 (Arthur Bit-Monnot)
• sat: Enforce SAT to be the first propagator to ensure its invariants remain. #149 (Arthur Bit-Monnot)
• csp: tautology propagator had an over-zealous sanity check. #149 (Arthur Bit-Monnot)
• jsp: Fix encoding that missed some terms in redundant linear constraint. #149 (Arthur Bit-Monnot)
• sched: Fix a constraint for the case where a machine could have no assigned tasks. #149 (Arthur Bit-Monnot)
• search: set default value for conflict based brancher #149 (Roland Godet)
• domains: implying literals for decision leading to empty domain #149 (Roland Godet)
• ci: Update sat solver command line arguments #149 (Arthur Bit-Monnot)
• sat: Keep watches on true literals if clause is satisfied. #149 (Arthur Bit-Monnot)
• sat: provide stronger explanation in STN theory propagation. #149 (Arthur Bit-Monnot)
• sat: Properly handle tautologies in clause minimization. #151 (Arthur Bit-Monnot)
• stn: Detection of a cycle with optional variables would incorrectly flag a conflict. #149 (Arthur Bit-Monnot)
• sat: Remove overly restrictive assertion on clause form. #151 (Arthur Bit-Monnot)
• reif: evaluation of EqVarMulLit when lhs is present but rhs is absent #149 (Roland Godet)
• reif: specify EqVarMulLit is not negatable #149 (Roland Godet)
• env: move comments to be parsable #149 (Roland Godet)
• sat: Clause minimization was incorrect when dealing with entailed literals. #151 (Arthur Bit-Monnot)
• encode: add some static implications #149 (Roland Godet)
• planning: Make sure we do not attempt to solve a finite problem if deadline has pased already #151 (Arthur Bit-Monnot)
• linter: Correct doc formating #151 (Arthur Bit-Monnot)
• stn: Upon cycle detection, we uselessly continued processing which could trigger a pedantic debug assertion #153 (Arthur Bit-Monnot)
• stn: guard against overflows in dynamic edges #158 (Arthur Bit-Monnot)
• ci: update Cargo.lock #158 (Arthur Bit-Monnot)
• planning: detrimental detection of non-single useful value #156 (Roland Godet)
• planning: detrimental loop through transition value #156 (Roland Godet)
• planning: add mis-removed condition #157 (Roland Godet)
• planning: correctly represent synthetic conditions introduced for numerics #157 (Arthur Bit-Monnot)
• grpc: use planning extract_plan_actions to build the actions #155 (Roland Godet)

Documentation

• planning: Add clear comment about useful values in detrimental supports #156 (Roland Godet)
• planning: Explication for the lexicographic ordering #157 (Roland Godet)

Styles

• cargo clippy #149 (Roland Godet)
• cargo clippy #149 (Roland Godet)
• linters #149 (Roland Godet)
• planning: clean up #156 (Roland Godet)

Code Refactoring

• planning: enforce linear sum of numeric support constraints #149 (Roland Godet)
• planning: enable ARIES_USELESS_SUPPORTS by default #156 (Roland Godet)
• planning: split extract_plan into smaller functions #155 (Roland Godet)

Performance Improvements

• scheduling: Improve flexible-jobshop model with top level operations. #149 (Arthur Bit-Monnot)
• collections: use an array instead of a bitset for RefSet. #151 (Arthur Bit-Monnot)
• sat: Use the dedicated reasoner for learnt clauses with a single literal. #151 (Arthur Bit-Monnot)
• sat: Limit clause sharing two clauses of size 3 #149 (Arthur Bit-Monnot)
• planning: Deactivate action rolling by default as it seems to substantially arm performance in some domains. #149 (Arthur Bit-Monnot)
• stn: Avoid repropagating inferred edges. #149 (Arthur Bit-Monnot)
• stn: Use theard-local storage for bound propagation persistent memory #151 (Arthur Bit-Monnot)
• stn: add a fast check to see if a variable is a node of the STN #151 (Arthur Bit-Monnot)
• stn: avoid redundant stn theory propagation #151 (Arthur Bit-Monnot)
• stn: improve STN theory propagation to avoid any dynamic allocation #151 (Arthur Bit-Monnot)
• cp: use optimized data structure for accumulating propagators to trigger #152 (Arthur Bit-Monnot)
• stn: allow the addition of dynamic edges that redundantly captures a subset of linear constraints #158 (Arthur Bit-Monnot)
• planning: Avoid unecessary bound-checking conditions on unbounded state variables. #157 (Arthur Bit-Monnot)

Tests

• up: Add UP tests specific to aries in the repository. #142 (Arthur Bit-Monnot)
• sched: Add automated test to check consistency of scheduling results over random variable orderings. #151 (Arthur Bit-Monnot)
• sched: add the option to deactivate the advanced constraints in scheduling model. #151 (Arthur Bit-Monnot)
• solver: Add solution witnesses to be able to detect invalid clauses. #151 (Arthur Bit-Monnot)
• scheduling: improve runtime of tests #151 (Arthur Bit-Monnot)

Continuous Integration

• Update ubuntu version on which tests are run. #141 (Arthur Bit-Monnot)
• request numpy version 1.X.Y to avoid incompatible update #141 (Arthur Bit-Monnot)
• use just rules for CI #142 (Arthur Bit-Monnot)
• add IPC problems using UPF #149 (Roland Godet)
• ipc: group problems using github action workflow commands #149 (Roland Godet)
• ipc: add problems solved in master branch #149 (Roland Godet)
• upgrade artifacct-handling actions (Arthur Bit-Monnot)
• ipc: store slow results #157 (Roland Godet)
• ipc: save best results for comparison #157 (Roland Godet)

Chores

• build basis of equality logic reasoner #137 (Arthur Bit-Monnot)
• eq: Complete propagation of equality logic #137 (Arthur Bit-Monnot)
• eq: initial integration of equality reasoner into the main solver. #137 (Arthur Bit-Monnot)
• eq: allow value nodes in equality graph #137 (Arthur Bit-Monnot)
• eq: complete domain propagation. #137 (Arthur Bit-Monnot)
• eq: complete explanations. #137 (Arthur Bit-Monnot)
• eq: Optimize propagation. #137 (Arthur Bit-Monnot)
• eq: Improve propagation of newly added edges. #137 (Arthur Bit-Monnot)
• explain: Add reasoner id to explanation callback. #137 (Arthur Bit-Monnot)
• explain: Add env param to enable/disable equality logic. #137 (Arthur Bit-Monnot)
• eq: Implement an optimized equality theory that partition variables into potentially unifiable ones. #137 (Arthur Bit-Monnot)
• eq: Update usage of equality theory for splitted version. #137 (Arthur Bit-Monnot)
• Fix compiler warnings. #137 (Arthur Bit-Monnot)
• Add convenience method for constructing Table constraints. #137 (Arthur Bit-Monnot)
• planning: Extract constraint encoding from the main encode method. #137 (Arthur Bit-Monnot)
• fix compilation warnings. #137 (Arthur Bit-Monnot)
• Add convenience method for extracting variables from an SAtom #137 (Arthur Bit-Monnot)
• planning: Move table constraint encoding to separate function. #137 (Arthur Bit-Monnot)
• Exclude non-interesting patterns from action rolling. #137 (Arthur Bit-Monnot)
• solver: Deactivate equality logic by default as it seem to be detrimental on some rare problems. #137 (Arthur Bit-Monnot)
• planning: Very minor improvement of plan output #137 (Arthur Bit-Monnot)
• model: Add method to get the type of an atom. #137 (Arthur Bit-Monnot)
• model: add method to extract replaced variables from a substitution. #137 (Arthur Bit-Monnot)
• model: add From<...> implementations for converting literals to Cst #137 (Arthur Bit-Monnot)
• model: Add a new PartialAssignment trait to enable the partial evaluation of expressions. #137 (Arthur Bit-Monnot)
• renaming to avoid name clash of PartialAssignment #137 (Arthur Bit-Monnot)
• update CI to rust 1.80 and fix new lints #146 (Arthur Bit-Monnot)
• refactor cp module, extracting linear constraint implementation to its own file. #149 (Arthur Bit-Monnot)
• generalize the acceptance of SignedVar in domain manipulation. #149 (Arthur Bit-Monnot)
• csp: Generalize the max propagator. #149 (Arthur Bit-Monnot)
• fix clippy lints #149 (Arthur Bit-Monnot)
• sat: Extract data structure to order literals during explanation. #149 (Arthur Bit-Monnot)
• cp: Simplify linear constraint interface by removing literals. #149 (Arthur Bit-Monnot)
• scheduler: Indicates absence of solutions on the stdout #149 (Arthur Bit-Monnot)
• sched: Also export solution on timeout. #149 (Arthur Bit-Monnot)
• sat: Use f64 to represent the priority. #149 (Arthur Bit-Monnot)
• sched: Make scheduler output easier to parse. #149 (Arthur Bit-Monnot)
• branching: Phase saving should not erase from any solution. #151 (Arthur Bit-Monnot)
• branching: Allow more variants of impact measurement. #151 (Arthur Bit-Monnot)
• knapsack: Improve the knapsack example to enable dynamic-programming like memoization. #151 (Arthur Bit-Monnot)
• sum: better display #149 (Roland Godet)
• planning: repercussion of linear sum update & prepare redesign of numeric support constraints #149 (Roland Godet)
• planning: generalize the reify_or_zero mechanism #149 (Roland Godet)
• model: generalize f_domain for linear sums #149 (Roland Godet)
• lcp: Kill planner if a thread panics. #149 (Arthur Bit-Monnot)
• knapsack: add missing import #151 (Arthur Bit-Monnot)
• lint: Fix clippy lints #149 (Arthur Bit-Monnot)
• jsp: Improve debug formatting of operations. #151 (Arthur Bit-Monnot)
• solver: Display learned clause in logs. #151 (Arthur Bit-Monnot)
• knapsack: Add hidden option to rename objects to ease debugging. #151 (Arthur Bit-Monnot)
• solver: Have the explainers accept a snapshot of the state (possibly from the past) instead of the current state only. #151 (Arthur Bit-Monnot)
• temporarily deactivate clause minimization #151 (Arthur Bit-Monnot)
• solver: Refactor to avoid using BoundValue #151 (Arthur Bit-Monnot)
• solver: Refactor to remove BoundValue(Add) #151 (Arthur Bit-Monnot)
• encode: disable USELESS_SUPPORTS by default #149 (Roland Godet)
• sat: extract recursive redundancy checking to specific method. #151 (Arthur Bit-Monnot)
• sat: Move clause minimization to independent file #151 (Arthur Bit-Monnot)
• can solve specific IPC problems #149 (Roland Godet)
• print ipc output on error #149 (Roland Godet)
• stn: Change bound update propaation API #151 (Arthur Bit-Monnot)
• deprecate iterator-based method on RefSet and upgrade their users to IterableRefSet #152 (Arthur Bit-Monnot)
• deprecate iteration-based methods on RefMap and update their usage #152 (Arthur Bit-Monnot)

Commits

• 297c2a0: wip (Arthur Bit-Monnot) #137
• 5c081d1: tmp (Arthur Bit-Monnot) #137
• a262832: tmp (Arthur Bit-Monnot) #137
• up: Update unified planning dependency. #137 (Arthur Bit-Monnot)
• fix clippy lint for rust 1.79 #137 (Arthur Bit-Monnot)
• f9bb5f0: Merge branch 'master' into equality-logic (Arthur Bit-Monnot) #137
• Add first documentation for parameters from environment variables. #137 (Arthur Bit-Monnot)
• update dependencies #138 (Arthur Bit-Monnot)
• add flexible jobshop instances #149 (Arthur Bit-Monnot)
• cp: Reduce the overhead of constraint propagation. #151 (Arthur Bit-Monnot)
• 1f79e7a: chore(sat) make sure we do not add false to the clause when extending it with the scope (Arthur Bit-Monnot) #151
• 33e95e8: Merge branch 'linear-expl' into knapsack (Arthur Bit-Monnot) #151
• 89d62d7: Merge branch 'linear-expl' into knapsack (Arthur Bit-Monnot) #151
• 920adbc: Merge branch 'linear-expl' into knapsack (Arthur Bit-Monnot) #151
• restriction of update to relevant edges #151 (Arthur Bit-Monnot)
• stn: tests and exploitation of relevant focus #151 (Arthur Bit-Monnot)
• stn: potential functions and edge with negative edges. #151 (Arthur Bit-Monnot)
• stn: Support graphs with negative edges in preliminary implementation. #151 (Arthur Bit-Monnot)
• e12ff39: deactivate bounds propagation by default (Arthur Bit-Monnot) #151
• 8a334ce: Merge branch 'master' into stn-relevant (Arthur Bit-Monnot) #151