libs/ezsat/demo_bit.cc

   1 /*
   2  *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
   3  *
   4  *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.com>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #include "ezminisat.h"
  21 #include <stdio.h>
  22
  23 void print_results(bool satisfiable, const std::vector<bool> &modelValues)
  24 {
  25         if (!satisfiable) {
  26                 printf("not satisfiable.\n\n");
  27         } else {
  28                 printf("satisfiable:");
  29                 for (auto val : modelValues)
  30                         printf(" %d", val ? 1 : 0);
  31                 printf("\n\n");
  32         }
  33 }
  34
  35 int main()
  36 {
  37         ezMiniSAT sat;
  38
  39         // 3 input AOI-Gate
  40         // 'pos_active' encodes the condition under which the pullup path of the gate is active
  41         // 'neg_active' encodes the condition under which the pulldown path of the gate is active
  42         // 'impossible' encodes the condition that both or none of the above paths is active
  43         int pos_active = sat.AND(sat.NOT("A"), sat.OR(sat.NOT("B"), sat.NOT("C")));
  44         int neg_active = sat.OR("A", sat.AND("B", "C"));
  45         int impossible = sat.IFF(pos_active, neg_active);
  46
  47         std::vector<int> modelVars;
  48         std::vector<bool> modelValues;
  49         bool satisfiable;
  50
  51         modelVars.push_back(sat.VAR("A"));
  52         modelVars.push_back(sat.VAR("B"));
  53         modelVars.push_back(sat.VAR("C"));
  54
  55         printf("\n");
  56
  57         printf("pos_active: %s\n", sat.to_string(pos_active).c_str());
  58         satisfiable = sat.solve(modelVars, modelValues, pos_active);
  59         print_results(satisfiable, modelValues);
  60
  61         printf("neg_active: %s\n", sat.to_string(neg_active).c_str());
  62         satisfiable = sat.solve(modelVars, modelValues, neg_active);
  63         print_results(satisfiable, modelValues);
  64
  65         printf("impossible: %s\n", sat.to_string(impossible).c_str());
  66         satisfiable = sat.solve(modelVars, modelValues, impossible);
  67         print_results(satisfiable, modelValues);
  68
  69         return 0;
  70 }
  71