У меня есть формула в файле .dimacs/.cnf, как показано ниже:
p cnf 6 9
1 0
-2 1 0
-1 2 0
-5 1 0
-6 1 0
-3 2 0
-4 2 0
-3 -4 0
3 4 -2 0
Можно ли извлечь только те предложения, которые содержат, например, переменные 2, 3 и 4 в SAT4j? Затем мне нужно проверить согласованность только для этого нового набора предложений, т. е. для:
p cnf 4 6
-2 1 0
-1 2 0
-3 2 0
-4 2 0
-3 -4 0
3 4 -2 0
Я пытался использовать предположения, я пытался использовать ограничения, но я все еще не могу найти способ сделать это.
Спасибо за любое предложение.
Редактировать
Я думал, что есть метод типа solver.addClause(clause), но наоборот solver.getClause(clause)... Хотя, я кормлю решатель предложениями из файла .cnf.
Редактировать 2
Во-первых, предположения имеют тот же синтаксис, что и предложение,
val assumption: IVecInt = new VecInt(Array(1, 2))
val clause: IVecInt = new VecInt(Array(1, 2))
но переменные conjunctions в предположениях и disjunctions в предложении. Это разница. Верно? Мои тестовые примеры говорят об этом. (Мне просто нужно было получить дополнительное разрешение на это).
Во-вторых, моя проблема с использованием переменных селектора такова:
Простая формула a V b имеет три модели:
(a, b),
(a, -b),
(-a, b)
Когда я добавляю селекторную переменную, например, s, и ее предположение равно -s, то у меня есть такое же количество моделей, т. е. 3 модели:
(a, b, -s),
(a, -b, -s),
(-a, b, -s)
Когда предположение true, т. е. s, то у меня есть 4 модели вместо 0, которые я хочу:
(a, b, s),
(a, -b, s),
(-a, b, s),
(-a, -b, s)
Конечно когда s = T, то (s V a V b) = (T V a V b) = T, но разве это способ удаления пункта (a V b)? Мне нужно количество моделей, настоящих моделей! Есть ли способ найти точные модели, «удалив» каким-то образом эти переменные (т. е. a и b), которые мы хотим исключить по предположению?
В данном случае это мой текущий код на Scala:
object Example_01 {
val solver: ISolver = new ModelIterator(SolverFactory.newDefault())
val reader: DimacsReader = new DimacsReader(solver)
val problem: IProblem = reader.parseInstance("example_01.cnf")
def main(args: Array[String]): Unit = {
var nrModels: Int = 0
val assumptions: IVecInt = new VecInt(Array(10))
try {
while(solver.isSatisfiable(assumptions)) {
println(reader.decode(problem.model()))
nrModels += 1
}
} catch {
case e: ContradictionException => println("UnSAT: ", e)
}
println("The number of models is: " + nrModels)
}
Спасибо за любую помощь.
