/* A converter that converts DIMACS format into CLP(FD)
Neng-Fa Zhou, 2004
Input format:
The common data format for GRASP is conjunctive normal form (CNF). A CNF formula f on n binary variables x1,..., xn is the conjunction (AND) of m clauses w1,...,wm each of which is the disjunction (OR) of one or more literals, where a literal is the occurrence of a variable or its complement. A formula f denotes a unique n-variable Boolean function f(x1,...,xn) and each of its clauses corresponds to an implicate f.
The GRASP engine reads input in DIMACS format. The following is an example of a data file in DIMACS format:
c Example SAT format file in DIMACS format
c It contains a formula in cnf formulation.
c
c
p cnf 4 3
2 3 -4 0
-4 0
2 3 4 0
A line starting with 'c' indicates a comment. The line represented as 'p cnf #var #cl' indicates the number of variables and clauses in the CNF formula. A single number '0' at the end of the line identifies the end of the clause.
Output format:
go:-
[V1,V2,...,Vn] :: 0..1, % declaration of Boolean variables,
a sequence of constraints in the format X1 #\/ X2 #\/ ... #\/ Xn #= 1
where Xi is a literal (either a Boolean variable V or the complement
of a Boolean variable in the form #\ V),
labeling([V1,V2,...,Vn]),
write([V1,V2,...,Vn]),nl.
go:-
write(unsatisfiable),nl.
*/
cnf2pl(File):-
atom_codes(File,String),
(append(MainString,".cnf",String)->
InFile=File,
append(MainString,".pl",OutString),
atom_codes(OutFile,OutString);
append(String,".cnf",InString),
append(String,".pl",OutString),
atom_codes(InFile,InString),
atom_codes(OutFile,OutString)),
cnf2pl(InFile,OutFile).
cnf2pl(File,OutFile):-
format("cnf2pl(~q,~q)~n",[File,OutFile]),
see(File),
tell(OutFile),
format("go:-top.~n",[]),
format("top:-cputime(X),top(X).~n",[]),
readUntilPLine(N), %N is the declared number of variables
functor(VarVect,vars,N),
fillVarNames(VarVect,1,N),
format("top(Start):-~n",[]),
VarVect=..[_|VarList],
format("~t~w :: 0..1,~n",[VarList]),
readTrimLine(ClauseLine),
readWriteClauses(ClauseLine,VarVect),
seen,
format("~t~w,nl,~n",[labeling_ffc(VarList)]),
format("~t~w,nl,~n",[write(VarList)]),
% format("~tcputime(End),T is End-Start,write(T),write(milliseconds),nl,~n",[]),
format("~tfail.~n",[]),
format("top(Start):-~n",[]),
format("~twrite(unsatisfiable),nl,~n",[]),
format("~tcputime(End),T is End-Start,write(T),write(milliseconds),nl.~n",[]),
told.
fillVarNames(VarVect,N0,N):-N0>N,!.
fillVarNames(VarVect,N0,N):-
number_codes(N0,N0Codes),
atom_codes(VarName,[0'V|N0Codes]),
arg(N0,VarVect,VarName),
N1 is N0+1,
fillVarNames(VarVect,N1,N).
readUntilPLine(N):-
readTrimLine(Line),
(Line==[]->throw(mailformatedCNFFile);true),
(Line=[0'p|_]->
append("p cnf ",LineRest,Line),
append(NCodes,[0' |_],LineRest),!,
number_codes(N,NCodes);
readUntilPLine(N)).
readTrimLine(Line):-
readLine(Line1),
trimSpaces(Line1,Line2),
(Line2=[0'%|_]->readTrimLine(Line);
Line2=[0'0|_]->readTrimLine(Line);
Line=Line2).
trimSpaces([0' |Line],Line1):-!,
trimSpaces(Line,Line1).
trimSpaces(Line,Line1):-Line1=Line.
readWriteClauses([],VarVect):-!. % end of file
readWriteClauses(Line,VarVect):-
extractLiterals(Line,Signs,[],Literals,[],VarVect),
length(Literals,Len),
/*
% (Len=<15->
append(Signs,Literals,Args),
Propagator=..[$bc_clause|Args],
format("~t~w,~n",[Propagator]);
constructConstrExp(Signs,Literals,Exp),
format("~t~w#=1,~n",[Exp])),
*/
constructConstrExp(Signs,Literals,Exp),
format("~t(~w)#=1,~n",[Exp]),
readTrimLine(NextLine),
readWriteClauses(NextLine,VarVect).
extractLiterals([],Signs,SignsR,Literals,LiteralsR,VarVect):-!,%no 0 in the previous line
readTrimLine(Line),
extractLiterals(Line,Signs,SignsR,Literals,LiteralsR,VarVect).
extractLiterals(Line,Signs,SignsR,Literals,LiteralsR,VarVect):-
(append(VNCodes,[0' |LineRest],Line);
VNCodes=Line,LineRest=[]),!,
number_codes(Vn,VNCodes),
(Vn==0->Literals=LiteralsR,Signs=SignsR;
trimSpaces(LineRest,LineRest1),
extractLiterals(LineRest1,Signs1,SignsR,Literals1,LiteralsR,VarVect),
(Vn>0->arg(Vn,VarVect,V),Signs=[1|Signs1],Literals=[V|Literals1];
Vm is -Vn, arg(Vm,VarVect,V),
Signs=[0|Signs1],
Literals=[V|Literals1])).
constructConstrExp([],[],0):-!.
constructConstrExp([Sign],[V],Exp):-(Sign==1->Exp=V;Exp=(#\ V)).
constructConstrExp([Sign|Signs],[V|Vs],Exp):-
Exp=(L #\/ Exp1),
(Sign==1->L=V;L=(#\ V)),
constructConstrExp(Signs,Vs,Exp1).
labeling_c(VarList):-
get_constraints_numbers(VarList,PairsList),
sort(0,>=,PairsList,SortedList),
labeling_c_extract_vars(SortedList,Vars),
clpb_labeling(Vars).
get_constraints_numbers([],[]).
get_constraints_numbers([V|Vs],[(N,V)|PairsList]):-
constraints_number(V,N),
get_constraints_numbers(Vs,PairsList).
labeling_c_extract_vars([],[]).
labeling_c_extract_vars([(N,V)|Vs],[V|VarList]):-
labeling_c_extract_vars(Vs,VarList).
clpb_labeling([]):-true : true.
clpb_labeling([Var|Vars]):-integer(Var) :
clpb_labeling(Vars).
clpb_labeling([Var|Vars]):-true :
(Var=1;Var=0),
clpb_labeling(Vars).
/*
test([X,Y,Z]):-
[X,Y,Z] :: 0..1,
$bc_clause(0,1,1,X,Y,Z),
labeling([X,Y,Z]).
%generate action rules for Boolean constraints
gen_bcp(N0,N):-N0>N,!.
gen_bcp(N0,N):-
Arity is 2*N0,
functor(Head,$bc_clause,Arity),
number_vars(Head,0,_),
format("~w,~n",[Head]),
format("~t{",[]),
I is N0+1,
gen_bcp_events(I,Arity,Head),
format("}~n",[]),
format("~t=>'_$bcp'(~w).~n",[N0]),
N1 is N0+1,
gen_bcp(N1,N).
gen_bcp_events(I0,I,Head):-I0=:=I,!,
arg(I0,Head,X),
format("ins(~w)",X).
gen_bcp_events(I0,I,Head):-
arg(I0,Head,X),
format("ins(~w),",X),
I1 is I0+1,
gen_bcp_events(I1,I,Head).
$clpb_negation(X,Y),var(X),var(Y),{ins(X),ins(Y)}=>true.
$clpb_negation(X,Y),var(X)=>(Y==1->X=0;X=1).
$clpb_negation(X,Y)=>(X==1->Y=0;Y=1).
*/
main:-
get_main_args(L),
sat(L).
sat([File]):-!,
write('=>sat'),nl,
cnf2pl(File,'temp.pl'),
compile(temp),
load(temp),
go.
sat(_):-format("Usage: sat cnf-file~n",[]).