Boolean Variable Ordering optimizations

diff --git a/src/AST/astops.h b/src/AST/astops.h
index 97d2c28e3b92cc3e97bbc9d63455266d91d09232..a451c5f5cdc023797c59f21afd28e1b3fe1d77a5 100644 (file)
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -25,6 +25,9 @@ enum ElementEncodingType {
 
 typedef enum ElementEncodingType ElementEncodingType;
 
+enum BooleanVarOrdering {CONSTRAINTORDERING=0, CHORONOLOGICALORDERING=1, REVERSEORDERING=2};
+typedef enum BooleanVarOrdering BooleanVarOrdering;
+
 Polarity negatePolarity(Polarity This);
 bool impliesPolarity(Polarity curr, Polarity goal);
 

diff --git a/src/ASTTransform/varorderingopt.cc b/src/ASTTransform/varorderingopt.cc
new file mode 100644 (file)
index 0000000..41f3edb
--- /dev/null
+++ b/src/ASTTransform/varorderingopt.cc
@@ -0,0 +1,52 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   VarOrderingOpt.cpp
+ * Author: hamed
+ * 
+ * Created on October 11, 2018, 5:31 PM
+ */
+
+#include "varorderingopt.h"
+#include "csolver.h"
+#include "tunable.h"
+#include "satencoder.h"
+#include "elementencoding.h"
+#include "element.h"
+
+VarOrderingOpt::VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder): Transform(_solver){
+       satencoder = _satencoder;
+}
+
+VarOrderingOpt::~VarOrderingOpt() {
+}
+
+void VarOrderingOpt::doTransform(){
+       BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
+       if ( direction == CONSTRAINTORDERING ){
+               return;
+       }
+       
+       uint size = solver->allElements.getSize();
+       if(direction == CHORONOLOGICALORDERING){
+               for (uint i = 0; i < size; i++) {
+                       Element *el = solver->allElements.get(i);
+                       ElementEncoding *encoding = el->getElementEncoding();
+                       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED)
+                               continue;
+                       satencoder->encodeElementSATEncoder(el);
+               }
+       }else{
+               for (int i = size-1; i>0; i--) {
+                       Element *el = solver->allElements.get(i);
+                       ElementEncoding *encoding = el->getElementEncoding();
+                       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED)
+                               continue;
+                       satencoder->encodeElementSATEncoder(el);
+               }
+       }
+}

diff --git a/src/ASTTransform/varorderingopt.h b/src/ASTTransform/varorderingopt.h
new file mode 100644 (file)
index 0000000..efb0152
--- /dev/null
+++ b/src/ASTTransform/varorderingopt.h
@@ -0,0 +1,30 @@
+/*
+ * To change this license header, choose License Headers in Project Properties.
+ * To change this template file, choose Tools | Templates
+ * and open the template in the editor.
+ */
+
+/* 
+ * File:   VarOrderingOpt.h
+ * Author: hamed
+ *
+ * Created on October 11, 2018, 5:31 PM
+ */
+
+#ifndef VARORDERINGOPT_H
+#define VARORDERINGOPT_H
+
+#include "transform.h"
+
+
+class VarOrderingOpt :Transform {
+public:
+        VarOrderingOpt(CSolver *_solver, SATEncoder *_satencoder);
+        void doTransform();
+        virtual ~VarOrderingOpt();
+private:
+        SATEncoder* satencoder;
+};
+
+#endif /* VARORDERINGOPT_H */
+

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 56be737580859e0e33ae5b52bd5953287a8f2847..827a9041b059922d78607771352bf7b615cd9a34 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -69,6 +69,7 @@ private:
        CSolver *solver;
        BooleanToEdgeMap booledgeMap;
        VectorEdge *vector;
+        friend class VarOrderingOpt;
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index da3d44a8ec3dd521e496668eec9f3a1bd489dc76..d8385477e84198be6fe67534210d0b319275907d 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -42,9 +42,10 @@ static TunableDesc proxyparameter(1, 5, 2);
 static TunableDesc mustValueBinaryIndex(5, 9, 8);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
+static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
-                                                        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, 
+        ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER};
 typedef enum Tunables Tunables;
 
 const char *tunableParameterToString(Tunables tunable);

diff --git a/src/csolver.cc b/src/csolver.cc
index 5a914e8af15d4c7b1dcf53b56329feccf4b2f9a9..a8ffc492c156064cb6fdb693b7084b76c737d478 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -26,6 +26,7 @@
 #include "orderedge.h"
 #include "orderanalysis.h"
 #include "elementopt.h"
+#include "varorderingopt.h"
 #include <time.h>
 #include <stdarg.h>
 
@@ -622,9 +623,12 @@ int CSolver::solve() {
        naiveEncodingDecision(this);
 //     eg.validate();
 
+       VarOrderingOpt bor(this, satEncoder);
+       bor.doTransform();
+       
        time2 = getTimeNano();
        model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
+       
        satEncoder->encodeAllSATEncoder(this);
        time1 = getTimeNano();
 

diff --git a/src/csolver.h b/src/csolver.h
index fd6487afb092c688a293f6e40e2d3e193befced5..1bc24769a7edee9e78cf2025b0e855b8d3fbf423 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -222,6 +222,7 @@ private:
        long long elapsedTime;
        long satsolverTimeout;
        friend class ElementOpt;
+        friend class VarOrderingOpt;
 };
 
 inline CompOp flipOp(CompOp op) {