@Test(groups = "1s") public void testAddClause() throws Exception { Assert.assertEquals(sat.assignment_.get(a), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.assignment_.get(b), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.assignment_.get(c), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.assignment_.get(d), SatSolver.Boolean.kUndefined); Assert.assertTrue(sat.addClause(SatSolver.makeLiteral(a, true))); Assert.assertEquals(sat.assignment_.get(a), SatSolver.Boolean.kFalse); Assert.assertTrue(sat.addClause(SatSolver.makeLiteral(b, false))); Assert.assertEquals(sat.assignment_.get(b), SatSolver.Boolean.kTrue); Assert.assertEquals(sat.qhead_, 2); Assert.assertEquals(sat.clauses.size(), 0); Assert.assertEquals(sat.implies_.size(), 0); }
public boolean addClause(TIntList ps) { assert 0 == trailMarker(); if (!ok_) return false; ps.sort(); int lit = kUndefinedLiteral; int j = 0; for (int i = 0; i < ps.size(); i++) { if (valueLit(ps.get(i)) == Boolean.kTrue || ps.get(i) == negated(lit)) { return true; } else if (valueLit(ps.get(i)) != Boolean.kFalse && ps.get(i) != lit) { lit = ps.get(i); ps.set(j++, lit); } } if (j < ps.size()) { ps.remove(j, ps.size() - j); } switch (ps.size()) { case 0: return (ok_ = false); case 1: uncheckedEnqueue(ps.get(0)); return (ok_ = propagate()); case 2: int l0 = ps.get(0); int l1 = ps.get(1); TIntArrayList i0 = implies_.get(negated(l0)); if (i0 == null) { i0 = new TIntArrayList(); implies_.put(negated(l0), i0); } i0.add(l1); TIntArrayList i1 = implies_.get(negated(l1)); if (i1 == null) { i1 = new TIntArrayList(); implies_.put(negated(l1), i1); } i1.add(l0); break; default: Clause cr = new Clause(ps.toArray()); clauses.add(cr); attachClause(cr); break; } return true; }
SatSolver implements SatFactory { public boolean addClause(TIntList ps) { assert 0 == trailMarker(); if (!ok_) return false; ps.sort(); int lit = kUndefinedLiteral; int j = 0; for (int i = 0; i < ps.size(); i++) { if (valueLit(ps.get(i)) == Boolean.kTrue || ps.get(i) == negated(lit)) { return true; } else if (valueLit(ps.get(i)) != Boolean.kFalse && ps.get(i) != lit) { lit = ps.get(i); ps.set(j++, lit); } } if (j < ps.size()) { ps.remove(j, ps.size() - j); } switch (ps.size()) { case 0: return (ok_ = false); case 1: uncheckedEnqueue(ps.get(0)); return (ok_ = propagate()); case 2: int l0 = ps.get(0); int l1 = ps.get(1); TIntArrayList i0 = implies_.get(negated(l0)); if (i0 == null) { i0 = new TIntArrayList(); implies_.put(negated(l0), i0); } i0.add(l1); TIntArrayList i1 = implies_.get(negated(l1)); if (i1 == null) { i1 = new TIntArrayList(); implies_.put(negated(l1), i1); } i1.add(l0); break; default: Clause cr = new Clause(ps.toArray()); clauses.add(cr); attachClause(cr); break; } return true; } }
SatSolver implements SatFactory { public boolean addClause(TIntList ps) { assert 0 == trailMarker(); if (!ok_) return false; ps.sort(); int lit = kUndefinedLiteral; int j = 0; for (int i = 0; i < ps.size(); i++) { if (valueLit(ps.get(i)) == Boolean.kTrue || ps.get(i) == negated(lit)) { return true; } else if (valueLit(ps.get(i)) != Boolean.kFalse && ps.get(i) != lit) { lit = ps.get(i); ps.set(j++, lit); } } if (j < ps.size()) { ps.remove(j, ps.size() - j); } switch (ps.size()) { case 0: return (ok_ = false); case 1: uncheckedEnqueue(ps.get(0)); return (ok_ = propagate()); case 2: int l0 = ps.get(0); int l1 = ps.get(1); TIntArrayList i0 = implies_.get(negated(l0)); if (i0 == null) { i0 = new TIntArrayList(); implies_.put(negated(l0), i0); } i0.add(l1); TIntArrayList i1 = implies_.get(negated(l1)); if (i1 == null) { i1 = new TIntArrayList(); implies_.put(negated(l1), i1); } i1.add(l0); break; default: Clause cr = new Clause(ps.toArray()); clauses.add(cr); attachClause(cr); break; } return true; } SatSolver(); }
SatSolver implements SatFactory { public boolean addClause(TIntList ps) { assert 0 == trailMarker(); if (!ok_) return false; ps.sort(); int lit = kUndefinedLiteral; int j = 0; for (int i = 0; i < ps.size(); i++) { if (valueLit(ps.get(i)) == Boolean.kTrue || ps.get(i) == negated(lit)) { return true; } else if (valueLit(ps.get(i)) != Boolean.kFalse && ps.get(i) != lit) { lit = ps.get(i); ps.set(j++, lit); } } if (j < ps.size()) { ps.remove(j, ps.size() - j); } switch (ps.size()) { case 0: return (ok_ = false); case 1: uncheckedEnqueue(ps.get(0)); return (ok_ = propagate()); case 2: int l0 = ps.get(0); int l1 = ps.get(1); TIntArrayList i0 = implies_.get(negated(l0)); if (i0 == null) { i0 = new TIntArrayList(); implies_.put(negated(l0), i0); } i0.add(l1); TIntArrayList i1 = implies_.get(negated(l1)); if (i1 == null) { i1 = new TIntArrayList(); implies_.put(negated(l1), i1); } i1.add(l0); break; default: Clause cr = new Clause(ps.toArray()); clauses.add(cr); attachClause(cr); break; } return true; } SatSolver(); @Override SatSolver _me(); int newVariable(); boolean addClause(TIntList ps); boolean learnClause(int... ps); boolean addClause(int l); void cancelUntil(int level); int trailMarker(); int nLearnt(); boolean propagateOneLiteral(int lit); void detachLearnt(int ci); static int makeLiteral(int var, boolean sign); static int negated(int l); static boolean sign(int l); static int var(int l); void copyFrom(SatSolver o); long nbclauses(); long numvars(); }
SatSolver implements SatFactory { public boolean addClause(TIntList ps) { assert 0 == trailMarker(); if (!ok_) return false; ps.sort(); int lit = kUndefinedLiteral; int j = 0; for (int i = 0; i < ps.size(); i++) { if (valueLit(ps.get(i)) == Boolean.kTrue || ps.get(i) == negated(lit)) { return true; } else if (valueLit(ps.get(i)) != Boolean.kFalse && ps.get(i) != lit) { lit = ps.get(i); ps.set(j++, lit); } } if (j < ps.size()) { ps.remove(j, ps.size() - j); } switch (ps.size()) { case 0: return (ok_ = false); case 1: uncheckedEnqueue(ps.get(0)); return (ok_ = propagate()); case 2: int l0 = ps.get(0); int l1 = ps.get(1); TIntArrayList i0 = implies_.get(negated(l0)); if (i0 == null) { i0 = new TIntArrayList(); implies_.put(negated(l0), i0); } i0.add(l1); TIntArrayList i1 = implies_.get(negated(l1)); if (i1 == null) { i1 = new TIntArrayList(); implies_.put(negated(l1), i1); } i1.add(l0); break; default: Clause cr = new Clause(ps.toArray()); clauses.add(cr); attachClause(cr); break; } return true; } SatSolver(); @Override SatSolver _me(); int newVariable(); boolean addClause(TIntList ps); boolean learnClause(int... ps); boolean addClause(int l); void cancelUntil(int level); int trailMarker(); int nLearnt(); boolean propagateOneLiteral(int lit); void detachLearnt(int ci); static int makeLiteral(int var, boolean sign); static int negated(int l); static boolean sign(int l); static int var(int l); void copyFrom(SatSolver o); long nbclauses(); long numvars(); public boolean ok_; public ArrayList<Clause> clauses; public ArrayList<Clause> learnts; public TIntObjectHashMap<TIntArrayList> implies_; public TIntArrayList touched_variables_; }