|
//---------------------------------------------------------------------
// <copyright file="Solver.cs" company="Microsoft">
// Copyright (c) Microsoft Corporation. All rights reserved.
// </copyright>
//
// @owner Microsoft
// @backupOwner Microsoft
//---------------------------------------------------------------------
using System;
using System.Collections.Generic;
using System.Linq;
namespace System.Data.Common.Utils.Boolean
{
using IfThenElseKey = Triple<Vertex, Vertex, Vertex>;
using System.Diagnostics;
/// <summary>
/// Supports construction of canonical Boolean expressions as Reduced Ordered
/// Boolean Decision Diagrams (ROBDD). As a side effect, supports simplification and SAT:
///
/// - The canonical form of a valid expression is Solver.One
/// - The canonical form of an unsatisfiable expression is Solver.Zero
/// - The lack of redundancy in the trees allows us to produce compact representations
/// of expressions
///
/// Any method taking a Vertex argument requires that the argument is either
/// a 'sink' (Solver.One or Solver.Zero) or generated by this Solver instance.
/// </summary>
internal sealed class Solver
{
#region Fields
readonly Dictionary<IfThenElseKey, Vertex> _computedIfThenElseValues =
new Dictionary<IfThenElseKey, Vertex>();
readonly Dictionary<Vertex, Vertex> _knownVertices =
new Dictionary<Vertex, Vertex>(VertexValueComparer.Instance);
int _variableCount;
// a standard Boolean variable has children '1' and '0'
internal readonly static Vertex[] BooleanVariableChildren = new Vertex[] { Vertex.One, Vertex.Zero };
#endregion
#region Expression factory methods
internal int CreateVariable()
{
return ++_variableCount;
}
internal Vertex Not(Vertex vertex)
{
// Not(v) iff. 'if v then 0 else 1'
return IfThenElse(vertex, Vertex.Zero, Vertex.One);
}
internal Vertex And(IEnumerable<Vertex> children)
{
// assuming input vertices v1, v2, ..., vn:
//
// v1
// 0|\1
// | v2
// |/0 \1
// | ...
// | /0 \1
// | vn
// | /0 \1
// FALSE TRUE
//
// order the children to minimize churn when building tree bottom up
return children
.OrderByDescending(child => child.Variable)
.Aggregate(Vertex.One, (left, right) => IfThenElse(left, right, Vertex.Zero));
}
internal Vertex And(Vertex left, Vertex right)
{
// left AND right iff. if 'left' then 'right' else '0'
return IfThenElse(left, right, Vertex.Zero);
}
internal Vertex Or(IEnumerable<Vertex> children)
{
// assuming input vertices v1, v2, ..., vn:
//
// v1
// 1|\0
// | v2
// |/1 \0
// | ...
// | /1 \0
// | vn
// | /1 \0
// TRUE FALSE
//
// order the children to minimize churn when building tree bottom up
return children
.OrderByDescending(child => child.Variable)
.Aggregate(Vertex.Zero, (left, right) => IfThenElse(left, Vertex.One, right));
}
/// <summary>
/// Creates a leaf vertex; all children must be sinks
/// </summary>
internal Vertex CreateLeafVertex(int variable, Vertex[] children)
{
Debug.Assert(null != children, "children must be specified");
Debug.Assert(2 <= children.Length, "must be at least 2 children");
Debug.Assert(children.All(child => child != null), "children must not be null");
Debug.Assert(children.All(child => child.IsSink()), "children must be sinks");
Debug.Assert(variable <= _variableCount, "variable out of range");
return GetUniqueVertex(variable, children);
}
#endregion
#region Private helper methods
/// <summary>
/// Returns a Vertex with the given configuration. If this configuration
/// is known, returns the existing vertex. Otherwise, a new
/// vertex is created. This ensures the vertex is unique in the context
/// of this solver.
/// </summary>
private Vertex GetUniqueVertex(int variable, Vertex[] children)
{
AssertVerticesValid(children);
Vertex result = new Vertex(variable, children);
// see if we know this vertex already
Vertex canonicalResult;
if (_knownVertices.TryGetValue(result, out canonicalResult))
{
return canonicalResult;
}
// remember the vertex (because it came first, it's canonical)
_knownVertices.Add(result, result);
return result;
}
/// <summary>
/// Composes the given vertices to produce a new ROBDD.
/// </summary>
private Vertex IfThenElse(Vertex condition, Vertex then, Vertex @else)
{
AssertVertexValid(condition);
AssertVertexValid(then);
AssertVertexValid(@else);
// check for terminal conditions in the recursion
if (condition.IsOne())
{
// if '1' then 'then' else '@else' iff. 'then'
return then;
}
if (condition.IsZero())
{
// if '0' then 'then' else '@else' iff. '@else'
return @else;
}
if (then.IsOne() && @else.IsZero())
{
// if 'condition' then '1' else '0' iff. condition
return condition;
}
if (then.Equals(@else))
{
// if 'condition' then 'x' else 'x' iff. x
return then;
}
Vertex result;
IfThenElseKey key = new IfThenElseKey(condition, then, @else);
// check if we've already computed this result
if (_computedIfThenElseValues.TryGetValue(key, out result))
{
return result;
}
int topVariableDomainCount;
int topVariable = DetermineTopVariable(condition, then, @else, out topVariableDomainCount);
// Recursively compute the new BDD node
// Note that we preserve the 'ordered' invariant since the child nodes
// cannot contain references to variables < topVariable, and
// the topVariable is eliminated from the children through
// the call to EvaluateFor.
Vertex[] resultCases = new Vertex[topVariableDomainCount];
bool allResultsEqual = true;
for (int i = 0; i < topVariableDomainCount; i++)
{
resultCases[i] = IfThenElse(
EvaluateFor(condition, topVariable, i),
EvaluateFor(then, topVariable, i),
EvaluateFor(@else, topVariable, i));
if (i > 0 && // first vertex is equivalent to itself
allResultsEqual && // we've already found a mismatch
!resultCases[i].Equals(resultCases[0]))
{
allResultsEqual = false;
}
}
// if the results are identical, any may be returned
if (allResultsEqual)
{
return resultCases[0];
}
// create new vertex
result = GetUniqueVertex(topVariable, resultCases);
// remember result so that we don't try to compute this if-then-else pattern again
_computedIfThenElseValues.Add(key, result);
return result;
}
/// <summary>
/// Given parts of an if-then-else statement, determines the top variable (nearest
/// root). Used to determine which variable forms the root of a composed Vertex.
/// </summary>
private static int DetermineTopVariable(Vertex condition, Vertex then, Vertex @else, out int topVariableDomainCount)
{
int topVariable;
if (condition.Variable < then.Variable)
{
topVariable = condition.Variable;
topVariableDomainCount = condition.Children.Length;
}
else
{
topVariable = then.Variable;
topVariableDomainCount = then.Children.Length;
}
if (@else.Variable < topVariable)
{
topVariable = @else.Variable;
topVariableDomainCount = @else.Children.Length;
}
return topVariable;
}
/// <summary>
/// Returns 'vertex' evaluated for the given value of 'variable'. Requires that
/// the variable is less than or equal to vertex.Variable.
/// </summary>
private static Vertex EvaluateFor(Vertex vertex, int variable, int variableAssigment)
{
if (variable < vertex.Variable)
{
// If the variable we're setting is less than the vertex variable, the
// the Vertex 'ordered' invariant ensures that the vertex contains no reference
// to that variable. Binding the variable is therefore a no-op.
return vertex;
}
Debug.Assert(variable == vertex.Variable,
"variable must be less than or equal to vertex.Variable");
// If the 'vertex' is conditioned on the given 'variable', the children
// represent the decompositions of the function for various assignments
// to that variable.
Debug.Assert(variableAssigment < vertex.Children.Length, "variable assignment out of range");
return vertex.Children[variableAssigment];
}
/// <summary>
/// Checks requirements for vertices.
/// </summary>
[Conditional("DEBUG")]
private void AssertVerticesValid(IEnumerable<Vertex> vertices)
{
Debug.Assert(null != vertices);
foreach (Vertex vertex in vertices)
{
AssertVertexValid(vertex);
}
}
/// <summary>
/// Checks requirements for a vertex argument (must not be null, and must be in scope
/// for this solver)
/// </summary>
[Conditional("DEBUG")]
private void AssertVertexValid(Vertex vertex)
{
Debug.Assert(vertex != null, "vertex must not be null");
// sinks are ok
if (!vertex.IsSink())
{
// so are vertices created by this solver
Vertex comparisonVertex;
Debug.Assert(_knownVertices.TryGetValue(vertex, out comparisonVertex) &&
comparisonVertex.Equals(vertex), "vertex not created by this solver");
}
}
#endregion
/// <summary>
/// Supports value comparison of vertices. In general, we use reference comparison
/// since the Solver ensures a single instance of each canonical Vertex. The Solver
/// needs this comparer to ensure a single instance of each canonical Vertex though...
/// </summary>
private class VertexValueComparer : IEqualityComparer<Vertex>
{
private VertexValueComparer() { }
internal static readonly VertexValueComparer Instance = new VertexValueComparer();
public bool Equals(Vertex x, Vertex y)
{
if (x.IsSink())
{
// sync nodes '1' and '0' each have one static instance; use reference
return x.Equals(y);
}
if (x.Variable != y.Variable ||
x.Children.Length != y.Children.Length)
{
return false;
}
for (int i = 0; i < x.Children.Length; i++)
{
// use reference comparison for the children (they must be
// canonical already)
if (!x.Children[i].Equals(y.Children[i]))
{
return false;
}
}
return true;
}
public int GetHashCode(Vertex vertex)
{
// sync nodes '1' and '0' each have one static instance; use reference
if (vertex.IsSink())
{
return vertex.GetHashCode();
}
Debug.Assert(2 <= vertex.Children.Length, "internal vertices must have at least 2 children");
unchecked
{
return ((vertex.Children[0].GetHashCode() << 5) + 1) + vertex.Children[1].GetHashCode();
}
}
}
}
/// <summary>
/// Record structure containing three values.
/// </summary>
struct Triple<T1, T2, T3> : IEquatable<Triple<T1, T2, T3>>
where T1 : IEquatable<T1>
where T2 : IEquatable<T2>
where T3 : IEquatable<T3>
{
readonly T1 _value1;
readonly T2 _value2;
readonly T3 _value3;
internal Triple(T1 value1, T2 value2, T3 value3)
{
Debug.Assert(null != (object)value1, "null key element");
Debug.Assert(null != (object)value2, "null key element");
Debug.Assert(null != (object)value3, "null key element");
_value1 = value1;
_value2 = value2;
_value3 = value3;
}
public bool Equals(Triple<T1, T2, T3> other)
{
return _value1.Equals(other._value1) &&
_value2.Equals(other._value2) &&
_value3.Equals(other._value3);
}
public override bool Equals(object obj)
{
Debug.Fail("used typed Equals");
return base.Equals(obj);
}
public override int GetHashCode()
{
return _value1.GetHashCode() ^
_value2.GetHashCode() ^
_value3.GetHashCode();
}
}
}
|