Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
SAT4J
sat4j
Commits
61fcb96a
Commit
61fcb96a
authored
Nov 11, 2018
by
Daniel Le Berre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Encapsulated fields of SolverStats to please SonarQube.
Need however to check if it does not impact efficiency.
parent
8a723aa0
Changes
8
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
191 additions
and
56 deletions
+191
-56
org.sat4j.core/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java
...re/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java
+1
-1
org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java
...ore/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java
+1
-1
org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java
...t4j.core/src/main/java/org/sat4j/minisat/core/Solver.java
+16
-16
org.sat4j.core/src/main/java/org/sat4j/minisat/core/SolverStats.java
...ore/src/main/java/org/sat4j/minisat/core/SolverStats.java
+157
-22
org.sat4j.core/src/main/java/org/sat4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java
...at4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java
+11
-11
org.sat4j.core/src/main/java/org/sat4j/minisat/learning/LimitedLearning.java
...main/java/org/sat4j/minisat/learning/LimitedLearning.java
+1
-1
org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/EMARestarts.java
...src/main/java/org/sat4j/minisat/restarts/EMARestarts.java
+2
-2
org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/Glucose21Restarts.java
...in/java/org/sat4j/minisat/restarts/Glucose21Restarts.java
+2
-2
No files found.
org.sat4j.core/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java
View file @
61fcb96a
...
...
@@ -58,7 +58,7 @@ class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
if
(
from
.
getActivity
()
>
2.0
)
{
int
nblevel
=
computeLBD
(
from
);
if
(
nblevel
<
from
.
getActivity
())
{
solver
.
stats
.
u
pdateLBD
++
;
solver
.
stats
.
incU
pdateLBD
()
;
from
.
setActivity
(
nblevel
);
}
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java
View file @
61fcb96a
...
...
@@ -67,7 +67,7 @@ class GlucoseLCDS<D extends DataStructureFactory> implements
solver
.
out
.
log
(
this
.
solver
.
getLogPrefix
()
+
"cleaning "
+
(
learnedConstrs
.
size
()
-
j
)
//$NON-NLS-1$
+
" clauses out of "
+
learnedConstrs
.
size
()
+
" with flag "
+
this
.
flag
+
"/"
+
solver
.
stats
.
c
onflicts
);
//$NON-NLS-1$ //$NON-NLS-2$
+
" clauses out of "
+
learnedConstrs
.
size
()
+
" with flag "
+
this
.
flag
+
"/"
+
solver
.
stats
.
getC
onflicts
()
);
//$NON-NLS-1$ //$NON-NLS-2$
// out.flush();
}
solver
.
learnts
.
shrinkTo
(
j
);
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java
View file @
61fcb96a
...
...
@@ -386,13 +386,13 @@ public class Solver<D extends DataStructureFactory>
this
.
learnts
.
push
(
c
);
c
.
setLearnt
();
c
.
register
();
this
.
stats
.
l
earnedclauses
++
;
this
.
stats
.
incL
earnedclauses
()
;
switch
(
c
.
size
())
{
case
2
:
this
.
stats
.
l
earnedbinaryclauses
++
;
this
.
stats
.
incL
earnedbinaryclauses
()
;
break
;
case
3
:
this
.
stats
.
l
earnedternaryclauses
++
;
this
.
stats
.
incL
earnedternaryclauses
()
;
break
;
default
:
// do nothing
...
...
@@ -886,7 +886,7 @@ public class Solver<D extends DataStructureFactory>
}
}
conflictToReduce
.
shrink
(
i
-
j
);
this
.
stats
.
r
educedliterals
+=
i
-
j
;
this
.
stats
.
incR
educedliterals
(
i
-
j
)
;
}
private
final
IVecInt
analyzetoclear
=
new
VecInt
();
...
...
@@ -908,7 +908,7 @@ public class Solver<D extends DataStructureFactory>
}
}
conflictToReduce
.
shrink
(
i
-
j
);
this
.
stats
.
r
educedliterals
+=
i
-
j
;
this
.
stats
.
incR
educedliterals
(
i
-
j
)
;
}
// Check if 'p' can be removed.' min_level' is used to abort early if
...
...
@@ -972,7 +972,7 @@ public class Solver<D extends DataStructureFactory>
}
}
conflictToReduce
.
shrink
(
i
-
j
);
this
.
stats
.
r
educedliterals
+=
i
-
j
;
this
.
stats
.
incR
educedliterals
(
i
-
j
)
;
}
// Check if 'p' can be removed.' min_level' is used to abort early if
...
...
@@ -1079,7 +1079,7 @@ public class Solver<D extends DataStructureFactory>
// ltrail.size() changes due to propagation
// cannot cache that value.
while
(
this
.
qhead
<
ltrail
.
size
())
{
lstats
.
p
ropagations
++
;
lstats
.
incP
ropagations
()
;
int
p
=
ltrail
.
get
(
this
.
qhead
++);
lslistener
.
propagating
(
toDimacs
(
p
));
lorder
.
assignLiteral
(
p
);
...
...
@@ -1101,7 +1101,7 @@ public class Solver<D extends DataStructureFactory>
this
.
voc
.
watches
(
p
).
moveTo
(
lwatched
);
final
int
size
=
lwatched
.
size
();
for
(
int
i
=
0
;
i
<
size
;
i
++)
{
this
.
stats
.
inspects
++
;
this
.
stats
.
in
cIn
spects
()
;
// try shortcut
// shortcut = shortcuts.get(i);
// if (shortcut != ILits.UNDEFINED && voc.isSatisfied(shortcut))
...
...
@@ -1130,7 +1130,7 @@ public class Solver<D extends DataStructureFactory>
int
p
=
toDimacs
(
constr
.
get
(
0
));
this
.
slistener
.
adding
(
p
);
if
(
constr
.
size
()
==
1
)
{
this
.
stats
.
l
earnedliterals
++
;
this
.
stats
.
incL
earnedliterals
()
;
this
.
slistener
.
learnUnit
(
p
);
}
else
{
this
.
learner
.
learns
(
constr
);
...
...
@@ -1206,7 +1206,7 @@ public class Solver<D extends DataStructureFactory>
private
Lbool
search
(
IVecInt
assumps
)
{
assert
this
.
rootLevel
==
decisionLevel
();
this
.
stats
.
s
tarts
++
;
this
.
stats
.
incS
tarts
()
;
int
backjumpLevel
;
// varDecay = 1 / params.varDecay;
...
...
@@ -1222,7 +1222,7 @@ public class Solver<D extends DataStructureFactory>
if
(
confl
==
null
)
{
// No conflict found
if
(
decisionLevel
()
==
0
&&
this
.
isDBSimplificationAllowed
)
{
this
.
stats
.
r
ootSimplifications
++
;
this
.
stats
.
incR
ootSimplifications
()
;
boolean
ret
=
simplifyDB
();
assert
ret
;
}
...
...
@@ -1263,7 +1263,7 @@ public class Solver<D extends DataStructureFactory>
}
if
(
this
.
sharedConflict
==
null
)
{
// New variable decision
this
.
stats
.
d
ecisions
++
;
this
.
stats
.
incD
ecisions
()
;
int
p
=
this
.
order
.
select
();
if
(
p
==
ILits
.
UNDEFINED
)
{
// check (expensive) if all the constraints are not
...
...
@@ -1300,7 +1300,7 @@ public class Solver<D extends DataStructureFactory>
}
if
(
confl
!=
null
)
{
// conflict found
this
.
stats
.
c
onflicts
++
;
this
.
stats
.
incC
onflicts
()
;
this
.
slistener
.
conflictFound
(
confl
,
decisionLevel
(),
this
.
trail
.
size
());
this
.
conflictCount
.
newConflict
();
...
...
@@ -1494,7 +1494,7 @@ public class Solver<D extends DataStructureFactory>
}
protected
final
void
reduceDB
()
{
this
.
stats
.
r
educeddb
++
;
this
.
stats
.
incR
educeddb
()
;
this
.
slistener
.
cleaning
();
this
.
learnedConstraintsDeletionStrategy
.
reduce
(
this
.
learnts
);
}
...
...
@@ -1820,7 +1820,7 @@ public class Solver<D extends DataStructureFactory>
&&
this
.
lastConflictMeansUnsat
)
{
int
before
=
this
.
trail
.
size
();
unitClauseProvider
.
provideUnitClauses
(
this
);
this
.
stats
.
importedUnits
+=
this
.
trail
.
size
()
-
before
;
this
.
stats
.
i
ncI
mportedUnits
(
this
.
trail
.
size
()
-
before
)
;
status
=
search
(
assumps
);
if
(
status
==
Lbool
.
UNDEFINED
)
{
this
.
restarter
.
onRestart
();
...
...
@@ -2024,7 +2024,7 @@ public class Solver<D extends DataStructureFactory>
this
.
stats
.
printStat
(
out
,
prefix
);
double
cputime
=
(
System
.
currentTimeMillis
()
-
this
.
timebegin
)
/
1000
;
out
.
println
(
prefix
+
"speed (assignments/second)\t: "
//$NON-NLS-1$
+
this
.
stats
.
p
ropagations
/
cputime
);
+
this
.
stats
.
getP
ropagations
()
/
cputime
);
this
.
order
.
printStat
(
out
,
prefix
);
printLearntClausesInfos
(
out
,
prefix
);
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/core/SolverStats.java
View file @
61fcb96a
...
...
@@ -44,39 +44,39 @@ import java.util.Map;
public
class
SolverStats
implements
Serializable
{
private
static
final
long
serialVersionUID
=
1L
;
p
ublic
int
starts
;
p
rivate
int
starts
;
p
ublic
long
decisions
;
p
rivate
long
decisions
;
p
ublic
long
propagations
;
p
rivate
long
propagations
;
p
ublic
long
inspects
;
p
rivate
long
inspects
;
p
ublic
long
conflicts
;
p
rivate
long
conflicts
;
p
ublic
long
learnedliterals
;
p
rivate
long
learnedliterals
;
p
ublic
long
learnedbinaryclauses
;
p
rivate
long
learnedbinaryclauses
;
p
ublic
long
learnedternaryclauses
;
p
rivate
long
learnedternaryclauses
;
p
ublic
long
learnedclauses
;
p
rivate
long
learnedclauses
;
p
ublic
long
ignoredclauses
;
p
rivate
long
ignoredclauses
;
p
ublic
long
rootSimplifications
;
p
rivate
long
rootSimplifications
;
p
ublic
long
reducedliterals
;
p
rivate
long
reducedliterals
;
p
ublic
long
changedreason
;
p
rivate
long
changedreason
;
p
ublic
int
reduceddb
;
p
rivate
int
reduceddb
;
p
ublic
int
shortcuts
;
p
rivate
int
shortcuts
;
p
ublic
long
updateLBD
;
p
rivate
long
updateLBD
;
p
ublic
int
importedUnits
;
p
rivate
int
importedUnits
;
public
void
reset
()
{
this
.
starts
=
0
;
...
...
@@ -99,7 +99,7 @@ public class SolverStats implements Serializable {
}
public
void
printStat
(
PrintWriter
out
,
String
prefix
)
{
out
.
println
(
prefix
+
"starts\t\t: "
+
this
.
s
tarts
);
out
.
println
(
prefix
+
"starts\t\t: "
+
this
.
getS
tarts
()
);
out
.
println
(
prefix
+
"conflicts\t\t: "
+
this
.
conflicts
);
out
.
println
(
prefix
+
"decisions\t\t: "
+
this
.
decisions
);
out
.
println
(
prefix
+
"propagations\t\t: "
+
this
.
propagations
);
...
...
@@ -112,8 +112,8 @@ public class SolverStats implements Serializable {
+
this
.
learnedternaryclauses
);
out
.
println
(
prefix
+
"learnt constraints\t: "
+
this
.
learnedclauses
);
out
.
println
(
prefix
+
"ignored constraints\t: "
+
this
.
ignoredclauses
);
out
.
println
(
prefix
+
"root simplifications\t: "
+
this
.
rootSimplifications
);
out
.
println
(
prefix
+
"root simplifications\t: "
+
this
.
rootSimplifications
);
out
.
println
(
prefix
+
"removed literals (reason simplification)\t: "
+
this
.
reducedliterals
);
out
.
println
(
prefix
+
"reason swapping (by a shorter reason)\t: "
...
...
@@ -121,8 +121,7 @@ public class SolverStats implements Serializable {
out
.
println
(
prefix
+
"Calls to reduceDB\t: "
+
this
.
reduceddb
);
out
.
println
(
prefix
+
"Number of update (reduction) of LBD\t: "
+
this
.
updateLBD
);
out
.
println
(
prefix
+
"Imported unit clauses\t: "
+
this
.
importedUnits
);
out
.
println
(
prefix
+
"Imported unit clauses\t: "
+
this
.
importedUnits
);
}
public
Map
<
String
,
Number
>
toMap
()
{
...
...
@@ -138,4 +137,140 @@ public class SolverStats implements Serializable {
}
return
map
;
}
public
int
getStarts
()
{
return
starts
;
}
public
void
incStarts
()
{
this
.
starts
++;
}
public
long
getDecisions
()
{
return
decisions
;
}
public
void
incDecisions
()
{
this
.
decisions
++;
}
public
long
getPropagations
()
{
return
propagations
;
}
public
void
incPropagations
()
{
this
.
propagations
++;
}
public
long
getInspects
()
{
return
inspects
;
}
public
void
incInspects
()
{
this
.
inspects
++;
}
public
long
getConflicts
()
{
return
conflicts
;
}
public
void
incConflicts
()
{
this
.
conflicts
++;
}
public
long
getLearnedliterals
()
{
return
learnedliterals
;
}
public
void
incLearnedliterals
()
{
this
.
learnedliterals
++;
}
public
long
getLearnedbinaryclauses
()
{
return
learnedbinaryclauses
;
}
public
void
incLearnedbinaryclauses
()
{
this
.
learnedbinaryclauses
++;
}
public
long
getLearnedternaryclauses
()
{
return
learnedternaryclauses
;
}
public
void
incLearnedternaryclauses
()
{
this
.
learnedternaryclauses
++;
}
public
long
getLearnedclauses
()
{
return
learnedclauses
;
}
public
void
incLearnedclauses
()
{
this
.
learnedclauses
++;
}
public
long
getIgnoredclauses
()
{
return
ignoredclauses
;
}
public
void
incIgnoredclauses
()
{
this
.
ignoredclauses
++;
}
public
long
getRootSimplifications
()
{
return
rootSimplifications
;
}
public
void
incRootSimplifications
()
{
this
.
rootSimplifications
++;
}
public
long
getReducedliterals
()
{
return
reducedliterals
;
}
public
void
incReducedliterals
(
int
increment
)
{
this
.
reducedliterals
+=
increment
;
}
public
long
getChangedreason
()
{
return
changedreason
;
}
public
void
incChangedreason
()
{
this
.
changedreason
++;
}
public
int
getReduceddb
()
{
return
reduceddb
;
}
public
void
incReduceddb
()
{
this
.
reduceddb
++;
}
public
int
getShortcuts
()
{
return
shortcuts
;
}
public
void
incShortcuts
()
{
this
.
shortcuts
++;
}
public
long
getUpdateLBD
()
{
return
updateLBD
;
}
public
void
incUpdateLBD
()
{
this
.
updateLBD
++;
}
public
int
getImportedUnits
()
{
return
importedUnits
;
}
public
void
incImportedUnits
(
int
increment
)
{
this
.
importedUnits
+=
increment
;
}
}
org.sat4j.core/src/main/java/org/sat4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java
View file @
61fcb96a
...
...
@@ -53,8 +53,8 @@ import org.sat4j.specs.Propagatable;
* @author leberre
*
*/
public
class
WatcherBasedPrimeImplicantStrategy
implements
PrimeImplicantStrategy
,
MandatoryLiteralListener
{
public
class
WatcherBasedPrimeImplicantStrategy
implements
PrimeImplicantStrategy
,
MandatoryLiteralListener
{
private
int
[]
prime
;
...
...
@@ -125,14 +125,14 @@ public class WatcherBasedPrimeImplicantStrategy implements
}
long
end
=
System
.
currentTimeMillis
();
if
(
solver
.
isVerbose
())
{
System
.
out
.
printf
(
"%s prime implicant computation statistics BRESIL (reverse = %b)%n"
,
solver
.
getLogPrefix
(),
this
.
comparator
!=
null
);
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 prime implicant computation statistics BRESIL (reverse = %b)%n"
,
solver
.
getLogPrefix
(),
this
.
comparator
!=
null
);
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
;
}
...
...
@@ -145,7 +145,7 @@ public class WatcherBasedPrimeImplicantStrategy implements
solver
.
voc
.
watches
(
p
).
moveTo
(
lwatched
);
final
int
size
=
lwatched
.
size
();
for
(
int
i
=
0
;
i
<
size
;
i
++)
{
solver
.
stats
.
inspects
++
;
solver
.
stats
.
in
cIn
spects
()
;
lwatched
.
get
(
i
).
propagatePI
(
this
,
p
);
}
return
null
;
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/learning/LimitedLearning.java
View file @
61fcb96a
...
...
@@ -75,7 +75,7 @@ public abstract class LimitedLearning<D extends DataStructureFactory>
this
.
all
.
learns
(
constr
);
}
else
{
this
.
none
.
learns
(
constr
);
this
.
stats
.
ignoredclauses
++
;
this
.
stats
.
i
ncI
gnoredclauses
()
;
}
}
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/EMARestarts.java
View file @
61fcb96a
...
...
@@ -76,11 +76,11 @@ public class EMARestarts implements RestartStrategy {
}
public
boolean
shouldRestart
()
{
return
this
.
stats
.
c
onflicts
>
limit
&&
fast
/
125
>
slow
/
100
;
return
this
.
stats
.
getC
onflicts
()
>
limit
&&
fast
/
125
>
slow
/
100
;
}
public
void
onRestart
()
{
limit
=
this
.
stats
.
c
onflicts
+
50
;
limit
=
this
.
stats
.
getC
onflicts
()
+
50
;
}
public
void
onBackjumpToRootLevel
()
{
...
...
org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/Glucose21Restarts.java
View file @
61fcb96a
...
...
@@ -77,7 +77,7 @@ public class Glucose21Restarts implements RestartStrategy {
// was
// ... trailLevel > 1.4 * bufferTrail.average()
// uses now only integers to avoid rounding issues
if
(
stats
.
c
onflicts
>
10000
&&
bufferTrail
.
isFull
()
if
(
stats
.
getC
onflicts
()
>
10000
&&
bufferTrail
.
isFull
()
&&
trailLevel
*
5L
>
7L
*
bufferTrail
.
average
())
{
bufferLBD
.
clear
();
}
...
...
@@ -97,7 +97,7 @@ public class Glucose21Restarts implements RestartStrategy {
// ... && bufferLBD.average() * 0.8 > sumOfAllLBD / stats.conflicts
// uses now only integers to avoid rounding issues
return
bufferLBD
.
isFull
()
&&
bufferLBD
.
average
()
*
stats
.
c
onflicts
*
4L
>
sumOfAllLBD
*
5L
;
&&
bufferLBD
.
average
()
*
stats
.
getC
onflicts
()
*
4L
>
sumOfAllLBD
*
5L
;
}
public
void
onRestart
()
{
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment