Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Romain WALLON
sat4j
Commits
3caf0d88
Commit
3caf0d88
authored
Nov 23, 2021
by
tfalque.ext
Browse files
✨
first implementation of GaussElimination
parent
b8128764
Pipeline
#17628
failed with stages
in 29 minutes and 41 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/GaussPBPreprocessing.java
View file @
3caf0d88
...
...
@@ -33,9 +33,20 @@ public class GaussPBPreprocessing extends AbstractPBPreprocessing {
groups
.
add
(
group
);
}
}
List
<
PBPreprocessingConstraint
>
finalList
=
new
ArrayList
<>();
for
(
PBPreprocessingConstraintGroup
group
:
groups
)
{
finalList
.
addAll
(
applyGauss
(
group
.
getLists
()));
}
return
finalList
;
return
null
;
}
private
List
<
PBPreprocessingConstraint
>
applyGauss
(
List
<
PBPreprocessingConstraint
>
constraints
)
{
SystemPreprocessing
system
=
new
SystemPreprocessing
(
constraints
);
return
system
.
compute
();
}
}
org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/PBPreprocessingConstraint.java
View file @
3caf0d88
...
...
@@ -6,6 +6,7 @@ package org.sat4j.pb.preprocessing;
import
java.math.BigInteger
;
import
org.sat4j.core.Vec
;
import
org.sat4j.core.VecInt
;
import
org.sat4j.pb.IPBSolver
;
import
org.sat4j.specs.ContradictionException
;
import
org.sat4j.specs.IVec
;
...
...
@@ -23,6 +24,42 @@ public class PBPreprocessingConstraint implements ITransformConstraint {
private
final
PBPreprocessingConstraintType
type
;
/**
* @return the literals
*/
public
IVecInt
getLiterals
()
{
return
literals
;
}
public
BigInteger
getCoeff
(
int
lit
)
{
int
index
=
literals
.
indexOf
(
lit
);
if
(
index
==
-
1
)
{
return
BigInteger
.
ZERO
;
}
return
coeffs
.
get
(
index
);
}
/**
* @return the coeffs
*/
public
IVec
<
BigInteger
>
getCoeffs
()
{
return
coeffs
;
}
/**
* @return the weight
*/
public
BigInteger
getWeight
()
{
return
weight
;
}
/**
* @return the type
*/
public
PBPreprocessingConstraintType
getType
()
{
return
type
;
}
/**
* @param literals
* @param coeffs
...
...
@@ -98,4 +135,32 @@ public class PBPreprocessingConstraint implements ITransformConstraint {
}
public
PBPreprocessingConstraint
mult
(
BigInteger
coeff
)
{
IVec
<
BigInteger
>
localCoeffs
=
new
Vec
<>(
this
.
coeffs
.
size
());
for
(
int
i
=
0
;
i
<
this
.
coeffs
.
size
();
i
++)
{
localCoeffs
.
push
(
this
.
coeffs
.
get
(
i
).
multiply
(
coeff
));
}
return
PBPreprocessingConstraint
.
newExactly
(
this
.
literals
,
localCoeffs
,
this
.
weight
.
multiply
(
coeff
));
}
public
PBPreprocessingConstraint
sub
(
PBPreprocessingConstraint
other
)
{
IVecInt
finalLits
=
new
VecInt
();
IVec
<
BigInteger
>
localCoeffs
=
new
Vec
<>();
for
(
IteratorInt
it
=
this
.
literals
.
iterator
();
it
.
hasNext
();)
{
int
lit
=
it
.
next
();
BigInteger
localCoeff
=
this
.
getCoeff
(
lit
)
.
subtract
(
other
.
getCoeff
(
lit
));
if
(
localCoeff
.
equals
(
BigInteger
.
ZERO
))
{
continue
;
}
finalLits
.
push
(
lit
);
localCoeffs
.
push
(
localCoeff
);
}
return
PBPreprocessingConstraint
.
newExactly
(
finalLits
,
localCoeffs
,
weight
.
subtract
(
other
.
getWeight
()));
}
}
org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/PBPreprocessingConstraintGroup.java
View file @
3caf0d88
...
...
@@ -21,4 +21,11 @@ public class PBPreprocessingConstraintGroup {
lists
.
add
(
constraint
);
}
/**
* @return the lists
*/
public
List
<
PBPreprocessingConstraint
>
getLists
()
{
return
lists
;
}
}
org.sat4j.pb/src/main/java/org/sat4j/pb/preprocessing/SystemPreprocessing.java
0 → 100644
View file @
3caf0d88
/**
*
*/
package
org.sat4j.pb.preprocessing
;
import
java.math.BigInteger
;
import
java.util.Collections
;
import
java.util.HashSet
;
import
java.util.List
;
import
java.util.Set
;
import
org.sat4j.specs.IteratorInt
;
/**
* @author Thibault Falque
*
*/
public
class
SystemPreprocessing
{
private
final
List
<
PBPreprocessingConstraint
>
equations
;
private
final
Set
<
Integer
>
variables
=
new
HashSet
<>();
/**
*
* @param constraints
*/
public
SystemPreprocessing
(
List
<
PBPreprocessingConstraint
>
constraints
)
{
this
.
equations
=
constraints
;
for
(
PBPreprocessingConstraint
constraint
:
this
.
equations
)
{
for
(
IteratorInt
it
=
constraint
.
getLiterals
().
iterator
();
it
.
hasNext
();)
{
this
.
variables
.
add
(
it
.
next
());
}
}
}
/**
*
* @return
*/
public
List
<
PBPreprocessingConstraint
>
compute
()
{
int
currentLine
=
0
;
for
(
Integer
i
:
variables
)
{
int
bestEquation
=
computeBestEquation
(
currentLine
,
i
);
Collections
.
swap
(
equations
,
currentLine
,
bestEquation
);
applyGaussianElimination
(
currentLine
,
i
);
currentLine
++;
}
return
null
;
}
/**
*
* @param currentLine
* @param lit
* @return
*/
private
int
computeBestEquation
(
int
currentLine
,
int
lit
)
{
int
bestEquation
=
currentLine
;
BigInteger
min
=
equations
.
get
(
currentLine
).
getCoeff
(
lit
);
for
(
int
i
=
currentLine
+
1
;
i
<
equations
.
size
();
i
++)
{
BigInteger
currentCoeff
=
equations
.
get
(
i
).
getCoeff
(
lit
);
if
(
currentCoeff
.
equals
(
BigInteger
.
ZERO
))
continue
;
if
((
min
.
equals
(
BigInteger
.
ZERO
))
||
(
min
.
compareTo
(
currentCoeff
)
==
1
))
{
bestEquation
=
i
;
min
=
currentCoeff
;
}
}
return
bestEquation
;
}
/**
*
* @param currentLine
* @param v
*/
void
applyGaussianElimination
(
int
currentLine
,
int
v
)
{
PBPreprocessingConstraint
p
=
equations
.
get
(
currentLine
);
BigInteger
c
=
p
.
getCoeff
(
v
);
for
(
int
i
=
currentLine
+
1
;
i
<
equations
.
size
();
i
++)
{
PBPreprocessingConstraint
e
=
equations
.
get
(
i
);
if
(
e
.
getCoeff
(
v
).
equals
(
BigInteger
.
ZERO
))
continue
;
equations
.
set
(
i
,
p
.
mult
(
e
.
getCoeff
(
v
)).
sub
(
e
.
mult
(
c
)));
}
}
}
Write
Preview
Supports
Markdown
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