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
Kučera Petr RNDr. Ph.D.
PCCompile
Commits
2447decf
Commit
2447decf
authored
Aug 02, 2021
by
Kučera Petr RNDr. Ph.D.
Browse files
Partial refactoring of dpelim options
parent
8a8a2148
Changes
12
Expand all
Hide whitespace changes
Inline
Side-by-side
bin/cnfprime.cpp
View file @
2447decf
...
...
@@ -37,6 +37,7 @@ parse_arguments(int argc, char *argv[])
{
config_t
conf
;
SUBool
::
PrgOptions
opts
;
opts
.
SetHelpDesc
(
prg_help
);
opts
.
InputOutput
(
&
conf
.
input_file
,
&
conf
.
output_file
);
po
::
options_description
desc
(
"Configuration options"
);
desc
.
add_options
()(
"unitprop,u"
,
po
::
bool_switch
(
&
conf
.
unitprop
),
...
...
bin/dpelim.cpp
View file @
2447decf
This diff is collapsed.
Click to expand it.
lib/dpelim.cpp
View file @
2447decf
...
...
@@ -13,10 +13,35 @@
#include "resolve.h"
#include "util.h"
const
SUBool
::
EnumAnnotation
<
SUBool
::
DPEliminator
::
IGNORE_POLICY
>
SUBool
::
DPEliminator
::
kIgnorePolicyAnnotation
(
"IGNORE_POLICY"
,
{{
IGNORE_POLICY
::
NONE
,
"none"
,
"do not discard any resolvents"
},
{
IGNORE_POLICY
::
IMPLICATES
,
"implicates"
,
"discard the clauses which are implicates of others"
},
{
IGNORE_POLICY
::
ABSORBED
,
"absorbed"
,
"discard the absorbed clauses (not empowering)"
}});
const
SUBool
::
EnumAnnotation
<
SUBool
::
DPEliminator
::
INPROCESSING
>
SUBool
::
DPEliminator
::
kInprocessingAnnotation
(
"INPROCESSING"
,
{{
INPROCESSING
::
NONE
,
"none"
,
"no inprocessing"
},
{
INPROCESSING
::
PRIME
,
"prime"
,
"find prime subimplicate"
}});
const
SUBool
::
EnumAnnotation
<
SUBool
::
DPEliminator
::
INCREASE_POLICY
>
SUBool
::
DPEliminator
::
kIncreasePolicyAnnotation
(
"INCREASE_POLICY"
,
{{
INCREASE_POLICY
::
ESTIMATE
,
"estimate"
,
"stop when the estimate of increase gets over the bound"
},
{
INCREASE_POLICY
::
AFTER_BOUND
,
"after_bound"
,
"stop when the size got over the bound"
},
{
INCREASE_POLICY
::
NEW_CLAUSES
,
"new_clauses"
,
"stop when the current number of new clauses gets over the "
"bound"
},
{
INCREASE_POLICY
::
NEW_CLAUSES_TOTAL
,
"new_clauses_total"
,
"stop when the total number of new clauses gets over the "
"bound"
}});
SUBool
::
DPEliminator
::
DPEliminator
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
)
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
)
:
mMaxFixedVariable
(
max_fixed_variable
),
mMaxVariable
(
cnf
.
MaxVariable
()),
mClauseInfo
(),
mInvalidClauseInfo
(),
mVarInfo
(
mMaxVariable
>
mMaxFixedVariable
...
...
@@ -150,8 +175,8 @@ SUBool::DPEliminator::CnfWithMask() &&
}
SUBool
::
CNF
SUBool
::
DPEliminator
::
EliminateAuxVariables
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
SUBool
::
DPEliminator
::
EliminateAuxVariables
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
,
size_t
max_size_increase
,
bool
at_least_one
)
{
...
...
@@ -161,23 +186,22 @@ SUBool::DPEliminator::EliminateAuxVariables(
{
return
cnf
;
}
DPEliminator
elim
(
cnf
,
max_fixed_variable
,
ignore_policy
,
inprocessing
,
increase_policy
);
DPEliminator
elim
(
cnf
,
max_fixed_variable
,
ignore_policy
,
inprocessing
,
increase_policy
);
elim
.
EliminateAuxVariables
(
max_size_increase
,
at_least_one
);
return
std
::
move
(
elim
).
Cnf
();
}
SUBool
::
CNF
SUBool
::
DPEliminator
::
EliminateAuxVariablesWithFactor
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
SUBool
::
DPEliminator
::
EliminateAuxVariablesWithFactor
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
,
long
double
max_size_increase_factor
,
bool
at_least_one
)
{
size_t
max_size_increase
=
static_cast
<
size_t
>
(
static_cast
<
long
double
>
(
cnf
.
Size
())
*
max_size_increase_factor
);
return
EliminateAuxVariables
(
cnf
,
max_fixed_variable
,
ignore_policy
,
inprocessing
,
increase_policy
,
max_size_increase
,
at_least_one
);
inprocessing
,
increase_policy
,
max_size_increase
,
at_least_one
);
}
void
...
...
@@ -201,14 +225,14 @@ SUBool::DPEliminator::CheckIncrease(size_t initial_size, size_t bound) const
case
INCREASE_POLICY
::
NEW_CLAUSES_TOTAL
:
return
mTotalNewClauses
<=
bound
;
default:
throw
BadParameterException
(
"DPEliminator::CheckIncrease"
,
"Unknown increase policy"
);
throw
BadParameterException
(
"DPEliminator::CheckIncrease"
,
"Unknown increase policy"
);
}
}
void
SUBool
::
DPEliminator
::
EliminateAuxVariables
(
size_t
max_size_increase
,
bool
at_least_one
)
SUBool
::
DPEliminator
::
EliminateAuxVariables
(
size_t
max_size_increase
,
bool
at_least_one
)
{
if
(
mMaxVariable
<=
mMaxFixedVariable
)
{
...
...
@@ -240,8 +264,8 @@ SUBool::DPEliminator::EliminateVarNotInHeap(unsigned var)
{
if
(
!
IsFree
(
var
))
{
throw
BadParameterException
(
"DPEliminator::EliminateVarNotInHeap"
,
"Variable is fixed"
);
throw
BadParameterException
(
"DPEliminator::EliminateVarNotInHeap"
,
"Variable is fixed"
);
}
auto
&
vi
=
GetVarInfo
(
var
);
auto
invalid
=
InvalidateClauses
(
vi
.
mPosClauses
);
...
...
@@ -343,7 +367,7 @@ SUBool::DPEliminator::AddClauses(std::vector<Clause> resolvents)
{
continue
;
}
if
(
mInprocessing
==
INPROCESSING
::
PRIME
_SUBIMPLICATE
)
if
(
mInprocessing
==
INPROCESSING
::
PRIME
)
{
clause
=
*
prime_subimplicate
(
mCnf
,
clause
);
}
...
...
@@ -405,8 +429,8 @@ SUBool::DPEliminator::VarInfo::RemoveInvalid()
}
bool
SUBool
::
DPEliminator
::
IgnoreClause
(
const
CNF
&
cnf
,
const
Clause
&
clause
,
OneProve
&
op
)
const
SUBool
::
DPEliminator
::
IgnoreClause
(
const
CNF
&
cnf
,
const
Clause
&
clause
,
OneProve
&
op
)
const
{
switch
(
mIgnorePolicy
)
{
...
...
@@ -417,7 +441,7 @@ SUBool::DPEliminator::IgnoreClause(const CNF &cnf, const Clause &clause,
case
IGNORE_POLICY
::
ABSORBED
:
return
!
op
.
IsEmpowering
(
clause
);
default:
throw
BadParameterException
(
"DPEliminator::IgnoreClause"
,
"Unknown ignore policy"
);
throw
BadParameterException
(
"DPEliminator::IgnoreClause"
,
"Unknown ignore policy"
);
}
}
lib/dpelim.h
View file @
2447decf
...
...
@@ -16,10 +16,12 @@
#include <vector>
#include "empower.h"
#include "enum.h"
#include "normalform.h"
namespace
SUBool
{
class
DPEliminator
{
...
...
@@ -37,8 +39,8 @@ namespace SUBool
enum
class
INPROCESSING
{
NONE
,
PRIME
_SUBIMPLICATE
,
Last
=
PRIME
_SUBIMPLICATE
PRIME
,
Last
=
PRIME
};
enum
class
INCREASE_POLICY
...
...
@@ -54,10 +56,14 @@ namespace SUBool
Last
=
NEW_CLAUSES_TOTAL
};
static
const
EnumAnnotation
<
IGNORE_POLICY
>
kIgnorePolicyAnnotation
;
static
const
EnumAnnotation
<
INPROCESSING
>
kInprocessingAnnotation
;
static
const
EnumAnnotation
<
INCREASE_POLICY
>
kIncreasePolicyAnnotation
;
private:
using
VarHeapElement
=
std
::
pair
<
size_t
,
unsigned
>
;
using
VarHeap
=
boost
::
heap
::
fibonacci_heap
<
VarHeapElement
,
boost
::
heap
::
compare
<
std
::
greater
<
VarHeapElement
>>>
;
using
VarHeap
=
boost
::
heap
::
fibonacci_heap
<
VarHeapElement
,
boost
::
heap
::
compare
<
std
::
greater
<
VarHeapElement
>>>
;
class
ClauseInfo
{
...
...
@@ -120,8 +126,8 @@ namespace SUBool
void
InitVarHeap
();
void
EliminateVarNotInHeap
(
unsigned
var
);
std
::
list
<
ClauseInfo
>
InvalidateClauses
(
const
std
::
list
<
ClauseInfo
::
tPointer
>
&
clauses
);
std
::
list
<
ClauseInfo
>
InvalidateClauses
(
const
std
::
list
<
ClauseInfo
::
tPointer
>
&
clauses
);
void
AddClauses
(
std
::
vector
<
Clause
>
resolvents
);
void
UpdateVarInfo
(
std
::
unordered_set
<
unsigned
>
variables
);
...
...
@@ -130,8 +136,8 @@ namespace SUBool
INPROCESSING
mInprocessing
;
INCREASE_POLICY
mIncreasePolicy
;
bool
IgnoreClause
(
const
CNF
&
cnf
,
const
Clause
&
clause
,
OneProve
&
op
)
const
;
bool
IgnoreClause
(
const
CNF
&
cnf
,
const
Clause
&
clause
,
OneProve
&
op
)
const
;
bool
CheckIncrease
(
size_t
initial_size
,
size_t
bound
)
const
;
CNF
mCnf
;
...
...
@@ -140,12 +146,12 @@ namespace SUBool
public:
DPEliminator
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
);
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
);
void
EliminateVariable
(
unsigned
var
);
// only non fixed variable allowed
void
EliminateAuxVariables
(
size_t
max_size_increase
,
bool
at_least_one
=
false
);
void
EliminateAuxVariables
(
size_t
max_size_increase
,
bool
at_least_one
=
false
);
size_t
Size
()
const
...
...
@@ -159,17 +165,15 @@ namespace SUBool
std
::
pair
<
CNF
,
std
::
vector
<
bool
>>
CnfWithMask
()
const
&
;
std
::
pair
<
CNF
,
std
::
vector
<
bool
>>
CnfWithMask
()
&&
;
static
CNF
EliminateAuxVariables
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
,
static
CNF
EliminateAuxVariables
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
,
size_t
max_size_increase
=
std
::
numeric_limits
<
size_t
>::
max
()
/
2
,
bool
at_least_one
=
false
);
static
CNF
EliminateAuxVariablesWithFactor
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
,
long
double
max_size_increase_factor
,
bool
at_least_one
=
false
);
static
CNF
EliminateAuxVariablesWithFactor
(
const
CNF
&
cnf
,
unsigned
max_fixed_variable
,
IGNORE_POLICY
ignore_policy
,
INPROCESSING
inprocessing
,
INCREASE_POLICY
increase_policy
,
long
double
max_size_increase_factor
,
bool
at_least_one
=
false
);
};
}
// namespace SUBool
...
...
lib/dpelim_opt.cpp
0 → 100644
View file @
2447decf
/*
* Project SUBool
* Petr Kucera, 2021
*/
/**@file dpelim_opt.cpp
* Program options related to DP elimination of variables in a CNF.
*/
#include "dpelim_opt.h"
const
SUBool
::
EnumAnnotation
<
SUBool
::
ELIMINATE_POLICY
>
SUBool
::
kEliminatePolicyAnnotation
(
"ELIMINATE"
,
{
//
{
ELIMINATE_POLICY
::
ALL
,
"all"
,
"Eliminate all auxiliary variables."
},
{
ELIMINATE_POLICY
::
MAX_INCREASE
,
"max_increase"
,
"Elimination limited with the absolute increase of "
"the size of the CNF."
},
{
ELIMINATE_POLICY
::
FACTOR
,
"factor"
,
"Elimination limited with the factor by which the "
"size of the CNF can increase."
}});
void
SUBool
::
DPElimMinimizeOptions
::
Init
()
{
mOptionsDesc
.
add_options
()
//
(
"minimize,m"
,
po
::
bool_switch
(
&
mFinalMinimize
),
"Perform minimization at the end (not needed with -M option)."
)
//
(
"elim-minimize,M"
,
po
::
bool_switch
(
&
mElimMinimize
),
"Use minimization during elimination."
)
//
(
"elim-minimize-step"
,
po
::
value
<
unsigned
>
(
&
mSizeStep
)
->
default_value
(
kDefaultSizeStep
),
"Size increase step between two minimizations."
)
//
(
"elim-minimize-factor"
,
po
::
value
<
double
>
(
&
mSizeFactor
)
->
default_value
(
kDefaultSizeFactor
,
kDefaultSizeFactorString
),
"Factor of the cnf size to be added to the minimize step."
);
}
bool
SUBool
::
DPElimMinimizeOptions
::
GetValues
()
{
return
true
;
}
lib/dpelim_opt.h
0 → 100644
View file @
2447decf
/*
* Project SUBool
* Petr Kucera, 2021
*/
/**@file dpelim_opt.h
* Program options related to DP elimination of variables in a CNF.
*/
#ifndef __DPELIM_OPT_H
#define __DPELIM_OPT_H
#include <boost/program_options.hpp>
#include "dpelim.h"
#include "encoding.h"
#include "enum_opt.h"
namespace
po
=
boost
::
program_options
;
namespace
SUBool
{
enum
class
ELIMINATE_POLICY
{
ALL
,
MAX_INCREASE
,
FACTOR
,
Last
=
FACTOR
};
extern
const
EnumAnnotation
<
ELIMINATE_POLICY
>
kEliminatePolicyAnnotation
;
struct
elim_config_t
{
unsigned
max_input_var
{
0
};
// Clause manipulation
CNFEncoding
::
BLOCK_PRIME
block_prime
{
CNFEncoding
::
BLOCK_PRIME
::
NONE
};
DPEliminator
::
INPROCESSING
inprocessing
{
DPEliminator
::
INPROCESSING
::
NONE
};
DPEliminator
::
IGNORE_POLICY
ignore_policy
{
DPEliminator
::
IGNORE_POLICY
::
ABSORBED
};
// Elimination policy
ELIMINATE_POLICY
eliminate
{
ELIMINATE_POLICY
::
ALL
};
DPEliminator
::
INCREASE_POLICY
increase_policy
{
DPEliminator
::
INCREASE_POLICY
::
AFTER_BOUND
};
unsigned
max_increase
{
0
};
long
double
factor
{
1.0
};
// bool use_minimize{false};
// bool final_minimize{false};
// unsigned minimize_size_step{5000};
// double minimize_size_factor{0.6};
};
class
DPElimMinimizeOptions
{
public:
static
constexpr
unsigned
kDefaultSizeStep
=
5000u
;
static
constexpr
double
kDefaultSizeFactor
=
0.6
;
inline
static
const
std
::
string
kDefaultSizeFactorString
=
"0.6"
;
private:
po
::
options_description
mOptionsDesc
;
bool
mElimMinimize
{
false
};
bool
mFinalMinimize
{
false
};
unsigned
mSizeStep
{
kDefaultSizeStep
};
double
mSizeFactor
{
kDefaultSizeFactor
};
void
Init
();
public:
DPElimMinimizeOptions
();
bool
GetValues
();
const
po
::
options_description
&
Desc
()
const
;
bool
ElimMinimize
()
const
;
bool
FinalMinimize
()
const
;
unsigned
SizeStep
()
const
;
double
SizeFactor
()
const
;
};
}
// namespace SUBool
inline
SUBool
::
DPElimMinimizeOptions
::
DPElimMinimizeOptions
()
:
mOptionsDesc
(
"Minimize options"
)
{
Init
();
}
inline
const
po
::
options_description
&
SUBool
::
DPElimMinimizeOptions
::
Desc
()
const
{
return
mOptionsDesc
;
}
inline
bool
SUBool
::
DPElimMinimizeOptions
::
ElimMinimize
()
const
{
return
mElimMinimize
;
}
inline
bool
SUBool
::
DPElimMinimizeOptions
::
FinalMinimize
()
const
{
return
mFinalMinimize
;
}
inline
unsigned
SUBool
::
DPElimMinimizeOptions
::
SizeStep
()
const
{
return
mSizeStep
;
}
inline
double
SUBool
::
DPElimMinimizeOptions
::
SizeFactor
()
const
{
return
mSizeFactor
;
}
#endif
lib/encoding.cpp
View file @
2447decf
...
...
@@ -20,6 +20,12 @@ const std::vector<std::string> SUBool::CNFEncoding::kKindNames = {
const
std
::
regex
SUBool
::
CNFEncoding
::
kHeaderRegex
(
"^[[:space:]]*c[[:space:]]+![[:space:]]*encoding[[:space:]]"
"+(sat|i-urc|i-pc|urc|pc)[[:space:]]+([[:digit:]]+)[[:space:]]*$"
);
const
SUBool
::
EnumAnnotation
<
SUBool
::
CNFEncoding
::
BLOCK_PRIME
>
SUBool
::
CNFEncoding
::
kBlockPrimeAnnotation
(
"BLOCK_PRIME"
,
{{
BLOCK_PRIME
::
NONE
,
"none"
,
"CNF is not made prime"
},
{
BLOCK_PRIME
::
UP_PRIME
,
"up_prime"
,
"use unit propagation for primality"
},
{
BLOCK_PRIME
::
PRIME
,
"prime"
,
"use SAT for primality"
}});
SUBool
::
CNFEncoding
::
KIND
SUBool
::
CNFEncoding
::
KindOfName
(
const
std
::
string
&
kind_name
)
...
...
@@ -78,9 +84,8 @@ SUBool::CNFEncoding::EliminateAuxVariablesWithMaxSize(size_t max_size)
logs
.
TLog
(
1
)
<<
"Starting elimination (p cnf "
<<
mCnf
.
MaxVariable
()
<<
" "
<<
mCnf
.
Size
()
<<
"), max input variable: "
<<
mMaxInputVariable
<<
std
::
endl
;
mCnf
=
DPEliminator
::
EliminateAuxVariables
(
mCnf
,
mMaxInputVariable
,
mElimIgnorePolicy
,
mElimInprocessing
,
mElimIncreasePolicy
,
mCnf
=
DPEliminator
::
EliminateAuxVariables
(
mCnf
,
mMaxInputVariable
,
mElimIgnorePolicy
,
mElimInprocessing
,
mElimIncreasePolicy
,
(
max_size
==
kEliminateAll
?
kEliminateAll
:
max_size
-
mCnf
.
Size
()));
mCnf
.
RemoveSubsumptions
();
CNFCompressor
compressor
(
mCnf
,
mMaxInputVariable
);
...
...
@@ -96,8 +101,7 @@ SUBool::CNFEncoding::CallEliminate(size_t size_inc, bool at_least_one)
{
CNFCompressor
compressor
(
mCnf
,
mMaxInputVariable
);
DPEliminator
dpelim
(
compressor
.
CompressCNF
(
mCnf
),
mMaxInputVariable
,
mElimIgnorePolicy
,
mElimInprocessing
,
mElimIncreasePolicy
);
mElimIgnorePolicy
,
mElimInprocessing
,
mElimIncreasePolicy
);
dpelim
.
EliminateAuxVariables
(
size_inc
,
at_least_one
);
auto
res
=
std
::
move
(
dpelim
).
CnfWithMask
();
res
.
first
=
compressor
.
UncompressCNF
(
std
::
move
(
res
.
first
));
...
...
@@ -105,8 +109,8 @@ SUBool::CNFEncoding::CallEliminate(size_t size_inc, bool at_least_one)
}
size_t
SUBool
::
CNFEncoding
::
SizeIncrease
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
)
const
SUBool
::
CNFEncoding
::
SizeIncrease
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
)
const
{
size_t
max_size_inc
=
(
max_size
==
kEliminateAll
?
kEliminateAll
:
max_size
-
mCnf
.
Size
());
...
...
@@ -120,9 +124,8 @@ SUBool::CNFEncoding::SizeIncrease(size_t max_size, size_t min_steps,
}
void
SUBool
::
CNFEncoding
::
EliminateAuxVariablesWithMaxSizeMinimize
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
)
SUBool
::
CNFEncoding
::
EliminateAuxVariablesWithMaxSizeMinimize
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
)
{
if
(
max_size
<
mCnf
.
Size
())
{
...
...
@@ -160,11 +163,11 @@ SUBool::CNFEncoding::EliminateAuxVariablesWithMaxSizeMinimize(size_t max_size,
{
case
BLOCK_PRIME
::
UP_PRIME
:
mCnf
=
BlockPrimeUP
(
res
.
first
,
curr_max_var
,
[
&
res
](
auto
i
)
{
return
!
res
.
second
[
i
];
});
[
&
res
](
auto
i
)
{
return
!
res
.
second
[
i
];
});
break
;
case
BLOCK_PRIME
::
PRIME
:
mCnf
=
BlockPrime
(
res
.
first
,
curr_max_var
,
ref_solver
.
Solver
(),
[
&
res
](
auto
i
)
{
return
!
res
.
second
[
i
];
});
[
&
res
](
auto
i
)
{
return
!
res
.
second
[
i
];
});
break
;
default:
mCnf
=
std
::
move
(
res
.
first
);
...
...
@@ -220,9 +223,9 @@ SUBool::CNFEncoding::EliminateAuxVariablesWithMaxIncMinimize(
void
SUBool
::
CNFEncoding
::
EliminateAuxVariablesWithMaxInc
(
size_t
max_size_increase
)
{
EliminateAuxVariablesWithMaxSize
(
(
max_size_increase
==
kEliminateAll
?
kEliminateAll
:
mCnf
.
Size
()
+
max_size_increase
));
EliminateAuxVariablesWithMaxSize
(
(
max_size_increase
==
kEliminateAll
?
kEliminateAll
:
mCnf
.
Size
()
+
max_size_increase
));
}
void
...
...
@@ -262,8 +265,8 @@ SUBool::SATEncoding::Consistent(const Assignment &alpha) const
{
if
(
alpha
.
Size
()
!=
mMaxInputVariable
)
{
throw
BadParameterException
(
"CNFEncoding::Consistent"
,
"alpha.Size() != mMaxInputVariable"
);
throw
BadParameterException
(
"CNFEncoding::Consistent"
,
"alpha.Size() != mMaxInputVariable"
);
}
if
(
mMaxInputVariable
==
mCnf
.
MaxVariable
())
{
...
...
@@ -283,8 +286,8 @@ SUBool::SATEncoding::Propagate(const PartialAssignment &alpha) const
{
if
(
alpha
.
Size
()
!=
mMaxInputVariable
)
{
throw
BadParameterException
(
"CNFEncoding::Propagate"
,
"alpha.Size() != mMaxInputVariable"
);
throw
BadParameterException
(
"CNFEncoding::Propagate"
,
"alpha.Size() != mMaxInputVariable"
);
}
auto
beta
=
mPropagator
.
PropagateMaxVar
(
alpha
,
mMaxInputVariable
);
if
(
beta
)
...
...
@@ -326,8 +329,8 @@ SUBool::URCEncoding::Propagate(const PartialAssignment &alpha) const
beta
=
mUP
.
Propagate
(
*
gamma
);
if
(
!
beta
)
{
throw
InvariantFailedException
(
"URCEncoding::Propagate"
,
"Unexpected conflict"
);
throw
InvariantFailedException
(
"URCEncoding::Propagate"
,
"Unexpected conflict"
);
}
gamma
=
std
::
move
(
beta
);
continue
;
...
...
@@ -419,8 +422,8 @@ SUBool::CNFEncoding::ReadHeader(std::istream &input)
std
::
smatch
sm
;
if
(
std
::
regex_match
(
line
,
sm
,
kHeaderRegex
))
{
return
Header
{
KindOfName
(
sm
[
1
]),
static_cast
<
unsigned
int
>
(
std
::
atoi
(
sm
[
2
].
str
().
c_str
()))};
return
Header
{
KindOfName
(
sm
[
1
]),
static_cast
<
unsigned
int
>
(
std
::
atoi
(
sm
[
2
].
str
().
c_str
()))};
}
}
return
Header
{
KIND
::
UNKNOWN
,
0
};
...
...
lib/encoding.h
View file @
2447decf
...
...
@@ -17,6 +17,7 @@
#include "cpuutil.h"
#include "dpelim.h"
#include "empower.h"
#include "enum.h"
#include "logstream.h"
#include "normalform.h"
#include "propagate.h"
...
...
@@ -63,14 +64,16 @@ namespace SUBool
Last
=
PRIME
};
static
const
EnumAnnotation
<
BLOCK_PRIME
>
kBlockPrimeAnnotation
;
private:
DPEliminator
::
IGNORE_POLICY
mElimIgnorePolicy
;
DPEliminator
::
INPROCESSING
mElimInprocessing
;
DPEliminator
::
INCREASE_POLICY
mElimIncreasePolicy
;
BLOCK_PRIME
mBlockPrime
;
size_t
SizeIncrease
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
)
const
;
size_t
SizeIncrease
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
)
const
;
protected:
CNF
mCnf
;
...
...
@@ -84,19 +87,19 @@ namespace SUBool
template
<
class
IgnorePred
>
CNF
BlockPrime
(
const
CNF
&
cnf
,
unsigned
cnf_max_var
,
const
SolverInterface
&
ref_solver
,
IgnorePred
pred
);
std
::
pair
<
CNF
,
std
::
vector
<
bool
>>
CallEliminate
(
size_t
size_inc
,
bool
at_least_one
);
const
SolverInterface
&
ref_solver
,
IgnorePred
pred
);
std
::
pair
<
CNF
,
std
::
vector
<
bool
>>
CallEliminate
(
size_t
size_inc
,
bool
at_least_one
);
public:
virtual
~
CNFEncoding
();
// The input variables have to be 1 to max_input_var,
// all remaining variables are auxiliary.
CNFEncoding
(
CNF
cnf
,
unsigned
max_input_var
,
DPEliminator
::
IGNORE_POLICY
elim_ignore_policy
,
DPEliminator
::
INPROCESSING
elim_inprocessing
,
DPEliminator
::
INCREASE_POLICY
elim_increase_policy
,
BLOCK_PRIME
block_prime
)
DPEliminator
::
IGNORE_POLICY
elim_ignore_policy
,
DPEliminator
::
INPROCESSING
elim_inprocessing
,
DPEliminator
::
INCREASE_POLICY
elim_increase_policy
,
BLOCK_PRIME
block_prime
)
:
mElimIgnorePolicy
(
elim_ignore_policy
),
mElimInprocessing
(
elim_inprocessing
),
mElimIncreasePolicy
(
elim_increase_policy
),
mBlockPrime
(
block_prime
),
...
...
@@ -114,14 +117,14 @@ namespace SUBool
// alpha on input variables
virtual
bool
Consistent
(
const
PartialAssignment
&
alpha
)
const
=
0
;
// Returns none if not consistent
virtual
std
::
optional
<
PartialAssignment
>
Propagate
(
const
PartialAssignment
&
alpha
)
const
=
0
;
virtual
std
::
optional
<
PartialAssignment
>
Propagate
(
const
PartialAssignment
&
alpha
)
const
=
0
;
void
SetEliminationPolicy
(
DPEliminator
::
IGNORE_POLICY
ignore_policy
,
DPEliminator
::
INPROCESSING
inprocessing
,
DPEliminator
::
INCREASE_POLICY
increase_policy
,
BLOCK_PRIME
block_prime
)
DPEliminator
::
INPROCESSING
inprocessing
,
DPEliminator
::
INCREASE_POLICY
increase_policy
,
BLOCK_PRIME
block_prime
)
{
mElimIgnorePolicy
=
ignore_policy
;
mElimInprocessing
=
inprocessing
;
...
...
@@ -161,12 +164,11 @@ namespace SUBool
virtual
void
EliminateAuxVariablesWithMaxSize
(
size_t
max_size
);
// If min_steps==0, then the maximum possible size increase is used when
// calling DPEliminator.
virtual
void
EliminateAuxVariablesWithMaxSizeMinimize
(
size_t
max_size
,
size_t
min_steps
,
double
min_factor
);
virtual
void
EliminateAuxVariablesWithMaxSizeMinimize
(