this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
5 *
6 * Copyright:
7 * Vincent Barichard, 2013
8 *
9 * Last modified:
10 * $Date$ by $Author$
11 * $Revision$
12 *
13 * This file is part of Quacode:
14 * http://quacode.barichard.com
15 *
16 * Permission is hereby granted, free of charge, to any person obtaining
17 * a copy of this software and associated documentation files (the
18 * "Software"), to deal in the Software without restriction, including
19 * without limitation the rights to use, copy, modify, merge, publish,
20 * distribute, sublicense, and/or sell copies of the Software, and to
21 * permit persons to whom the Software is furnished to do so, subject to
22 * the following conditions:
23 *
24 * The above copyright notice and this permission notice shall be
25 * included in all copies or substantial portions of the Software.
26 *
27 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
28 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
29 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
30 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
31 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
32 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
33 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
34 *
35 */
36
37#include <iostream>
38#include <vector>
39#include <map>
40
41#include <quacode/qspaceinfo.hh>
42#include <gecode/minimodel.hh>
43#include <gecode/driver.hh>
44
45
46using namespace Gecode;
47
48
49#ifdef GECODE_HAS_GIST
50namespace Gecode { namespace Driver {
51 /// Specialization for QDFS
52 template<typename S>
53 class GistEngine<QDFS<S> > {
54 public:
55 static void explore(S* root, const Gist::Options& opt) {
56 (void) Gist::explore(root, false, opt);
57 }
58 };
59}}
60#endif
61
62
63/**
64 * \brief Options taking one additional parameter
65 */
66class QBFOptions : public Options {
67 /// Print strategy or not
68 Gecode::Driver::BoolOption _printStrategy;
69 Driver::BoolOption _qConstraint; /// Parameter to decide between optimized quantified constraints or usual ones
70public:
71 int n; /// Parameter to be given on the command line
72 /// Initialize options for example with name \a s
73 QBFOptions(const char* s, int n0, bool _qConstraint0)
74 : Options(s),
75 _printStrategy("-printStrategy","Print strategy",false),
76 _qConstraint("-quantifiedConstraints",
77 "whether to use quantified optimized constraints",
78 _qConstraint0),
79 n(n0)
80 {
81 add(_printStrategy);
82 add(_qConstraint);
83 }
84 /// Parse options from arguments \a argv (number is \a argc)
85 void parse(int& argc, char* argv[]) {
86 Options::parse(argc,argv);
87 if (argc < 2)
88 return;
89 n = atoi(argv[1]);
90 }
91 /// Return true if the strategy must be printed
92 bool printStrategy(void) const {
93 return _printStrategy.value();
94 }
95 bool qConstraint(void) const {
96 return _qConstraint.value();
97 }
98 /// Print help message
99 virtual void help(void) {
100 Options::help();
101 std::cerr << "\t(unsigned int) default: " << n << std::endl
102 << "\t\tnumber of the instance used" << std::endl;
103 }
104};
105
106class QBFProblem : public Script, public QSpaceInfo {
107 BoolVarArray X;
108public:
109 QBFProblem(const QBFOptions& opt) : Script(opt), QSpaceInfo()
110 {
111 std::cout << "Loading problem" << std::endl;
112 if (!opt.printStrategy()) strategyMethod(0); // disable build and print strategy
113 using namespace Int;
114
115 X = BoolVarArray(*this,4,0,1);
116 BoolVarArray O(*this,7,0,1);
117
118 switch (opt.n) {
119 case 0:
120// forall{a}(forall{b}(forall{c}(exists{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT ( 6p, 4n, 1f) Q:( 0p, 0n, 1f)
121 setForAll(*this,X[0]);
122 setForAll(*this,X[1]);
123 setForAll(*this,X[2]);
124 break;
125 case 1:
126// forall{a}(forall{b}(exists{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (27p, 10n, 2f) Q:( 3p, 0n, 1f)
127 setForAll(*this,X[0]);
128 setForAll(*this,X[1]);
129 setForAll(*this,X[3]);
130 break;
131 case 2:
132// forall[a](exists[b](forall[c](forall[d] ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (18p, 8n, 2f) Q:( 0p, 0n, 1f)
133 setForAll(*this,X[0]);
134 setForAll(*this,X[2]);
135 setForAll(*this,X[3]);
136 break;
137 case 3:
138// forall{a}(exists{b}(forall{c}(exists{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK SAT (40p, 13n, 2f) Q:(18p, 7n, 1f)
139 setForAll(*this,X[0]);
140 setForAll(*this,X[2]);
141 break;
142 case 4:
143// exists{a}(forall{b}(forall{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (18p, 9n, 2f) Q:( 0p, 0n, 1f)
144 setForAll(*this,X[1]);
145 setForAll(*this,X[2]);
146 setForAll(*this,X[3]);
147 break;
148 case 5:
149// exists{a}(forall{b}(exists{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK UNSAT (53p, 19n, 4f) Q:( 3p, 0n, 1f)
150 setForAll(*this,X[1]);
151 setForAll(*this,X[3]);
152 break;
153 case 6:
154// exists{a}(exists{b}(exists{c}(forall{d} ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK SAT (16p, 5n, 0f) Q:( 9p, 5n, 0f)
155 setForAll(*this,X[3]);
156 break;
157 case 7:
158// exists[a](exists[b](exists[c](exists[d] ((c | b) & (b -> ((c -> d)&(c | (a <-> !d)))))))) OK SAT ( 9p, 4n, 0f) Q:( 9p, 4n, 0f)
159 break;
160 default:
161 GECODE_NEVER;
162 }
163
164
165 if (opt.qConstraint()) {
166 QBoolVar qa, qb, qc, qd;
167 qa = QBoolVar(quantifier(X[0]),X[0],1);
168 qb = QBoolVar(quantifier(X[1]),X[1],2);
169 qc = QBoolVar(quantifier(X[2]),X[2],3);
170 qd = QBoolVar(quantifier(X[3]),X[3],4);
171 qrel(*this, qa, BOT_XOR, qd, O[6]);
172 qrel(*this, qc, BOT_OR, O[6], O[5]);
173 qrel(*this, qc, BOT_IMP, qd, O[4]);
174 qrel(*this, O[4], BOT_AND, O[5], O[3]);
175 qrel(*this, qb, BOT_IMP, O[3], O[2]);
176 qrel(*this, qc, BOT_OR, qb, O[1]);
177 qrel(*this, O[1], BOT_AND, O[2], O[0]);
178 rel(*this, O[0], IRT_EQ, 1);
179 } else {
180 BoolVar qa, qb, qc, qd;
181 qa = X[0];
182 qb = X[1];
183 qc = X[2];
184 qd = X[3];
185 rel(*this, qa, BOT_XOR, qd, O[6]);
186 rel(*this, qc, BOT_OR, O[6], O[5]);
187 rel(*this, qc, BOT_IMP, qd, O[4]);
188 rel(*this, O[4], BOT_AND, O[5], O[3]);
189 rel(*this, qb, BOT_IMP, O[3], O[2]);
190 rel(*this, qc, BOT_OR, qb, O[1]);
191 rel(*this, O[1], BOT_AND, O[2], O[0]);
192 rel(*this, O[0], IRT_EQ, 1);
193 }
194
195 branch(*this, X, INT_VAR_NONE(), INT_VAL_MIN());
196 }
197
198 QBFProblem(bool share, QBFProblem& p) : Script(share,p), QSpaceInfo(*this,share,p)
199 {
200 X.update(*this,share,p.X);
201 }
202
203 virtual Space* copy(bool share) { return new QBFProblem(share,*this); }
204
205 void print(std::ostream& os) const {
206 strategyPrint(os);
207 }
208};
209
210int main(int argc, char* argv[])
211{
212
213 QBFOptions opt("Non CNF, Non Prenex, Quantified Boolean Problem",0,true);
214 opt.parse(argc,argv);
215 Script::run<QBFProblem,QDFS,QBFOptions>(opt);
216
217 return 0;
218}