Boolean Variable Ordering optimizations
authorHamed Gorjiara <hgorjiar@uci.edu>
Fri, 12 Oct 2018 21:54:56 +0000 (14:54 -0700)
committerbdemsky <bdemsky@uci.edu>
Sat, 13 Oct 2018 02:20:30 +0000 (19:20 -0700)
src/AST/astops.h
src/ASTTransform/varorderingopt.cc [new file with mode: 0644]
src/ASTTransform/varorderingopt.h [new file with mode: 0644]
src/Backend/satencoder.h
src/Tuner/tunable.h
src/csolver.cc
src/csolver.h

index 97d2c28..a451c5f 100644 (file)
@@ -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
@@ -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
@@ -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 */
+
index 56be737..827a904 100644 (file)
@@ -69,6 +69,7 @@ private:
        CSolver *solver;
        BooleanToEdgeMap booledgeMap;
        VectorEdge *vector;
+        friend class VarOrderingOpt;
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
index da3d44a..d838547 100644 (file)
@@ -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);
index 5a914e8..a8ffc49 100644 (file)
@@ -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();
 
index fd6487a..1bc2476 100644 (file)
@@ -222,6 +222,7 @@ private:
        long long elapsedTime;
        long satsolverTimeout;
        friend class ElementOpt;
+        friend class VarOrderingOpt;
 };
 
 inline CompOp flipOp(CompOp op) {