Commit e5676273 authored by Daniel Le Berre's avatar Daniel Le Berre

Annotated prime implicant strategy

parent 22374e5e
Pipeline #9069 passed with stages
in 113 minutes and 59 seconds
......@@ -8,4 +8,5 @@ varheuristics=Variable selection heuristics
phaseheuristics=Phase selection policy for a given variable
reader=Reader responsible for feeding the solver
solver=The complexity hierarchy of solvers in Sat4j
solutionlistener=A listener called when a model is found by the solver
\ No newline at end of file
solutionlistener=A listener called when a model is found by the solver
primeimplicant=Prime Implicant computation strategy
\ No newline at end of file
......@@ -31,6 +31,7 @@ package org.sat4j.minisat.core;
import static org.sat4j.core.LiteralsUtils.toInternal;
import org.sat4j.annotations.Feature;
import org.sat4j.core.VecInt;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
......@@ -46,8 +47,9 @@ import org.sat4j.specs.IteratorInt;
* @author leberre
*
*/
public class CounterBasedPrimeImplicantStrategy implements
PrimeImplicantStrategy {
@Feature(value = "primeimplicant", parent = "expert")
public class CounterBasedPrimeImplicantStrategy
implements PrimeImplicantStrategy {
private int[] prime;
......@@ -128,11 +130,11 @@ public class CounterBasedPrimeImplicantStrategy implements
System.out.printf(
"%s prime implicant computation statistics ALGO2%n",
solver.getLogPrefix());
System.out
.printf("%s implied: %d, decision: %d, removed %d (+%d), propagated %d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, posremoved,
propagated, end - begin);
System.out.printf(
"%s implied: %d, decision: %d, removed %d (+%d), propagated %d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, posremoved, propagated,
end - begin);
}
return implicant;
}
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import org.sat4j.annotations.Feature;
/**
* The aim of those classes is to reduce the model found by a SAT solver into a
* prime implicant. See Computing prime implicants, David Deharbe, Pascal
......@@ -37,6 +39,7 @@ package org.sat4j.minisat.core;
* @author leberre
*
*/
@Feature(value = "primeimplicant", parent = "expert")
public interface PrimeImplicantStrategy {
/**
......
......@@ -32,6 +32,7 @@ package org.sat4j.minisat.core;
import static org.sat4j.core.LiteralsUtils.neg;
import static org.sat4j.core.LiteralsUtils.toInternal;
import org.sat4j.annotations.Feature;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.IteratorInt;
......@@ -44,6 +45,7 @@ import org.sat4j.specs.IteratorInt;
* @author leberre
*
*/
@Feature(value = "primeimplicant", parent = "expert")
public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
private int[] prime;
......@@ -55,7 +57,8 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
* a literal
* @return true if no conflict is reached, false if a conflict is found.
*/
boolean setAndPropagate(Solver<? extends DataStructureFactory> solver, int p) {
boolean setAndPropagate(Solver<? extends DataStructureFactory> solver,
int p) {
if (solver.voc.isUnassigned(p)) {
assert !solver.trail.contains(p);
assert !solver.trail.contains(neg(p));
......@@ -154,11 +157,11 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
System.out.printf(
"%s prime implicant computation statistics ORIG%n",
solver.getLogPrefix());
System.out
.printf("%s implied: %d, decision: %d, removed %d (+%d), tested %d, propagated %d), l2 propagation:%d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, posremoved,
tested, propagated, l2propagation, end - begin);
System.out.printf(
"%s implied: %d, decision: %d, removed %d (+%d), tested %d, propagated %d), l2 propagation:%d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, posremoved, tested,
propagated, l2propagation, end - begin);
}
return implicant;
......
......@@ -35,6 +35,7 @@ import static org.sat4j.core.LiteralsUtils.var;
import java.util.Comparator;
import org.sat4j.annotations.Feature;
import org.sat4j.core.VecInt;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVec;
......@@ -53,6 +54,7 @@ import org.sat4j.specs.Propagatable;
* @author leberre
*
*/
@Feature(value = "primeimplicant", parent = "expert")
public class WatcherBasedPrimeImplicantStrategy
implements PrimeImplicantStrategy, MandatoryLiteralListener {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment