41#define CHECK_FOR_INTERRUPTS() ((void)0)
84 auto nb_bags =
bags.size();
85 for(
bag_t i{0}; i<nb_bags; ++i) {
92 decltype(copy_children) new_children;
93 new_children.push_back(current);
95 new_children.push_back(copy_children[k]);
103 nb_bags =
bags.size();
104 for(
bag_t i{0}; i<nb_bags; ++i) {
107 for(
size_t j = 1; j <
getBag(i).
size(); ++j) {
110 for(
size_t k = 0; k <
getBag(i).
size() - j; ++k, ++it)
117 std::vector<std::set<gate_t>> gates_in_children(
bags.size());
118 auto getChildrenGates = [&gates_in_children](
bag_t i) ->
auto& {
119 return gates_in_children[
static_cast<std::underlying_type<bag_t>::type
>(i)];
125 getChildrenGates(
getParent(i)).insert(g);
132 nb_bags =
bags.size();
133 for(
bag_t i{0}; i<nb_bags; ++i) {
136 std::vector<gate_t> extra_gates;
138 if(getChildrenGates(i).find(g) == getChildrenGates(i).end())
139 extra_gates.push_back(g);
144 if(!extra_gates.empty()) {
147 if(
getChildren(i).size()==1 && intersection.
size()==getChildrenGates(i).size()) {
152 auto gate = extra_gates.back();
155 extra_gates.pop_back();
159 for(
auto g: extra_gates) {
175 const std::vector<bag_t> &ch)
223 std::string result=
"digraph circuit{\n graph [rankdir=UD] ;\n";
227 result +=
" " +
to_string(i) +
" [label=\"{";
229 for(
auto gate:
getBag(i)) {
252 unsigned long nb_bags;
255 td.
bags.resize(nb_bags);
256 td.
parent.resize(nb_bags);
259 for(
bag_t i{0}; i<nb_bags; ++i) {
270 for(
unsigned long j=0; j<nb_gates; ++j) {
285 unsigned long nb_children;
288 for(
unsigned long j=0; j<nb_children; ++j) {
311 unsigned max_width{0};
312 std::unordered_map<gate_t, bag_t> bag_ids;
323 CHECK_FOR_INTERRUPTS();
325 unsigned long node = strategy.
get_next();
327 std::unordered_set<unsigned long> neigh = graph.
remove_node(node);
328 max_width = std::max<unsigned>(neigh.size(), max_width);
344 bag_ids[
gate_t{node}] = bag_id++;
357 bags.push_back(remaining_bag);
371 auto it = bag_ids.find(n);
372 if(it!=bag_ids.end() && it->second!=i)
373 min_bag = std::min(it->second, min_bag);
Boolean provenance circuit with support for knowledge compilation.
gate_t
Strongly-typed gate identifier.
Priority-queue-based node-elimination ordering for tree decomposition.
std::istream & operator>>(std::istream &in, TreeDecomposition &td)
Read a tree decomposition in PACE challenge format.
Tree decomposition of a Boolean circuit for knowledge compilation.
std::string to_string(bag_t b)
Convert a bag_t to its decimal string representation.
bag_t
Strongly-typed bag identifier for a tree decomposition.
Boolean circuit for provenance formula evaluation.
Mutable adjacency-list graph over unsigned-long node IDs.
void fill(const std::unordered_set< unsigned long > &nodes, bool undirected=true)
Add all missing edges within nodes (clique fill).
const std::unordered_set< unsigned long > & get_nodes() const
Return the set of all node IDs in the graph.
std::unordered_set< unsigned long > remove_node(unsigned long node)
Remove node and all its incident edges.
unsigned long number_nodes() const
Return the number of nodes in the graph.
Node-elimination ordering strategy using a priority queue.
unsigned long get_next()
Pop and return the node with the smallest statistic.
virtual void recompute(const std::unordered_set< unsigned long > &nodes, Graph &graph)
Recompute statistics for a subset of nodes and update the queue.
bool empty()
Return true if the queue is empty.
void init_permutation(Graph &graph)
Populate the priority queue with all nodes in graph.
Exception thrown when a tree decomposition cannot be constructed.
bag_t findGateConnection(gate_t v) const
Find the bag whose gate set is closest to gate v (for rooting).
bag_t addEmptyBag(bag_t parent, const std::vector< bag_t > &children=std::vector< bag_t >())
Insert a new empty bag as a child of parent.
std::vector< Bag > bags
Bag contents, indexed by bag_t.
void addGateToBag(gate_t g, bag_t b)
Add gate g to the contents of bag b.
flat_set< gate_t, small_vector > Bag
The type of a bag: a small flat set of gate IDs.
void setParent(bag_t b, bag_t p)
Set the parent of bag b to p.
TreeDecomposition()=default
std::string toDot() const
Render the tree decomposition as a GraphViz DOT string.
void reroot(bag_t bag)
Re-root the tree so that bag becomes the root.
static constexpr int OPTIMAL_ARITY
Preferred maximum arity of bags in the friendly form.
std::vector< bag_t > parent
Parent of each bag (root points to itself).
unsigned treewidth
Treewidth of the decomposition.
bag_t getParent(bag_t b) const
Return the parent of bag b.
static constexpr int MAX_TREEWIDTH
Maximum supported treewidth.
std::vector< std::vector< bag_t > > children
Children of each bag.
bag_t root
Identifier of the root bag.
Bag & getBag(bag_t b)
Mutable access to bag b.
void makeFriendly(gate_t root)
Restructure the tree into the friendly normal form.
std::vector< bag_t > & getChildren(bag_t b)
Mutable access to the children of bag b.
Constructs a d-DNNF from a Boolean circuit and its tree decomposition.
iterator begin()
Return iterator to the first element.
decltype(std::begin(std::declval< const storage_t & >())) const_iterator
size_t size() const
Return the number of elements in the set.
void insert(const K &value)
Insert value if not already present (const-ref overload).